Abstract (EN)

Taking advantage of the symmetries of a system is an efficient way to cope with the combinatory explosion involved by the verification process. Whereas numerous algorithms and tools efficiently deal with the verification 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 first 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.