A semantics for every GSPN

Abstract

Generalised Stochastic Petri Nets (GSPNs) are a popular modelling formalism for performance and dependability analysis. Their semantics is traditionally associated to continuous-time Markov chains (CTMCs), enabling the use of standard CTMC analysis algorithms and software tools. Due to ambiguities in the semantic interpretation of confused GSPNs, this analysis strand is however restricted to nets that do not exhibit non-determinism, the so-called well-defined nets. This paper defines a simple semantics for every GSPN. No restrictions are imposed on the presence of confusions. Immediate transitions may be weighted but are not required to be. Cycles of immediate transitions are admitted too. The semantics is defined using a non-deterministic variant of CTMCs, referred to as Markov automata. We prove that for well-defined bounded nets, our semantics is weak bisimulation equivalent to the existing CTMC semantics. Finally, we briefly indicate how every bounded GSPN can be quantitatively assessed. © 2013 Springer-Verlag.