Flatness and complexity of immediate observation petri nets

Mikhail Raskin, Chana Weil-Kennedy, Javier Esparza

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

2 Scopus citations

Abstract

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.

Original languageEnglish
Title of host publication31st International Conference on Concurrency Theory, CONCUR 2020
EditorsIgor Konnov, Laura Kovacs
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages451-4519
Number of pages4069
ISBN (Electronic)9783959771603
DOIs
StatePublished - 1 Aug 2020
Event31st International Conference on Concurrency Theory, CONCUR 2020 - Virtual, Vienna, Austria
Duration: 1 Sep 20204 Sep 2020

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume171
ISSN (Print)1868-8969

Conference

Conference31st International Conference on Concurrency Theory, CONCUR 2020
Country/TerritoryAustria
CityVirtual, Vienna
Period1/09/204/09/20

Keywords

  • Flattability
  • Parameterized Verification
  • Petri Nets
  • Reachability Analysis

Fingerprint

Dive into the research topics of 'Flatness and complexity of immediate observation petri nets'. Together they form a unique fingerprint.

Cite this