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

• 田辺 良則

  (独) 科学技術振興機構CREST (独) 産業技術総合研究所システム検証研究センター

• 高橋 孝一

  (独) 産業技術総合研究所システム検証研究センター

• 山本 光晴

  千葉大学理学部

• 佐藤 貴洋

  東京大学大学院情報理工学系研究科

• 萩谷 昌己

  東京大学大学院情報理工学系研究科

書誌事項

タイトル別名

• 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.

収録刊行物

• コンピュータ ソフトウェア

  コンピュータ ソフトウェア 22 (3), 154-166, 2005

  日本ソフトウェア科学会

詳細情報

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