SAT solverを用いるLTLタブロー構成法とその評価

概要

論文の詳細を見る
システム仕様が実現可能性を満足するかどうかを,そのシステムの実装前に判定しておくことは,開発プロセスの手戻りを減らすことにつながる.システム仕様の実現可能性に関わる様々な性質について,システム仕様がそれらを満足するかどうかを判定するための手続きが実装されている.その実用性は,アルゴリズムの本質的な複雑さから,様々な効率的な実装手法を組み合わせて用いることに頼っている.この手続きでは,システム仕様からシステムの状態遷移モデルを表すグラフを構成する必要がある.本稿では,効率の良いグラフ構成手続きの実装としてSAT solverを用いる手法を提案する.提案手法は,グラフ構成における次ノード集合の計算を,SAT問題のすべての極小モデルを生成することに帰着し,SAT solverにより高速に解くことで効率化をはかる.また,これまでに提案されているBDDを用いた実装と,本実装との比較実験を行い,その結果から本実装はBDDを利用する実装に比べ,構成するグラフのサイズを同程度に小さく抑えられること,使用メモリを小さく抑えられ空間的に効率的であることを確認した.さらに,例題によってはグラフ構成にかかる時間を短縮できることも確認した.
2014-02-15