Evaluation of SAT-based Bounded Model Checking of ACTL Properties

Bounded model checking (BMC) based on SAT has been introduced as a complementary method to BDD based symbolic model checking of LTL and ACTL properties in recent years. For general LTL and ACTL properties, BMC has traditionally aimed mainly at error detection, taking the advantage that error detection may only need to explore a small portion of the whole state space. Recently bounded model checking aiming at verification has also been proposed. The aim of this paper is to exploit the strength of BMC methods by combining different BMC approaches and compare it with the traditional BDD-based symbolic methods. We consider two bounded model checking methods, which are for error detection and verification of ACTL properties, respectively, and then combine them to a BMC algorithm. Based on this algorithm, we have implemented a tool named BMV (bounded model verifier), and carried out a number of experiments, and we have then compared BMV with Cadence SMV. The experimental results show that for certain types of problems, both for verification and error detection, BMV can perform much better than Cadence SMV in both time and memory consumption, and we believe that this is the first attempt to have an implementation of a method that combines practical error detection and verification of ACTL properties by SAT-based model checking.