*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 L_{1}) 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*