New Canonical Representative Marking Algorithms for Place/Transition-Nets

摘要

Symmetries of a Place/Transition-net can be exploited during the state space analysis by considering only one representative marking in each orbit induced by the symmetries. This paper describes two new algorithms for the core problem of transforming a marking into an equivalent, canonical representative marking. The algorithms are based on a backtrack search through all the symmetries of the net. The first algorithm prunes the search with the marking in question and its stabilizers that are found during the search. The second algorithm first applies a standard preprocessing technique in graph isomorphism algorithms to obtain an ordered partition of the net elements in a symmetry-respecting way. The partition is then used to further prune the search through the symmetries. The efficiency of the proposed algorithms is experimentally evaluated. The results show that the new algorithms usually outperform the previous ones implemented in the LoLA tool.