Computer Performance Engineering

Hybrid Petri nets have been extended with random variables to model stochastic time delays. This restricted class of stochastic hybrid systems has successfully been used to model critical infrastructures like water sewage systems and smart home energy storage and control. The logic STL has been proposed to formulate properties, which can automatically be model checked for Hybrid Petri nets. Model checking requires to first build the underlying state space and then relies on geometric operations on convex state sets which symbolically represent sets of states with similar properties. After the satisfaction sets are computed a final integration step is needed to compute the probability that a specific STL formula holds. This paper provides an overview on the state-of-the-art in model checking Hybrid Petri nets, featuring a newly released tool, which performs full-fledged STL model checking efficiently for Hybrid Petri nets with a finite but arbitrary number of random variables.