The Best of Both Worlds: Analytically-Guided Simulation of HPnGs for Optimal Reachability

Niehage, Mathis; Remke, Anne

Zusammenfassung

Efficient reachability analysis, as well as statistical model checking have been proposed for the evaluation of Hybrid Petri nets with general transitions (HPnG). Both have different (dis-)advantages. The performance of statistical simulation suffers in large models and the number of required simulation runs to achieve a relatively small confidence interval increases considerably. The approach introduced for analytical reachability analysis of HPnGs however, becomes infeasible for a large number of random variables. To overcome these limitations, this paper applies statistical simulation for optimal reachability defined as until property in Stochastic Time Logic to a pre-computed symbolic state-space representation of HPnGs, i.e., the Parametric Location Tree (PLT), which has previously been used for model checking HPnGs. A case study on a water tank model shows the feasiblity of the approach and illustrates its advantages w.r.t. the original simulation and analysis approaches.