Exploiting Partial Symmetries in Well-formed nets for the Reachability and the Linear Time Model Checking Problems
Baarir, Souheib; Haddad, Serge; Ilié, Jean-Michel (2005), Exploiting Partial Symmetries in Well-formed nets for the Reachability and the Linear Time Model Checking Problems, in Carré-Ménétrier, Véronique; Cao, Xi Ren; Zaytoon, Janan, Discrete Event Systems 2004., Elsevier, p. 223-228
TypeCommunication / Conférence
Conference title7th IFAC Workshop on Discrete Event Systems (WODES'04)
Book titleDiscrete Event Systems 2004.
Book authorCarré-Ménétrier, Véronique; Cao, Xi Ren; Zaytoon, Janan
Number of pages484
MetadataShow full item record
Abstract (EN)Taking advantage of the symmetries of a system is an efficient way to cope with the combinatory explosion involved by the veriﬁcation process. Whereas numerous algorithms and tools efficiently deal with the veriﬁcation of a symmetrical formula on a symmetrical model, the management of partial symmetries is still an open research topic. In this work, we present the design and the evaluation of two methods applicable on coloured Petri nets. These two methods are extensions of the symbolic reachability graph construction for the well- formed Petri nets. The ﬁrst algorithm, called the extended symbolic reachability graph construction, tackles the reachability problem. The second one, called the symbolic synchronized product, checks a partially symmetric linear time formula on a net. The evaluations show that these two methods outperform the previous approaches dealing with partial symmetries. Furthermore they are complementary ones since the former while being less general gives better results than the latter when applied to the reachability problem.
Subjects / KeywordsColoured Petri Net; Well-Formed Petri Net; Partial Symmetry; Symbolic Reachability Graph
Showing items related by title and author.