Algebraic framework for efficient simulation of SWN

An algebraic calculus recently introduced is the kernel for the implementation of several algorithms for the analysis of (Stochastic) Colored Petri Nets (CPN) taking advantage of structural considerations. In this paper a recurring task in several CPN analysis techniques is considered, that consists in finding the set of transition color instances enabled in a given marking. This operation affects not only reachability graph construction, but also model-checking, and especially discrete-event simulation, which is an interesting alternative when analytical solutions are unfeasible due to state-space explosion. Using an extension of the calculus it is possible to formally express the set of transition instances enabled in a given marking as a function of the marking itself.