Jensenらは, プログラムと時相論理式を用いて記述した検証条件を与えたとき に, プログラムの到達可能な状態全てが検証条件を満たすかどうかを決定する 問題として検証問題を定義した. そして, 彼らの論文では, 相互再帰を含まな いプログラムのクラスに対して検証問題が決定可能となることが示されている.
本発表では, プログラムのトレース集合がインデックス言語となることを示し,
その系として検証問題が決定可能となることを示す. 本手法は, 検証条件を時
相論理式よりも真に表現能力の大きい正規言語で記述することができ, かつ,
任意のプログラムに対して検証可能となるため, Jensenらの結果を真に改善し
ている.
さらに, 検証問題の計算複雑さについても述べ, 効率良く解ける検証問題の部
分クラスを提案する.