抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証

点击翻译按钮获取中文摘要

平成13年度から継続して行っている課題「抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証」において、平成15年度は「2方向計算木論理(2CTL)を用いたグラフ遷移系の抽象化」に関する研究を行った。「2方向計算木論理を用いたグラフ遷移系の抽象化」は、平成14年度に行ったグラフとその上の書き換えによるシステムの抽象化の議論をより一般化な形で展開したものであり、セルをリンクによって繋いでできる構造からなるシステムにおいて、隣接あるいは関連するセルの状態に応じてセルの状態が同期的あるいは非同期的に変化するような状況を抽象化するためのものである。グラフ上の書き換えはプログラム中で頻繁に用いられるリンク構造に対する操作を含んでおり、一般には状態空間が無限となるため、モデル検査等の有限的探索手法を用いる場合には抽象化が必要となる。従来研究と比較して、本研究は以下のような特徴を有している。・セルオートマトンの解析セルの状態が同期的あるいは非同期的に変化する場合の両方について扱っている。・2CTLの利用セルの抽象的状態を記述するために、通常の計算木論理(CTL)に逆方向の様相を追加した2方向計算木論理(2CTL)を使用している。抽象化の計算においては2CTLの充足可能性判定が大きな役割を果たしている。・抽象化の自動計算抽象化を特徴付ける2CTL論理式の集合を与えると、抽象化を自動的に計算することができる。これを可能にするため、2CTLの充足可能性判定手続きの定式化を行った。