2009 Fiscal Year Annual Research Report
| Project/Area Number |
20700004
|
|---|
| Research Institution | Tottori University of Environmental Studies |
|---|
Principal Investigator |
西澤 弘毅 Tottori University of Environmental Studies, 環境情報学部, 講師 (60455433)
|
|---|
| Keywords | 情報基礎 / システム検証 / モデル検査 / 抽象化 / 多値論理 |
|---|
| Research Abstract |
ソフトウェアやハードウェアの誤動作によって起こる社会的な問題は後を絶たない。そこで、これらのシステムを稼働前に検証するモデル検査の技術が広まりつつある。本研究では、モデル検査で不可欠な「抽象化」と呼ばれる効率化情報を再利用または修正するための理論を与える。ある性質の検証には有効であった抽象化も、別の性質の検証にはまったく役に立たない場合があるため、現在のシステム検証の現場では、抽象化のコストが高い。本研究によって抽象化の再利用が進めば、抽象化のコストを下げることができる。本研究では特にさまざまな多値論理の間で抽象化を再利用するための理論を与える。抽象化の正しさは多値論理と模倣の理論に基づいて数学的に保証する。
研究の結果、4つの多値論理(Frame、DeMorgan Frame、Bilattice、MixedTS)を例に含む一般性の高い不動点論理を提案することができた。また、それらにおける模倣の健全性を証明することができた。これによりさまざまな多値論理やさまざまな抽象化を含む一般的な論理を提案したといえる。これらについては、後日、成果をまとめた論文を発表する予定である。
関連研究として、べき集合を用いた多値論理の上の単項演算子についても分析した。その結果、単項演算子の別表現として知られる「多重関係」の階層構造と、クリーネ代数の階層構造との対応付けを発見した。これについては、査読付論文として発表した。
|
