Inductively Finding a Reachable State Space Over-Approximation

Abstract — We present an algorithm to find an overapproximation of the set of reachable states in a finite state machine. The algorithm works by inductively proving implications of the form a ⇒ b between pairs of nodes in the logic network. Because each implication proved is guaranteed to hold in every reachable state, the conjunction of the implications forms an over-approximation of the reachable state set. This over-approximation becomes tighter as more implications are proved, providing the user with a runtime vs. quality trade-off. Experimental results show that this method can find a tightenough reachable state space approximation to enable circuit optimization, even for very large problems. I