Model Checking is a technique for verifying the correctness of temporal properties over finite transition systems such as protocols and hardware circuits. The standard Model Checking algorithm searches for errors by symbolically exploring the reachable state-space. Bounded Model Checking (BMC) is a rather new SAT-based method for verifying properties up to a given depth $k$. BMC is conducted in an iterative process, where $k$ is incremented until either an error is found, the problem becomes intractable, or $k$ reaches some pre-computed threshold (the `completeness threshold'), which indicates that the property holds globally. The value of this threshold depends on the temporal property, the verified model, and the reduction method to SAT. Calculating this value for arbitrary Linear Temporal Logic (LTL) properties was so far an open problem.

The talk will begin with an overview of BMC, and some experimental results showing its efficiency. It will then focus on the question of how to compute the value of the Completeness Threshold for general LTL formulas. Since the complexity of BMC depends on this value, we show that there is a complexity gap of an exponent between BMC and competing methods, like traditional (unbounded) LTL model checking. It is still unknown whether this gap can be closed without loosing the main benefits of BMC.

This is work in progress with J. Ouaknine and E. Clarke.