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 toWN. 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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
CPN-AMI: a Petri net based CASE environment. url: http://www-src.lip6.fr/cpn-ami.
G. Chiola, C. Dutheillet, G. Franceschinis, and S. Haddad. Stochastic well-formed colored nets and symmetric modeling applications. IEEE Transactions on Computers, 42(11):1343–1360, 1993.
G. Chiola, C. Dutheillet, G. Franceschinis, and S. Haddad. A symbolic reachability graph for coloured Petri nets. Theoretical Computer Science, 176(1–2):39–65, 1997.
G. Chiola and G. Franceschinis. Structural colour simplification in Well-Formed coloured nets. In Proc. 4th Int. Workshop on Petri Nets and Performance Models, pages 144–153, Melbourne, Australia, December 1991.
C.N. Ip and D.L. Dill. Better verification through symmetry. In D. Agnew, L. Claesen, and R. Camposano, editors, Computer Hardware Description Languages and their Applications, pages 87–100, Ottawa, Canada, 1993. Elsevier Science Publishers B.V., Amsterdam, Netherland.
D. Regep, Y. Thierry-Mieg, F. Gilliers, and F. Kordon. Modélisation et vérification de systèmes répartis: une approche intégrée avec L f P. In AFADL 2003, Approches Formelles dans l’Assistance au Développement de Logiciels. INRIA, proceedings, January 2003.
M. Doche, I. Vernier-Mounier, and F. Kordon. A modular approach to the specification and validation of an electrical flight control system. In FME’01, Formal Methods for Increasing Software Productivity, pages 590–610, Berlin, Germany, March 2001. Springer Verlag.
GreatSPN: GRaphical Editor, Analyzer for Timed, and Stochastic Petri Nets. url: http://www.di.unito.it/~greatspn/.
J-C. Fernandez, C. Jard, T. Jeron, and C. Viho. An experiment in automatic generation of test suites for protocols with verification technology. Science of Computer Programming, 29(1–2):123–146, 1997.
Serge Haddad, Jean Michel Ilie, M. Taghelit, and B. Zouari. Symbolic reachability graph and partial symmetries. In Application and Theory of Petri Nets, pages 238–257, 1995.
D. Poitrenaud and J-F. Pradat-Peyre. Pre-and post-agglomeration for ltl model-checking. Lecture Notes in Computer Science, 1825:387–408, 2000.
D. Regep and F. Kordon. L f P: a specification language for rapid prototyping of concurrent systems. In 12th IEEE International Workshop on Rapid System Prototyping, June 2001.
V. Rusu, L. du Bousquet, and T. Jéron. An approach to symbolic test generation. In 2nd International Workshop on Integrated Formal Method (IFM’00), number 1945 in LNCS, pages 338–357, Dagstuhl, Germany, 2000. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Thierry-Mieg, Y., Dutheillet, C., Mounier, I. (2003). Automatic Symmetry Detection in Well-Formed Nets. In: van der Aalst, W.M.P., Best, E. (eds) Applications and Theory of Petri Nets 2003. ICATPN 2003. Lecture Notes in Computer Science, vol 2679. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44919-1_9
Download citation
DOI: https://doi.org/10.1007/3-540-44919-1_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40334-0
Online ISBN: 978-3-540-44919-5
eBook Packages: Springer Book Archive