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 semantics, based on converting a Kripke model to a model (called a k-model) in which the transition relation is captured by a set of k-paths (each path with k transitions). This bounded semantics is not practically useful for the evaluation of a formula, since it involves too many paths in the k-model. Then the technique is to divide the k-model into submodels with a limited number of k-paths (which depends on k and the ACTL property to be verified) such that if an ACTL property is true in every such model, then it is true in the k-model as well. This characterization can then be used as the basis for practical verification of valid ACTL properties by satisfiability checking. A simple case study is provided to show the use of this approach for both verification and error detection of an abstract two-process program written as a first order transition system.