loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'05)
Colored Petri Nets State-Space Reduction via Symbolic Execution
Timisoara, Romania
September 25-September 29
ISBN: 0-7695-2453-2
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.
Index Terms:
High-Level Petri Nets, quotient graphs, symmetries, linear constraints
Citation:
Lorenzo Capra, "Colored Petri Nets State-Space Reduction via Symbolic Execution," synasc, pp.231-238, Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'05), 2005
Usage of this product signifies your acceptance of the Terms of Use.