Model Checking with SAT-Based Characterization of ACTL Formulas

Bounded semantics of LTL with existential interpretation and that of ECTL (the existential fragment of CTL), and the characterization of these existentially interpreted properties have been studied and used as the theoretical basis for SAT-based bounded model checking [2, 18]. This has led to a lot of successful work with respect to error detection in the checking of LTL and ACTL (the universal fragment of CTL) properties by satisfiability testing. Bounded semantics of LTL with the universal interpretation and that of ACTL, and the characterization of such properties by propositional formulas have not been successfully established and this hinders practical verification of valid universal properties by satisfiability checking. This paper studies this problem and the contribution is a bounded semantics for ACTL and a characterization of ACTL properties by propositional formulas. Firstly, we provide a simple bounded semantics for ACTL without considering the practical aspect of the se...

• Type: Conference
• Year: 2007
• Where: ICFEM
• Authors: Wenhui Zhang
• Keywords: ACTL Properties, ACTL Property, ICFEM 2007, Semantics