研究課題
若手研究(B)
ソフトウェアやハードウェアの誤動作によって起こる社会的な問題は後を絶たない。そこで、これらのシステムを稼働前に検証するモデル検査の技術が広まりつつある。本研究では、モデル検査で不可欠な「抽象化」と呼ばれる効率化情報を再利用または修正するための理論を与える。ある性質の検証には有効であった抽象化も、別の性質の検証にはまったく役に立たない場合があるため、現在のシステム検証の現場では、抽象化のコストが高い。本研究によって抽象化の再利用が進めば、抽象化のコストを下げることができる。本研究では特にさまざまな多値論理の間で抽象化を再利用するための理論を与える。抽象化の正しさは多値論理と模倣の理論に基づいて数学的に保証する。研究成果は以下の通りである。4つの多値論理(Frame、DeMorgan Frame、Bilattice、MixedTS)を例に含む一般性の高い不動点論理を提案した。その論理のもとで、「随伴の対」によって抽象化を定義し、この抽象化によって検証結果を引き戻せることを証明した。そして、論理を変えたときに、抽象化を再利用できるための十分条件を与えた。関連研究として、べき集合を用いた多値論理の上の単項演算子についても分析した。その結果、単項演算子の別表現として知られる「多重関係」の階層構造と、クリーネ代数の階層構造との対応付けを発見した。
すべて 2009 2008
すべて 雑誌論文 (4件) (うち査読あり 4件) 学会発表 (2件)
コンピュータソフトウェア Vol.26、No.2
ページ: 147-156
Bulletin of Informatics and Cybernetics Vol.41
ページ: 40871
Relations and Kleene Algebra in Computer Science RelMiCS/AKA(Springer LNCS) Vol.5827
ページ: 276-290
Proc. Relations and Kleene Algebra in Computer Science, LNCS Vol.4988
ページ: 110-122
