Classic and non-prophetic model checking for hybrid Petri nets with stochastic firings

Carina Pilch, Arnd Hartmanns, Anne Remke

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)

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.
Original languageEnglish
Title of host publicationHSCC '20: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control
EditorsAaron Ames, Sanjit A. Seshia, Jyotirmoy Deshmukh
PublisherAssociation for Computing Machinery (ACM)
Number of pages11
ISBN (Electronic)978-1-4503-7018-9
DOIs
Publication statusPublished - Apr 2020
Event23rd International Conference on Hybrid Systems: Computation and Control, HSCC 2020 - Hilton Sydney, Sydney, Australia
Duration: 21 Apr 202024 Apr 2020
Conference number: 23
https://berkeleylearnverify.github.io/HSCC_2020/

Conference

Conference23rd International Conference on Hybrid Systems: Computation and Control, HSCC 2020
Abbreviated titleHSCC 2020
CountryAustralia
CitySydney
Period21/04/2024/04/20
Internet address

Fingerprint Dive into the research topics of 'Classic and non-prophetic model checking for hybrid Petri nets with stochastic firings'. Together they form a unique fingerprint.

  • Cite this

    Pilch, C., Hartmanns, A., & Remke, A. (2020). Classic and non-prophetic model checking for hybrid Petri nets with stochastic firings. In A. Ames, S. A. Seshia, & J. Deshmukh (Eds.), HSCC '20: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control [10] Association for Computing Machinery (ACM). https://doi.org/10.1145/3365365.3382198