Verification of ACTL properties by bounded model checking. EUROCAST

Summary With the papers of Biere et. al. [1, 2] in 1999, SAT-based bounded model checking (BMC) for verification of LTL properties has been introduced as a complementary technique to BDD-based symbolic model checking, and a lot of successful work has been done with this approach. The idea has later also been applied to the verification of ACTL (the universal fragment of CTL) properties [6]. The efficiency of this method is based on the observation that if a system is faulty then only a fragment of its state space is sufficient for finding an error. For valid properties, the length (completeness threshold) that needed to be checked in order to certify that the system is error free is usually quite big, such that it is not practical to use this approach for checking systems that are error free with respect to given properties. An improvement is to use approximations of such a length taking the diameter of the model into consideration. However, for a reasonably large system, this length would possibly also be large enough to make the verification intractable