Constraint-based state space reduction in colored PN

State-space reduction techniques for Colored Petri Nets (CPN) are normally based on detection of behavioral equivalences or symmetries. Well-Formed Nets (WN) are an interesting CPN flavor with the same expressive power as CPN: WNs allow the direct construction of the Symbolic Reachability Graph (SRG), a quotient graph that captures symmetries suitably encoded in the WN color sets, holding 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 one exploiting local symmetries. The model of an asymmetric distributed algorithm is used as comparison term.