Generating Petri net state spaces

Abstract

Most specific characteristics of (Place/Transition) Petri nets can be traced back to a few basic features including the monotonicity of the enabling condition, the linearity of the firing rule, and the locality of both. These features enable "Petri net" analysis techniques such as the invariant calculus, the coverability graph technique, approaches based on unfolding, or structural (such as siphon/trap based) analysis. In addition, most verification techniques developed outside the realm of Petri nets can be applied to Petri nets as well. In this paper, we want to demonstrate that the basic features of Petri nets do not only lead to additional analysis techniques, but as well to improved implementations of formalism-independent techniques. As an example, we discuss the explicit generation of a state space. We underline our arguments with some experience from the implementation and use of the Petri net based state space tool LoLA. © Springer-Verlag Berlin Heidelberg 2007.