第一階述語論理のサブクラスに対する項の高さ縮減を用いた不変条件の近似的検証アルゴリズム

摘要

自動的にハードウェア設計の形式的検証を行う手法にモデルチェッキング技術があるが,モデルチェッキングには,扱うシステムが大規模になると状態数が爆発してしまい,計算量的に適用できないという問題がある.計算量を軽減するための1つの方法として,EUFと呼ばれる第一階述語論理のサブクラスを用いてシステムを抽象化する手法が提案されているが,EUFを用いたモデルチェッキングは一般に決定不能であることが知られている.本稿では,EUFの項の高さに上限を与えることで,現れうる項の形を制限し,状態集合の数え上げを終了させる手法を提案する.また数え上げた状態集合に対して,指定した不変条件の成立を保証できる近似アルゴリズムを提案する.さらに,アルゴリズムを簡単な回路設計に適用した例を示す.