Incremental Methods for FSM Traversal

Computing the set of reachable states of a finite state machine is an important component of many problems in the synthesis, and formal verification of digital systems. Computing the reachable states is computationally expensive due to the "explosion" in the number of states in real designs. However, the process of design is usually iterative, and the designer may modify and recompute information many times. Unfortunately, the reachability computation is called each time the designer modifies the system, because current methods for reachability analysis are not incremental. The current method for representation of the reachable states is inherently non-updatable. We solve this problem by presenting alternate ways to represent the reachable set, and incremental algorithms that can update the new representation each time the designer changes the system. The incremental algorithms use the reachable set computed at a previous iteration and information about the changes to the system to upd..