State-space reduction in colored PN with linearly constrained domains

Colored Petri Nets (CPN) State-space reduction is nor mally based upon behavioral equivalences or symmetries. Well-Formed Nets (WN) are a CPN flavor retaining expres sive power and allowing the direct construction of a Sym bolic Reachability Graph (SRG), that captures symmetries suitably encoded in the WN syntax. Statically specified symmetries, however, are not effective in many real cases. In this paper a new quotient graph for WN-like models is introduced, that relies upon a simple mapping of color domains into numerical domains, and makes use of linear constraints to perform a sort of symbolic execution. It is compared to a recently presented approach exploiting lo cal symmetries. The model of an asymmetric distributed algorithm is used as running example.