An Iterative Method for Reached State Approximation

In this paper we present a new method for computing the approximate reached state set of a finite state machine by modifying its transition relation. Both upper and lower bounds are computed using this method. 1 Introduction Computing the set of reached states in a finite state machine (FSM) is a key operation in both verification [1] and synthesis [2] & [3]. The reached state set allows designers to check a design for errors and other unwanted behavior. It is a precise measure of the exact set of states a design can take under all possible inputs. Given a directed graph, and a set of initial nodes in the graph, reachability computes the set of nodes on some path from the initial nodes. A FSM can be represented by a directed graph, which is also called a state transition graph. Computing the reachable states (nodes) of this graph can be done by a breadth first search traversal of the state transition graph beginning at the initial states. Unfortunately this computation explodes when t..