In: Proceedings of the IEEE International Computer Science Conference, APSEC'97, Hong Kong, pages 111-126. December 1997.
Abstract: The reachability graph is one of the useful method to analyse the properties of a Petri net; its construction is straightforward and the graph describes all the possible behaviours of the system. When we consider high-level Petri nets, the size of the graph can be very large or infinite, even for bounded nets, due to the domains of tokens handled by the system. The symbolic reachability graphs is more tractable than the full graph, because it reduces the combinatory explosion problem. Such a reduction is obtained by exploiting the symmetries of the net. This paper presents a more general definition of intrinsic symmetries and of symbolic reachability graphs, leading to the introduction of the quasi-minimal and minimal symbolic reachability graphs. Algorithms are given for computing these new classes of symbolic reachability graphs.