Title
Classic and non-prophetic model checking for hybrid Petri nets with stochastic firings
Abstract
Nondeterminism occurs naturally in Petri nets whenever multiple events are enabled at the same time. Traditionally, it is resolved at specification time using probability weights and priorities. In this paper, we focus on model checking for hybrid Petri nets with an arbitrary but finite number of stochastic firings (HPnGs) while preserving the inherent nondeterminism as a first-class modelling and analysis feature. We present two algorithms to compute optimal non-prophetic and prophetic schedulers. The former can be applied to all HPnG models while the latter is only applicable if information on the firing times of general transitions is specifically encoded in the model. Both algorithms make use of recent work on the parametric location tree, which symbolically unfolds the state space of an HPnG. A running example illustrates the approach and confirms the feasibility of the presented algorithm.
Year
DOI
Venue
2020
10.1145/3365365.3382198
HSCC '20: 23rd ACM International Conference on Hybrid Systems: Computation and Control Sydney New South Wales Australia April, 2020
Keywords
DocType
ISBN
Reachability analysis, Stochastic hybrid systems, Hybrid Petri nets with general transitions, Nondeterminism, Prophetic Schedulers
Conference
978-1-4503-7018-9
Citations 
PageRank 
References 
1
0.35
0
Authors
3
Name
Order
Citations
PageRank
Carina Pilch161.44
Arnd Hartmanns228925.97
Anne Remke317523.96