In: Proceedings of the 10th International Conference on Application and Theory of Petri Nets, 1989, Bonn, Germany; Supplement, pages 1-22. 1989.
Also in: Rozenberg, G.: Lecture Notes in Computer Science, Vol. 483; Advances in Petri Nets 1990, pages 491-515. Berlin, Germany: Springer-Verlag, 1991.
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 method preserves all terminal states and the existence of nontermination. It is shown how the method can be used to detect violations of invariant properties. The method preserves the liveness and livelocks which cannot be exited. The theory is developed in an abstract variable/transition framework and adapted to elementary Petri nets, place/transition nets, and coloured Petri nets.
Keywords: stubborn sets (for) reduced state space generation; terminal state preservation; violation; liveness preservation; livelock preservation; variable/transition framework; place/transition net; coloured net.