New Canonical Representative Marking Algorithms for Place/Transition-Nets

摘要

Symmetries of a Place/Transition-net can be exploited during the reachability analysis by considering only one representative marking in each orbit induced by the symmetries. In this report, three new algorithms for transforming a marking into a symmetric canonical representative marking are described. All the algorithms depend on the precalculation of a Schreier- Sims representation for the symmetry group of the net in question. The first algorithm uses a black box graph canonizer algorithm to produce a canonical version of the characteristic graph associated with a marking and then derives the canonical representative marking from it. The second algorithm is a backtrack search in the Schreier-Sims representation, pruning the search with the marking in question and its stabilizers found during the search. The third algorithm combines the first and second one by pruning the search in the Schreier-Sims representation with an ordered partition obtained with a standard preprocessing technique applied in graph isomorphism algorithms.