Paper Info
Title
Automatic symmetry detection in well-formed nets
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.
Year
DOI
Venue
2003
10.1007/3-540-44919-1_9
ICATPN
Keywords
Field
DocType
symbolic study,symbolic analysis,well-formed nets,well-formed net,automatic symmetry detection,so-called state-space explosion problem,symbolic reachability graph,high-level petri net,inherent size,reachability graph,high-level petri nets,ami-net package,petri net,symmetry breaking,formal verification,complex system
Discrete mathematics,Petri net,Computer science,Symbolic computation,Algorithm,Reachability,Symbolic data analysis,Equivalence class,State space,Formal verification,Computation
Conference
Volume
ISSN
ISBN
2679
0302-9743
3-540-40334-5
Citations 
PageRank 
References 
12
0.96
11
Authors
3
Name
Order
Citations
PageRank
Yann Thierry-Mieg122518.17
Claude Dutheillet28414.29
Isabelle Mounier31316.06