For the most recent entries see the Petri Nets Newsletter.

Improved Implementations via a New Structural Equivalence on Labeled Nets.

Fraczak, Wojciech; Pelz, Elisabeth

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.


Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography