State-Space Reduction in Colored PN with Linearly Constrained Domains

L. Capra (Italy)


Colored PNs, statespace reduction, linear constraints.


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.

Important Links:

Go Back