BDDを用いた2方向CTL論理式充足可能性決定手続きの実装

DOI

書誌事項

タイトル別名
  • An Implementation of a Decision Procedure for Satisfiability of Two-way CTL Formulas Using BDD

説明

Deciding satisfiability plays an important role in abstraction methods used for formal verification such as model checking. In their previous work, the authors developed a decision procedure for judging satisfiability of two-way CTL formulas and applied it to the analysis of concurrent systems such as cellular automata. In this paper we provide its correctness proof and report its efficient implementation, which achieves performance sufficient for practical application owing to the use of BDD, while naive implementations would require large space and time.

収録刊行物

詳細情報 詳細情報について

  • CRID
    1390282679714375040
  • NII論文ID
    130004892028
  • DOI
    10.11309/jssst.22.3_154
  • ISSN
    02896540
  • データソース種別
    • JaLC
    • CiNii Articles
  • 抄録ライセンスフラグ
    使用不可

問題の指摘

ページトップへ