線形時間のモデルチェックアルゴリズムを持つ正則時相論理と変数代入機構による拡張

概要

論文の詳細を見る
順序機械など有限状態システムの設計が正しいことを保証するための検証手法の確立が重要な課題となっている。我々はこれまで正則時相論理(RTL, Regular Temporal Logic)のモデルチェックアルゴリズムを示し、またこれに基づき実際に順序機械のの検証を行なってきた。RTLは任意の有限オートマトンを特徴づけることができるが、モデルチェックの計算複雑度は非初等的と大きい。また、CTL (Computational Tree Logic)は、有限状態システムの動作を反映するKripke構造Sの大きさ(|S|)と時相論理式fの長さ(|f|)の積に対し線形時間でモデルチェックを行うことができるが、表現能力が低く有限オートマトンを特徴づけることができない。本稿ではまずCTLよりも高い表現能力を持つRRTL(Restricted Regu1ar Temporal Logic)を提案し、CTLと同じく|S|と|f|の積に比例する時間計算量を持つモデルチェックアルゴリズムを示す。次に、時相論理式による記述の簡潔にするため、RRTLにブール変数への代入とそれらの値を参照する機構を導入したER-RTL(Extended RRTL)を定義し、O(|S|×|F|×2^<|V|>)(Vはブール変数の集合)の時間計算量を持つモデルチェックアルゴリズムを示す。
一般社団法人情報処理学会の論文
1990-03-14