2005 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年度から継続して行っている課題「抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証」において、平成17年度は「時相論理を用いたグラフ書き換え系の抽象化」に関する研究、および最終年度に際してこれまでの研究のとりまとめを行った。
我々は平成14年度よりグラフ上の書き換え系を時相論理により抽象化し、検証に利用することについて研究を行ってきた。グラフ上の書き換えはプログラム中で頻繁に用いられるリンク構造に対する操作を含んでおり、一般には状態空間が無限となるため、モデル検査等の有限的探索手法を用いる場合には抽象化が必要となる。
我々が時相論理を抽象化に用いているのは、(1)時相論理に対するいくつかの拡張がグラフ構造の抽象化に有用であること(2)決定可能な論理を用いることによって、充足可能性判定を抽象化に利用できることが主要な理由である。
(1)において我々が注目した拡張は2方向性、global modality,およびnominalである。空間的な性質の記述において順方向だけでなく逆方向の記述を要する際、逆様相を持つ時相論理、すなわち2方向の時相論理を用いるのが自然である。global modalityは抽象化によるshape analysisと充足可能性判定において構成されるタブローとを結びつける。nominalはループに関する性質等、グラフ上の空間的性質を記述する能力を強化する。
(1)のような拡張を施しても(2)の決定可能性が崩れないことが時相論理を用いる利点となっている。このことにより、抽象化に用いる時相論理式の集合が与えられれば、充足可能性判定を用いて抽象化が自動的に計算できるような枠組みになっている。平成15年度から継続して行っているBDDを用いた充足可能性判定手続きは、この抽象化の自動計算の部分で利用される。
|
