Computational challenges in bounded model checking

We describe several observations regarding the completeness and the complexity of bounded model checking and propose techniques to solve some of the associated computational challenges. We begin by defining the completeness threshold (CT) problem: for every finite model M and LTL property φ, there exists a number CT such that if there is no counterexample to φ in M of length CT or less, then M satisfies φ. Finding this number, if it is sufficiently small, offers a practical method for making bounded model checking complete. We describe how to compute an overapproximation to CT for a general LTL property using Büchi automata, following the Vardi-Wolper LTL model checking framework. This computation is based on finding the initialized diameter and initialized recurrence-diameter (the longest loop-free path from an initial state) of the product automaton. We show a method for finding a recurrence diameter with a formula of size O(klogk) (or O(k(logk)²) in practice), where k is the attempted depth, which is an improvement compared to the previously known method that requires a formula of size in O(k²). Based on the value of CT, we prove that the complexity of standard SAT-based BMC is doubly exponential and that, consequently, there is a complexity gap of an exponent between this procedure and standard LTL model checking. We discuss ways to bridge this gap.

International Journal on Software Tools for Technology Transfer 7(2), 2005. 10 pages.

PDF © 2005 Springer-Verlag.