An Implementation of a Decision Procedure for Satisfiability of Two-way CTL Formulas Using BDD

DOI
  • TANABE Yoshinori
    Japan Science and Technology Agency Research Center for Verification and Semantics, National Institute of Advanced Industrial Science and Technology (AIST)
  • TAKAHASHI Koichi
    Research Center for Verification and Semantics, National Institute of Advanced Industrial Science and Technology (AIST)
  • YAMAMOTO Mitsuharu
    Faculty of Science, Chiba University
  • SATO Takahiro
    Graduate School of Information Science and Technology, University of Tokyo
  • HAGIYA Masami
    Graduate School of Information Science and Technology, University of Tokyo

Bibliographic Information

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

Description

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.

Journal

  • Computer Software

    Computer Software 22 (3), 154-166, 2005

    Japan Society for Software Science and Technology

Details 詳細情報について

  • CRID
    1390282679714375040
  • NII Article ID
    130004892028
  • DOI
    10.11309/jssst.22.3_154
  • ISSN
    02896540
  • Data Source
    • JaLC
    • CiNii Articles
  • Abstract License Flag
    Disallowed

Report a problem

Back to top