On-the-fly verification with stubborn sets

Abstract

A new on-the-fly verification method is presented. The method uses a generalization of Büchi automata called “tester processes” for representing and detecting illegal behaviour. To reduce the number of states that are constructed the method applies the stubborn set theory in a new way. The method can be used in connection with the “Supertrace” memory-saving technique. A simple algorithm is suggested for efficient detection of violations of an important subclass of liveness properties during the construction of the reduced state space.