Stubborn sets for reduced state space generation

Abstract

The "stubborn set" theory and method for generating reduced state spaces is presented. The theory takes advantage of concurrency, or more generally, of the lack of interaction between transitions, captured by the notion of stubborn sets. The basic method preserves all terminal states and the existence of nontermination. A more advanced version suited to the analysis of properties of reactive systems is developed. It is shown how the method can be used to detect violations of invariant properties. The method preserves the liveness (in Petri net sense) of transitions, and livelocks which cannot be exited. A modification of the method is given which preserves the language generated by the system. The theory is developed in an abstract variable/transition framework and adapted to elementary Petri nets, place/transition nets with infinite capacity of places, and coloured Petri nets. Keywords system verification, analysis of behaviour of nets CONTENTS