Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Structural Liveness of Conservative Petri Nets

Petr Jančar, Jérôme Leroux, Jiří Valůšek

TL;DR

It is shown that for structurally live conservative nets the values of the least live markings are at most double exponential in the size of the nets, which entails the EXPSPACE-completeness of structural liveness for conservative Petri nets; the complexity of the general case remains unclear.

Abstract

We show that the EXPSPACE-hardness result for structural liveness of Petri nets [Jancar and Purser, 2019] holds even for a simple subclass of conservative nets. As the main result we then show that for structurally live conservative nets the values of the least live markings are at most double exponential in the size of the nets, which entails the EXPSPACE-completeness of structural liveness for conservative Petri nets; the complexity of the general case remains unclear. As a proof ingredient with a potential of wider applicability, we present an extension of the known results bounding the smallest integer solutions of boolean combinations of linear (in)equations and divisibility constraints.

Structural Liveness of Conservative Petri Nets

TL;DR

It is shown that for structurally live conservative nets the values of the least live markings are at most double exponential in the size of the nets, which entails the EXPSPACE-completeness of structural liveness for conservative Petri nets; the complexity of the general case remains unclear.

Abstract

We show that the EXPSPACE-hardness result for structural liveness of Petri nets [Jancar and Purser, 2019] holds even for a simple subclass of conservative nets. As the main result we then show that for structurally live conservative nets the values of the least live markings are at most double exponential in the size of the nets, which entails the EXPSPACE-completeness of structural liveness for conservative Petri nets; the complexity of the general case remains unclear. As a proof ingredient with a potential of wider applicability, we present an extension of the known results bounding the smallest integer solutions of boolean combinations of linear (in)equations and divisibility constraints.

Paper Structure

This paper contains 25 sections, 28 theorems, 11 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Basic Definitions, and Results
  3. Petri Nets.
  4. Linear Systems.
  5. Linear Systems for Subgroups of $\mathbb{Z}^d$.
  6. RB-functions.
  7. Upper Bound (Proof of Theorem \ref{['th:upper']})
  8. Convention on RB-functions.
  9. Convention on using "small" and "large".
  10. Overview of the proof.
  11. Virtual reachability in reversible nets
  12. Petri nets with states (PNSs)
  13. Petri Nets with States (PNSs).
  14. Reversibility of PNSs, and Restricted PNSs.
  15. Proper PNSs.
  16. ...and 10 more sections

Key Result

lemma thmcounterlemma

Let $M=\{x\in\mathbb{N}^n \mid Bx=\hbox{\boldmath$0$}\}$ where $B$ is an $m\times n$ matrix over $\mathbb{Z}$. Then $X=\min_{\leq}(M\smallsetminus\{\mathbf{0}\})$ is a finite set such that $M=X^*$. Moreover the following bound holds, where $r=\operatorname{rank}(B)$:

Figures (4)

  • Figure 1: The net $A_1$ on the left is conservative (as evidenced by the weight vector $(1,1,1,2,1)$) and structurally live; $x_0=(1,0,1,0,2)$ is a live configuration, since there is the only (infinite) execution $(1,0,1,0,2) \xrightarrow{a_1} (0,1,2,0,1) \xrightarrow{a_3} (0,1,0,1,1) \xrightarrow{a_2} (1,0,0,1,1) \xrightarrow{a_4} (1,0,1,0,2)\xrightarrow{a_1}\cdots$ from $x_0$. We can verify that if a configuration $x$ of $A_1$ is live, then $x(1)+x(2)>0 \land x(3)+x(4)>0 \land x(5)>0$; on the other hand, if $(x(3) > 0 \land x(4) > 0) \lor x(1) \geq 2 \lor x(2) \geq 2 \lor x(3) \geq 3 \lor x(4) \geq 2$, then $x$ is non-live. Thus, if $x$ is live, then $x(i)< 3$ for all $i\in[1,4]$. The net $A_2$ on the right is the restriction $A_1{_{| \{1,2,3,4\}}}$; $A_2$ is not conservative, since $\Delta(a_1a_2)=(0,0,1,0)$. Since $A_1$ is reversible, $A_2$ is also reversible.
  • Figure 2: Illustration for the proof of Lemma \ref{['lem:foneftwogen']}.
  • Figure 3: Transformation of the pair $(a_-,a_+)$, $(a_+,a_-)$ where $||a_-||_1 = ||a_+||_1 = 3$.
  • Figure 4: Construction in the proof of Lemma \ref{['lem:PPSCtoSLP']}.

Theorems & Definitions (46)

  • lemma thmcounterlemma: DBLP:conf/rta/Pottier91
  • theorem thmcountertheorem
  • theorem thmcountertheorem
  • corollary thmcountercorollary
  • proof
  • theorem thmcountertheorem
  • corollary thmcountercorollary
  • proof
  • proposition thmcounterproposition: Finite bottom SCCs, and reversibility
  • proof
  • ...and 36 more