Integrating symmetries and symbolic enabling test for efficient simulation of SWNs

(Stochastic) Colored Petri Nets are a for- malism widely used to specify and analyze distributed discrete-event systems. Determining the set of transi- tion color instances enabled in a given marking is a basic task affecting analysis techniques based on state-space exploration, model-checking, and especially discrete- event simulation (the latter is an interesting alternative when analytical solutions are unfeasible due to state- space explosion). An algebraic approach to enabling test has been recently proposed as kernel for efficient state-space exploration of SWN, a Stochastic CPN fla- vor retaining expressive power. The approach is sym- bolic because it directly manipulates arc functions by means of rewriting rules. What makes interesting the SWN formalism is the ability of exploiting behavioral system’s symmetries, thanks to structured color anno- tations. This paper illustrates in a semi-formal way how the symmetry-based technique typical of SWN can be profitably combined with the SWN symbolic enabling test, giving rise to a fully symbolic simulation kernel. An application example to a workflow model is presented.