Abstraction of Systems with Counters for Symbolic Model Checking

ion of Systems with Counters for Symbolic Model Checking # Klaus Schneider and George Logothetis University of Karlsruhe, Department of Computer Science, Institute for Computer Design and Fault Tolerance (Prof. Dr.-Ing. D. Schmid), P.O. Box 6980, 76128 Karlsruhe, Germany, email: {Klaus.Schneider,George.Logothetis}@informatik.uni-karlsruhe.de, http://goethe.ira.uka.de/ 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..