Finite symbolic reachability graphs for high-level Petri nets

The construction of reachability graphs (rg) is one of the most useful techniques to analyse the properties of concurrent systems modelled by Petri nets. Such a graph describes all the possible behaviours of the system, and its construction is straightforward. When high-level Petri nets are under consideration, the size of the graph most often is infinite or large. The reason for this combinatory explosion is twofold: first, we have the explosion due to the interleaving of traces which is usual in models of concurrency; the second explosion results from the token identity since each transition occurrence is characterized by the transition and by the tokens involved in this occurrence. Then, the reachability graph of a bounded net may be infinite, if the domains of tokens are infinite. Symbolic reachability graphs (srg) have been introduced to cope with the latter cause of explosion. By exploiting the symmetries of the net, they are more reduced than the whole reachability graph. This paper introduces a general definition of symbolic reachability graphs. This leads to the introduction of various finite symbolic reachability graphs and to their construction. Two instances of such symbolic reachability graphs are defined. Moreover, a criterion for these two srg to be finite is given together with computation algorithms.