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

Carina Pilch; Arnd Hartmanns; Anne Remke

doi:10.1145/3365365.3382198

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

Carina Pilch, Arnd Hartmanns, Anne Remke

Formal Methods and Tools

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

8 Citations (Scopus)

72 Downloads (Pure)

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 language	English
Title of host publication	HSCC '20
Subtitle of host publication	Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control
Editors	Aaron Ames, Sanjit A. Seshia, Jyotirmoy Deshmukh
Place of Publication	New York, NY
Publisher	Association for Computing Machinery
Number of pages	11
ISBN (Electronic)	978-1-4503-7018-9
DOIs	https://doi.org/10.1145/3365365.3382198
Publication status	Published - 22 Apr 2020
Event	23rd International Conference on Hybrid Systems: Computation and Control, HSCC 2020 - Hilton Sydney, Sydney, Australia Duration: 21 Apr 2020 → 24 Apr 2020 Conference number: 23 https://berkeleylearnverify.github.io/HSCC_2020/

Conference

Conference	23rd International Conference on Hybrid Systems: Computation and Control, HSCC 2020
Abbreviated title	HSCC 2020
Country/Territory	Australia
City	Sydney
Period	21/04/20 → 24/04/20
Internet address	https://berkeleylearnverify.github.io/HSCC_2020/

Keywords

hybrid Petri nets with general transitions
Nondeterminism
Prophetic schedulers
Reachability analysis
Stochastic hybrid systems
22/2 OA procedure

Access to Document

10.1145/3365365.3382198

Pilch-2020-Classic-and-non-prophetic-model-cheFinal published version, 1.2 MBLicence: Taverne

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 Article 10 Association for Computing Machinery. https://doi.org/10.1145/3365365.3382198

@inproceedings{3734b6102f9447f780c500570f339e50,

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.",

keywords = "hybrid Petri nets with general transitions, Nondeterminism, Prophetic schedulers, Reachability analysis, Stochastic hybrid systems, 22/2 OA procedure",

author = "Carina Pilch and Arnd Hartmanns and Anne Remke",

note = "Funding Information: This work was partly supported by NWO VENI grant 639.021.754. Publisher Copyright: {\textcopyright} 2020 ACM.; 23rd International Conference on Hybrid Systems: Computation and Control, HSCC 2020, HSCC 2020 ; Conference date: 21-04-2020 Through 24-04-2020",

year = "2020",

month = apr,

day = "22",

doi = "10.1145/3365365.3382198",

language = "English",

editor = "Aaron Ames and Seshia, {Sanjit A.} and Jyotirmoy Deshmukh",

booktitle = "HSCC '20",

publisher = "Association for Computing Machinery",

address = "United States",

url = "https://berkeleylearnverify.github.io/HSCC_2020/",

}

Pilch, C, Hartmanns, A & Remke, A 2020, Classic and non-prophetic model checking for hybrid Petri nets with stochastic firings. in A Ames, SA Seshia & J Deshmukh (eds), HSCC '20: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control., 10, Association for Computing Machinery, New York, NY, 23rd International Conference on Hybrid Systems: Computation and Control, HSCC 2020, Sydney, New South Wales, Australia, 21/04/20. https://doi.org/10.1145/3365365.3382198

Classic and non-prophetic model checking for hybrid Petri nets with stochastic firings. / Pilch, Carina; Hartmanns, Arnd; Remke, Anne.
HSCC '20: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control. ed. / Aaron Ames; Sanjit A. Seshia; Jyotirmoy Deshmukh. New York, NY: Association for Computing Machinery, 2020. 10.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

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

AU - Pilch, Carina

AU - Hartmanns, Arnd

AU - Remke, Anne

N1 - Conference code: 23

PY - 2020/4/22

Y1 - 2020/4/22

N2 - 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.

AB - 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.

KW - hybrid Petri nets with general transitions

KW - Nondeterminism

KW - Prophetic schedulers

KW - Reachability analysis

KW - Stochastic hybrid systems

KW - 22/2 OA procedure

UR - http://www.scopus.com/inward/record.url?scp=85086526403&partnerID=8YFLogxK

U2 - 10.1145/3365365.3382198

DO - 10.1145/3365365.3382198

M3 - Conference contribution

BT - HSCC '20

A2 - Ames, Aaron

A2 - Seshia, Sanjit A.

A2 - Deshmukh, Jyotirmoy

PB - Association for Computing Machinery

CY - New York, NY

T2 - 23rd International Conference on Hybrid Systems: Computation and Control, HSCC 2020

Y2 - 21 April 2020 through 24 April 2020

ER -

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

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this