Colored Petri nets state-space reduction via symbolic execution
Lorenzo Capra · 2005
State-space reduction techniques for distributed discrete-event systems are normally based on detection of behavioral equivalences or symmetries. Well-formed nets (WN) are a colored Petri net flavor allowing the direct construction of a quotient graph, the symbolic reachability graph (SRG), that captures symmetries suitably encoded in the WN color annotations, and holds the same information as the ordinary reachability graph. Like all those approaches based on static (global) symmetries, however the SRG is not effective in many real cases. In this paper a new quotient graph for colored PNs matching an extended WN-like syntax is introduced. The technique, which relies on a simple mapping of color domains into numerical domains, makes use of linear constraints to perform a sort of symbolic execution. We compare it with a recently presented approach exploiting local symmetries. The model of an asymmetric distributed algorithm is used as comparison term.