| 研究課題/領域番号 |
20700004
|
|---|
| 研究種目 |
若手研究(B)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
情報学基礎
|
|---|
| 研究機関 | 鳥取環境大学 |
|---|
研究代表者 |
西澤 弘毅 鳥取環境大学, 環境情報学部, 講師 (60455433)
|
|---|
| 研究期間 (年度) |
2008 – 2009
|
| 研究課題ステータス |
完了 (2009年度)
|
| 配分額 *注記 |
1,950千円 (直接経費: 1,500千円、間接経費: 450千円)
2009年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2008年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
|
|---|
| キーワード | 情報基礎 / システム検証 / モデル検査 / 抽象化 / 多値論理 |
|---|
| 研究概要 |
ソフトウェアやハードウェアの誤動作によって起こる社会的な問題は後を絶たない。そこで、これらのシステムを稼働前に検証するモデル検査の技術が広まりつつある。本研究では、モデル検査で不可欠な「抽象化」と呼ばれる効率化情報を再利用または修正するための理論を与える。ある性質の検証には有効であった抽象化も、別の性質の検証にはまったく役に立たない場合があるため、現在のシステム検証の現場では、抽象化のコストが高い。本研究によって抽象化の再利用が進めば、抽象化のコストを下げることができる。本研究では特にさまざまな多値論理の間で抽象化を再利用するための理論を与える。抽象化の正しさは多値論理と模倣の理論に基づいて数学的に保証する。
研究成果は以下の通りである。4つの多値論理(Frame、DeMorgan Frame、Bilattice、MixedTS)を例に含む一般性の高い不動点論理を提案した。その論理のもとで、「随伴の対」によって抽象化を定義し、この抽象化によって検証結果を引き戻せることを証明した。そして、論理を変えたときに、抽象化を再利用できるための十分条件を与えた。
関連研究として、べき集合を用いた多値論理の上の単項演算子についても分析した。その結果、単項演算子の別表現として知られる「多重関係」の階層構造と、クリーネ代数の階層構造との対応付けを発見した。
|
