*For the most recent entries see the
Petri Nets Newsletter.*

## Automatic Symmetry Detection in Well-Formed Nets.

Thierry-Mieg, Yann;
Dutheillet, Claude;
Mounier, Isabelle
In:
*Proceedings of the 24th International Conference on Applications and Theory of Petri Nets (ICATPN 2003), Eindhoven, The Netherlands, June 23-27, 2003*, pages 82-101.
Volume 2679 of Lecture Notes in Computer Science / Wil M. P. van der Aalst and Eike Best (Eds.) --- Springer-Verlag,
June 2003.

Abstract:
Formal verification of complex systems using high-level Petri Nets faces
the so-called state-space explosion problem. In the context of Petri nets
generated from a higher level specification, this problem is particularly
acute due to the inherent size of the considered models. A solution is to
perform a symbolic analysis of the reachability graph, which exploits the
symmetry of a model.

Well-Formed Nets ( WN) are a class of high-level Petri nets, developed
specifically to allow automatic construction of a symbolic reachability
graph (SRG), that represents equivalence classes of states. This relies on
the definition by the modeler of the symmetries of the model, through the
definition of "static sub-classes". Since a model is
self-contained, these (a)symmetries are actually defined by the model
itself.

This paper presents an algorithm capable of automatically extracting the
symmetries inherent to a model, thus allowing its symbolic study by
translating it to WN. The computation starts from the assumption that the
model is entirely symmetric, then examines each component of a net to
deduce the symmetry break it induces.

This translation is transparent to the end-user, and is implemented as a
service for the AMI-Net package. It is particularly adapted to models
containing large value domains, yielding combinatorial gain in the size of
the reachability graph.

Keywords:
well-formed Petri nets; symmetry detection; symbolic model-checking;
partial symmetry.

*Do you need a refined search? Try our search engine
which allows complex field-based queries.*
*Back to the Petri Nets Bibliography*