Michael Blondin ; Javier Esparza - Separators in Continuous Petri Nets

lmcs:10017 - Logical Methods in Computer Science, February 21, 2024, Volume 20, Issue 1 - https://doi.org/10.46298/lmcs-20(1:15)2024
Separators in Continuous Petri NetsArticle

Authors: Michael Blondin ORCID; Javier Esparza

    Leroux has proved that unreachability in Petri nets can be witnessed by a Presburger separator, i.e. if a marking $\vec{m}_\text{src}$ cannot reach a marking $\vec{m}_\text{tgt}$, then there is a formula $\varphi$ of Presburger arithmetic such that: $\varphi(\vec{m}_\text{src})$ holds; $\varphi$ is forward invariant, i.e., $\varphi(\vec{m})$ and $\vec{m} \rightarrow \vec{m}'$ imply $\varphi(\vec{m}'$); and $\neg \varphi(\vec{m}_\text{tgt})$ holds. While these separators could be used as explanations and as formal certificates of unreachability, this has not yet been the case due to their worst-case size, which is at least Ackermannian, and the complexity of checking that a formula is a separator, which is at least exponential (in the formula size). We show that, in continuous Petri nets, these two problems can be overcome. We introduce locally closed separators, and prove that: (a) unreachability can be witnessed by a locally closed separator computable in polynomial time; (b) checking whether a formula is a locally closed separator is in NC (so, simpler than unreachability, which is P-complete). We further consider the more general problem of (existential) set-to-set reachability, where two sets of markings are given as convex polytopes. We show that, while our approach does not extend directly, we can efficiently certify unreachability via an altered Petri net.

    Volume: Volume 20, Issue 1
    Published on: February 21, 2024
    Accepted on: December 12, 2023
    Submitted on: September 8, 2022
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Formal Languages and Automata Theory
      Source : OpenAIRE Graph
    • Parametrized Verification and Synthesis; Funder: European Commission; Code: 787367
    • Funder: Natural Sciences and Engineering Research Council of Canada

    Consultation statistics

    This page has been seen 593 times.
    This article's PDF has been downloaded 245 times.