BDD vs. Constraint-Based Model Checking: An Experimental Evaluationfor Asynchronous Concurrent Systems

BDD-based symbolic model checking has been applied to a wide range ofapplications. Recently, constraint-based approaches, which use arithmeticconstraints as a symbolic representation, have been used in symbolic modelchecking of infinite-state systems. We argue that use of constraint-basedmodel checking is not limited to infinite-state systems. It can also be anefficient alternative to BDD-based model checking for systems with integervariables that have large domains. In this paper we compare the performance ofBDD-based model checker SMV to the performance of our constraint-based modelchecker on verification of several asynchronous concurrent systems. Theresults indicate that constraint-based model checking is a viable option forverification of asynchronous concurrent systems that require more than 5boolean variables to encode each integer variable.