Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'05) (2005)
Sept. 25, 2005 to Sept. 29, 2005
Lorenzo Capra , Universitá degli studi di Milano
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.
High-Level Petri Nets, quotient graphs, symmetries, linear constraints
L. Capra, "Colored Petri Nets State-Space Reduction via Symbolic Execution," Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'05)(SYNASC), Timisoara, Romania, 2005, pp. 231-238.