2026-08-03T02:56:32Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10949 2024-03-06T10:46:53Z ddc:004 open_access

Petri Net Reachability Problem (Invited Talk) Leroux, Jérôme Petri net Reachability problem Formal verification Concurrency Petri nets, also known as vector addition systems, are a long established model of concurrency with extensive applications in modelling and analysis of hardware, software and database systems, as well as chemical, biological and business processes. The central algorithmic problem for Petri nets is reachability: whether from the given initial configuration there exists a sequence of valid execution steps that reaches the given final configuration. The complexity of the problem has remained unsettled since the 1960s, and it is one of the most prominent open questions in the theory of verification. In this presentation, we overview decidability and complexity results over the last fifty years about the Petri net reachability problem. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jérôme Leroux 2019 Is Part Of LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2019.5 urn:nbn:de:0030-drops-109493 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.5 eng https://creativecommons.org/licenses/by/3.0/legalcode