On-The-Fly Verification Of Finite Transition Systems

The analysis of programs by the exhaustive inspection of reachable states in a finite state graph is a well-understood procedure It is actually implemented in several industrial tools but one of their main limitations is the size of the memory needed to exhaustively build the state graphs of the programs. For numerous properties such as Buchi acceptance (in the deterministic case) and behavioral equivalence, it is not necessary to explicitly build this graph and an exhaustive depth--first traversal is often sufficient. In order to avoid retraversing states, it is however important to store in memory some of the already visited states and randomly replace them (to keep the memory size bounded and avoid a performance falling down) In most cases this depth--first traversal with replacement can push back significantly the limits of verification tools