2004 Fiscal Year Annual Research Report
抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証
| Project/Area Number |
16016211
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
山本 光晴 千葉大学, 理学部, 助教授 (00291295)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
萩谷 昌己 東京大学, 大学院・情報理工学系研究科, 教授 (30156252)
辻 尚史 千葉大学, 理学部, 教授 (70016666)
|
|---|
| Keywords | 形式的手法 / 証明検証系 / 抽象モデル検査 / 時相論理 / セルオートマトン / グラフ書き換え |
|---|
| Research Abstract |
平成13年度から継続して行っている課題「抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証」において、平成16年度は「グラフ遷移系の抽象化のための逆様相を持つ時相論理とその充足可能性」に関する研究を行った。
我々は平成14年度よりグラフ上の書き換え系を時相論理により抽象化し、検証に利用することについて研究を行ってきた。グラフ上の書き換えはプログラム中で頻繁に用いられるリンク構造に対する操作を含んでおり、一般には状態空間が無限となるため、モデル検査等の有限的探索手法を用いる場合には抽象化が必要となる。
時相論理による抽象化を自動的に行うには、時相論理式の充足可能性判定を実用的な時間で行う必要がある。我々は、逆様相を持つ時相論理の一つである2CTLの充足可能性判定手続きをBDD(2分決定グラフ)を用いて実装し、その効率について評価を行った。また、BDDを用いた充足可能性判定法がどのぐらいの強さの論理にまで適用可能かについて考察を行っている。
さらに、時相論理の充足可能性による抽象化手法を2次元セル・オートマトンのような格子状の隣接関係を持つシステムに応用するため、格子状の様相を持つ時相論理とその充足可能性について考察を行った。このような論理における充足可能性は一般的には決定不能であるが、Presburger論理式を利用して典型的な問題が持つ周期性を捕えられるようにしたことが特徴である。
|
