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

• 安藤, 崇央

• 萩原, 茂樹

• 米﨑, 直樹

書誌事項

タイトル別名

• Implementation Method of LTL Tableau Construction using SAT Solver

抄録

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

In system development processes, we could number of reduce reversions if realizability for system specifications is verified before implementation of the system. For some properties that are necessary conditions of realizability, procedures to check whether system specifications satisfy those properties have been implemented. Since their algorithms have inherently high complexity, the practicality of them depends on using combining various efficient implementations. In those procedures, the graph which represents a state transition model of system is constructed from a system specification. Therefore it is important to implement the graph construction sub-procedure efficiently. In this paper, we propose a method of using a SAT solver for implementing the graph construction sub-procedure. In our method, generation of nodes in the procedure is reduced to searching out all minimal models of SAT problem for propositional formula, and, by solving the problem quickly with a SAT solver, we attempt to increase the efficiency of the procedure. From results of experiments to compare between our implementation of graph construction procedure and existing implementation using BDD, we concluded that our implementation method has some advantages.

収録刊行物

• 情報処理学会論文誌

  情報処理学会論文誌 55 (2), 909-921, 2014-02-15

キーワード

• [特集：ソフトウェア工学] 形式手法，線形時相論理，タブロー法，SAT solver

詳細情報

• CRID: 1050001337904422144
• NII論文ID: 110009665001
• NII書誌ID: AN00116647
• ISSN: 18827764
• Web Site: http://id.nii.ac.jp/1001/00098489/
• 本文言語コード: ja
• 資料種別: journal article
• データソース種別:
  • IRDB
  • CiNii Articles
  • KAKEN