Nov 13, 2012: Rob Bamberg: Non-Deterministic Generalised Stochastic Petri Nets: Modelling and Analysis

November 13, 2012Non-Deterministic Generalised Stochastic Petri Nets: Modelling and Analysis
Room: Zi 5126Rob Bamberg

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.