English

Structural Liveness of Immediate Observation Petri Nets

Logic in Computer Science 2024-02-14 v4

Abstract

We look in detail at the structural liveness problem (SLP) for subclasses of Petri nets, namely immediate observation nets (IO nets) and their generalized variant called branching immediate multi-observation nets (BIMO nets), that were recently introduced by Esparza, Raskin, and Weil-Kennedy. We show that SLP is PSPACE-hard for IO nets and in PSPACE for BIMO nets. In particular, we discuss the (small) bounds on the token numbers in net places that are decisive for a marking to be (non)live.

Cite

@article{arxiv.2112.15524,
  title  = {Structural Liveness of Immediate Observation Petri Nets},
  author = {Petr Jancar and Jiri Valusek},
  journal= {arXiv preprint arXiv:2112.15524},
  year   = {2024}
}

Comments

Final version

R2 v1 2026-06-24T08:36:56.212Z