2011 Fiscal Year Annual Research Report
| Project/Area Number |
21500006
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
田辺 良則 国立情報学研究所, アーキテクチャ科学研究系, 特任研究員 (60443199)
|
|---|
| Keywords | 様相論理 / 法定手続き / ソフトウェア検証 / モデル検査 / 充足可能性 / 様相μ計算 / min-plus代数 |
|---|
| Research Abstract |
平成23年度には,(1)N∞値充足可能性判定法の研究,および(2)昨年度までの本研究での結果をモデル検査および定理証明支援系へ応用する研究を実施した.
(1)昨年度までに得らた充足可能性判定法は,N∞値様相μ計算論理式を,それと充足可能性が同値となる2値論理式の充足可能性判定問題に帰着する変換を与えるものであった.この方式には,計算量的には不利であることと,判定可能な値が0と∞のみであることであるという問題点がある.これを解決するため,本年度は2値論理式を経由しない直接の判定手続きの構築に取り組んだ.昨年度までの検討では,タブローノードに意味を与えても展開がうまくできないという課題を抱えていた.これを,論理式の値が「k以下」,「kより大きい」という意味を与えうるようにタブローノードの構成を拡張することによって,すべての論理記号に関する展開をうまく機能させることに成功した.もう一つの課題であった優先度関数の定義に関しても,ローカルに優先度を定義するのではなく,繰り返して現れるノード間に,否定に関する遷移が存在するかどうかに依存して優先度を変化させる方法を導入することで,充足可能性と整合する定義を与えることができた.この部分の正当性の証明には,21年度の成果であるゲーム意味論をうまく利用している.以上のアイディアをベースに,判定手続きは完成を見た.正当性証明については骨格をまとめた段階で年度末を迎えてしまったが,引き続き証明の執筆を行っている.
(2)本研究の応用先として,定理証明支援系への組み込みに取り組んだ.N∞値が減少する列になることを示すことで,プログラムが停止することを示す枠組みである.本年度は,証明支援系CoqでN∞(min-plus代数)に関するライブラリを作成し,システム記述の際に取り込めるようにした.この上でモデル検査アルゴリズムの停止性証明を行うことを目指した実装を行った.
|
