形式的設計検証のための分岐時間正則時相論理

概要

論文の詳細を見る
論理設計の多様化,複雑化にともない,設計が正しいことを示すための検証手法の確立が重要な課題となっている.対象を順序機械などの有限状態の機械ととらえたとき,設計が仕様を満足するかどうかを厳密に示すために,命題時相論理によって仕棟を記述し,モデル検査アルゴリズムを適用する手法が提案されている.命題時相論理には種々の体系が存在するが,このうちClarkeらによって提唱されたCTL(Computational Tree Logic)では,有限状態機械の動作を反映するKripke構造Sの大きさ(Size(S))と時相論理式fの長さ(Len(f))の積に対し線形時間でモデル検査を行うことができ,順序機械,通信プロトコルなどの検証に応用されてきている.しかし,本輪文で示すように,CTLは事象の繰り返しなどの性質を記述できないといった問題点があり,有限状態機械の仕様の記述に用いることを考えた場合,十分な表現力を持つとは言えない.そこで本論文ではCTLと比べ真に高い表現能力を持つ分岐時間正則時相論理(Branching time RegularTemporal Logic,BRTL)を提案する.またそのモデル検査アルゴリズムを示し,その時間計算量がCTLの場合と同じく,Size(S)とLen(f)の積に比例することを証明する.
一般社団法人情報処理学会の論文
1992-04-15