Verification of ACTL Properties by Bounded Model Checking

摘要

SAT-based bounded model checking has been introduced as a complementary technique to BDD-based symbolic model checking in recent years and a lot of successful work has been done with this approach. The success is mostly due to the efficiency of error-detection. Verification of valid properties depends on a completeness threshold that could be too large to be practical. We discuss an approach to checking valid ACTL (the universal fragment of CTL) properties similar to bounded model checking of ACTL. Bounded model checking of ATCL has been considered in [8]. Given a model M and an ACTL formula φ, a series of k-models of M are constructed for k = 0,1,2,..., and the process for checking φ proceeds as follows: start with the 0-model, if the model does not satisfy the negation of φ, use 1-model and so forth, until the negation of φ is satisfied or until a bound of k is reached. A general bound for k is the number of states of M. Trying all k-models up to the bound in order to obtain a conclusion is obviously not desirable. For attacking this problem, we propose an approach to (partly) avoid the use of such a bound.