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, dans Carré-Ménétrier, Véronique; Cao, Xi Ren; Zaytoon, Janan, Discrete Event Systems 2004., Elsevier, p. 223-228
TypeCommunication / Conférence
Titre du colloque7th IFAC Workshop on Discrete Event Systems (WODES'04)
Date du colloque2004-09
Ville du colloqueReims
Pays du colloqueFrance
Titre de l'ouvrageDiscrete Event Systems 2004.
Auteurs de l’ouvrageCarré-Ménétrier, Véronique; Cao, Xi Ren; Zaytoon, Janan
Nombre de pages484
MétadonnéesAfficher la notice complète
Résumé (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.
Mots-clésColoured Petri Net; Well-Formed Petri Net; Partial Symmetry; Symbolic Reachability Graph
Affichage des éléments liés par titre et auteur.