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