Statistical Model Checking for Hybrid Petri Nets with Multiple General Transitions

Abstract

The modeling formalism of hybrid Petri nets allows investigating the dependability of e.g. critical infrastructures with hybrid characteristics. Hybrid Petri nets can model random delays with so-called general transitions. Approaches for analyzing such Petri nets are available for models with one or two general transitions, which change the discrete marking of the system by firing only once. We extend the formalism to more general transitions that possibly fire multiple times. This work provides a definition of the probability space for the evolution of hybrid Petri nets over time and presents an efficient approach to discrete-event simulation. Statistical Model Checking techniques are introduced to verify complex properties on hybrid Petri nets. The presented methods are implemented in Java and we show their feasibility in a case study that also serves to validate our results.