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

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

抽象モデル検査で用いられるグラフ探索アルゴリズムを証明検証系で形式化するための準備として、平成14年度は以下の点に関する研究を行った。1.平成13年度に引き続き、時間付き多重集合書き換えの性質の解析時間を含むシステムの代表例である時間オートマトンと時間ペトリネットの両方を包含するシステムとして平成13年度に導入した時間付き多重集合書き換えについて、基本的性質である到達可能性・有界性・被覆性の決定可能性に関する考察をより進めた。特に、有界性・被覆性が決定可能であるクラスをより詳細に特徴づけることにより、決定可能性の結果が時間オートマトンの決定可能性の一般化になるようにした。2.グラフの時相論理式による抽象化高橋・萩谷によるリンク構造の正則表現による抽象化を用いた抽象モデル検査の考え方を発展させ、リンク構造の一般化であるグラフを時相論理式によって抽象化する方法を与えた。これにより、一般には有限でないグラフ書き換えの結果を有限的に捕えることが可能となり、安全性に関するモデル検査が可能となる。上の2つの成果は次のように関連している。まず、多重集合に構造を導入することによりグラフが得られるため、時間付き多重集合書き換えの拡張として時間付きグラフ書き換えが考えられる。また、リンク構造の変化もやはりグラフ上の書き換えと捕えることができる。時間付きグラフ書き換えのとその抽象化を合わせて考えることにより、将来的に時間と空間の両方を扱うシステムの検証を行うことを目指している。