In: Azéma, P.; Balbo, G.: Lecture Notes in Computer Science, Vol. 1248: 18th International Conference on Application and Theory of Petri Nets, Toulouse, France, June 1997, pages 117-135. Berlin, Germany: Springer-Verlag, June 1997.
Abstract: In almost all process algebras the equation P;Ø=P holds on a semantic level. This is not the case for standard Petri Box Calculus (PBC), whose semantic domain is a class of labeled Petri Nets, called ``Boxes''. By making this equation true, we resolve a problem arising during the development of the PEP-programming environment, in fact a limitation of model checking possibilities, due to the semantics of the ``iteration'', one of the important operators of the PBC.
We introduce a new structural equivalence on labeled nets, based on a reduction of ``silent transitions''. Consequently, we show that the net semantics implemented in the actual PEP-versions, which ensures minimal size of the nets and 1-safeness, is equivalent (w.r.t. the new equivalence) to the original one. For the verification of properties expressed in L (a slight extension of Esparza's logic L1) we show the coherence between new equivalent nets, via some non-trivial transformation of formulas. In this way, the possibility of model-checking is extended to all those terms (or programs) which lead in the original semantics to non 1-safe nets.
Back to the Petri Nets Bibliography