Exploiting Place Invariants in Condensed State Space Construction for Coloured Petri Nets

摘要

The symmetry method exploits the symmetry present in many concurrent systems to alleviate the state explosion problem. This is done by constructing a condensed state space in which the nodes represent equivalence classes of markings. During the construction of a condensed state space, it is necessary to repeatedly determine whether markings are symmetric. This is time expensive due to the apparent complexity of the orbit problem. The contribution of this paper is to show how place invariants can be exploited to consider only a subset of the places when determining whether two markings are symmetric. This can be used to speedup the computation of condensed state spaces.