TY - GEN
T1 - Parameterized Analysis of Immediate Observation Petri Nets
AU - Esparza, Javier
AU - Raskin, Mikhail
AU - Weil-Kennedy, Chana
N1 - Publisher Copyright:
© Springer Nature Switzerland AG 2019.
PY - 2019
Y1 - 2019
N2 - We introduce immediate observation Petri nets, a class of interest in the study of population protocols (a model of distributed computation), and enzymatic chemical networks. In these areas, relevant analysis questions translate into parameterized Petri net problems: whether an infinite set of Petri nets with the same underlying net, but different initial markings, satisfy a given property. We study the parameterized reachability, coverability, and liveness problems for immediate observation Petri nets. We show that all three problems are in PSPACE for infinite sets of initial markings defined by counting constraints, a class sufficiently rich for the intended application. This is remarkable, since the problems are already PSPACE -hard when the set of markings is a singleton, i.e., in the non-parameterized case. We use these results to prove that the correctness problem for immediate observation population protocols is PSPACE -complete, answering a question left open in a previous paper.
AB - We introduce immediate observation Petri nets, a class of interest in the study of population protocols (a model of distributed computation), and enzymatic chemical networks. In these areas, relevant analysis questions translate into parameterized Petri net problems: whether an infinite set of Petri nets with the same underlying net, but different initial markings, satisfy a given property. We study the parameterized reachability, coverability, and liveness problems for immediate observation Petri nets. We show that all three problems are in PSPACE for infinite sets of initial markings defined by counting constraints, a class sufficiently rich for the intended application. This is remarkable, since the problems are already PSPACE -hard when the set of markings is a singleton, i.e., in the non-parameterized case. We use these results to prove that the correctness problem for immediate observation population protocols is PSPACE -complete, answering a question left open in a previous paper.
KW - Parameterized verification
KW - Petri nets
KW - Population protocols
KW - Reachability analysis
UR - http://www.scopus.com/inward/record.url?scp=85067807621&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-21571-2_20
DO - 10.1007/978-3-030-21571-2_20
M3 - Conference contribution
AN - SCOPUS:85067807621
SN - 9783030215705
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 365
EP - 385
BT - Application and Theory of Petri Nets and Concurrency - 40th International Conference, PETRI NETS 2019, Proceedings
A2 - Donatelli, Susanna
A2 - Haar, Stefan
PB - Springer Verlag
T2 - 40th International Conference on Application and Theory of Petri Nets and Concurrency, Petri Nets 2019
Y2 - 23 June 2019 through 28 June 2019
ER -