State reduction using reversible rules
C. Norris Ip, David L. Dill · 1996
We reduce the state explosion problem in automatic verification of finite-state systems by automatically collapsing subgraphs of the state graph into abstract states. The key idea of the method is to identify state generation rules that can be inverted. It can be used for verification of deadlock-freedom, error and invariant checking and stuttering-invariant CTL model checking. 1 Introduction Formal verification methods that rely on state enumeration are very effective in catching errors in designs. However, such methods suffer from the state explosion problem: the vast number of possibilities cannot be explored within available time and memory. The number of possibilities usually grows exponentially with number of components in the system. Although many techniques (e.g. BDDs [1, 3]) have been developed to tackle the state explosion problem, a lot of practical designs are still too complicated for automatic verification, especially for high level systems or protocols [8]. In this exp...