Abstract

Generalized Stochastic Petri Nets (GSPNs) are a well-known modelling formalism to compute dependability and performance of distributed systems. GSPNs are translated to Continuous Time Markov Chains (CTMCs)for their analysis, which means they can not support non-determinism. Conflicts and confusion are resolved by specifying priorities and weights for each transition, which is not desirable in all cases.

We define a more expressive and general Non-Deterministic GSPN (ND-GSPN). ND-GSPNs support the weights and priorities and additionally introduce the use of non-determinism. This means conflicts between transitions do not necessarily have to be resolved any more. ND-GSPNs also include reset, weighted inhibitor and probabilistic arcs. Probabilistic arcs make it is possible to define probability more local, because they make the result of a transition probabilistically distributed. We express the ND-GSPN in terms of the more general Markov Automaton (MA).An MA combines probability, exponentially distributed leave rates and non-determinism and is therefore suited to express the semantics of ND-GSPNs.

The Petri Net Markup Language (PNML) is an ISO/IEC 15909 standard, which can be used to specify Petri Nets. We define how the PNML for ND-GSPNs should look like. MAs can be specified in the Markov Automaton Process Algebra (MAPA), which is used as input for the tool SCOOP. SCOOP automatically reduces its models and can export the state space directly to a model-checker. The IMCA model-checker can be used to check an MA for time-bounded reachability, unbounded reachability, expected time and long run averages. 
We implemented the translation from ND-GSPNs in PNML to MAPA in the tool GEMMA. This means we can specify an ND-GSPN in PNML and translate it to MAPA. SCOOP can then reduce this MAPA model and generate the MA, which can be checked with the IMCA model-checker.

References

1. Timmer, M. (2011) SCOOP: A Tool for SymboliC Optimisations Of Probabilistic Processes. In: Proceedings of the 8th International Conference on Quantitative Evaluation of SysTems, QEST 2011, 5-8 Sep 2011, Aachen, Germany. IEEE Computer Society. (Digital version available here)
2. SCOOP (Digital version available here)

Additional Resources

1. The paper