In: IEICE Trans. on Fundamentals of Electronics, Communications, and Computer Science, Vol. E77-A, No. 10, pages 1602-1606. 1994.
Abstract: State space explosion is a serious problem in analyzing discrete event systems that allow concurrent occurring of events. A new method is proposed for generating reduced state spaces of systems. This method is an improvement of Valmari's stubborn set method. The generated state space preserves liveness, livelocks, and terminal states of the ordinary state space. Petri nets are used as a model of systems, and a method is shown for generating a reduced state space from a given Petri net.
Keywords: Petri nets, concurrent systems, state space generation, stubborn sets, weak persistency.