TY - GEN
T1 - Flatness and complexity of immediate observation petri nets
AU - Raskin, Mikhail
AU - Weil-Kennedy, Chana
AU - Esparza, Javier
N1 - Publisher Copyright:
© Mikhail Raskin, Chana Weil-Kennedy, and Javier Esparza; licensed under Creative Commons License CC-BY 31st International Conference on Concurrency Theory (CONCUR 2020).
PY - 2020/8/1
Y1 - 2020/8/1
N2 - In a previous paper we introduced immediate observation (IO) Petri nets, a class of interest in the study of population protocols and enzymatic chemical networks. In the first part of this paper we show that IO nets are globally flat, and so their safety properties can be checked by efficient symbolic model checking tools using acceleration techniques, like FAST. In the second part we study Branching IO nets (BIO nets), whose transitions can create tokens. BIO nets extend both IO nets and communication-free nets, also called BPP nets, a widely studied class. We show that, while BIO nets are no longer globally flat, and their sets of reachable markings may be non-semilinear, they are still locally flat. As a consequence, the coverability and reachability problem for BIO nets, and even a certain set-parameterized version of them, are in PSPACE. This makes BIO nets the first natural net class with non-semilinear reachability relation for which the reachability problem is provably simpler than for general Petri nets.
AB - In a previous paper we introduced immediate observation (IO) Petri nets, a class of interest in the study of population protocols and enzymatic chemical networks. In the first part of this paper we show that IO nets are globally flat, and so their safety properties can be checked by efficient symbolic model checking tools using acceleration techniques, like FAST. In the second part we study Branching IO nets (BIO nets), whose transitions can create tokens. BIO nets extend both IO nets and communication-free nets, also called BPP nets, a widely studied class. We show that, while BIO nets are no longer globally flat, and their sets of reachable markings may be non-semilinear, they are still locally flat. As a consequence, the coverability and reachability problem for BIO nets, and even a certain set-parameterized version of them, are in PSPACE. This makes BIO nets the first natural net class with non-semilinear reachability relation for which the reachability problem is provably simpler than for general Petri nets.
KW - Flattability
KW - Parameterized Verification
KW - Petri Nets
KW - Reachability Analysis
UR - http://www.scopus.com/inward/record.url?scp=85091590828&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.CONCUR.2020.45
DO - 10.4230/LIPIcs.CONCUR.2020.45
M3 - Conference contribution
AN - SCOPUS:85091590828
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 451
EP - 4519
BT - 31st International Conference on Concurrency Theory, CONCUR 2020
A2 - Konnov, Igor
A2 - Kovacs, Laura
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 31st International Conference on Concurrency Theory, CONCUR 2020
Y2 - 1 September 2020 through 4 September 2020
ER -