Abstraction of Systems with Counters for Symbolic Model Checking.
Klaus Schneider, George Logothetis · 1999
Abstract Model checking of temporal logics has become a standard technique for the verification of finite state reactive systems. However, these procedures suffer from the so-called state explosion problem which limits their practical use. Therefore, appropriate abstractions have to be applied to reduce the state space if these tools are to be applied to real-world problems. In particular, counters are hard to verify with model checking procedures. Hence, we present in this paper a special abstraction technique for counters that leads to very small, and in particular finite, state spaces. The method even allows in many cases to verify generic systems without interactive theorem proving, i.e. without induction. As counters are often used for the implementation of control systems, the method presented here is of essential importance for the verification of these systems. 1