Structural Liveness of Immediate Observation Petri Nets

TL;DR

This work classifies the structural liveness problem ($SLP$) for two Petri-net submodels: immediate observation nets (IO nets) and their branching multi-observation generalization (BIMO nets). It proves $SLP$ is PSPACE-hard for ord-IO nets via a reduction from deterministic linear-bounded automata, and shows $SLP$ lies in $PSPACE$ for the broader BIMO family, with concrete bounds on token counts in places that decisively determine liveliness. The paper introduces key concepts—carriers of markings, relaxed nets, and DL-markings—and leverages them to derive tight upper bounds on live-marking sizes and to establish complexity classifications. The results extend the understanding of liveness verification in restricted Petri-net classes and connect to population protocols and related formalisms, with implications for static analysis and verification of concurrent systems. The combination of hardness proofs and $PSPACE$-membership bounds provides a precise complexity landscape for structural liveness in IO/BIMO nets and their variants.

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.

Figures (1)

• Figure 1: Example of a marked ord-BIMO net.

Theorems & Definitions (11)

• Proposition 2.1
• Remark 2.2
• Remark 2.3
• Proposition 2.4
• Theorem 2.5
• Remark 2.6
• Remark 3.1
• Proposition 3.2: Added tokens can be pasted down to original tokens in ord-IO nets
• Theorem 3.3
• Proposition 4.1: If a transition is dead with ignored places, then it is dead originally