Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Persistent Permutability in Choice Petri Nets

Eike Best, Raymond Devillers

TL;DR

This work investigates persistent permutability in choice Petri nets, focusing on whether finite SPE (permutable finite executions with persistence) entails overall persistence. It establishes SPE⇒persistence for two key net classes: equal-conflict nets and pure dissymmetric nets, thereby confirming Ochmański's conjecture within these families and extending prior FC-net results. The authors introduce patterns and embeddings to characterize non-persistent behavior, define multiple notions of fairness and persistent equivalence (SPE, S̃PE, FPE), and present a plain, pure counterexample showing SPE does not generalize to FPE in all nets. The findings illuminate how specific structural restrictions on choice (EC and DC) guarantee SPE implies persistence, with broader implications for scheduling and concurrency in Petri nets. The work also contrasts finite and infinite sequence fairness regimes and outlines open questions about extending these guarantees beyond the studied classes.

Abstract

Persistence is a strong, global, behavioural property of a Petri net, meaning that no activity can disable a different activity. Persistent permutability is a weaker property, pertaining to individual interleavings of a Petri net and stating that a non-persistent sequence can be permuted into a persistent one. We identify Petri net classes for which persistent permutability already suffices to imply overall persistence. These classes generalise free-choice nets and are related to Petri's concept of ``confusion'', while they are distinguished from each other by diverse restrictions on the choice structure of a net. We prove Ochmanski's conjecture to be correct for these classes.

Persistent Permutability in Choice Petri Nets

TL;DR

This work investigates persistent permutability in choice Petri nets, focusing on whether finite SPE (permutable finite executions with persistence) entails overall persistence. It establishes SPE⇒persistence for two key net classes: equal-conflict nets and pure dissymmetric nets, thereby confirming Ochmański's conjecture within these families and extending prior FC-net results. The authors introduce patterns and embeddings to characterize non-persistent behavior, define multiple notions of fairness and persistent equivalence (SPE, S̃PE, FPE), and present a plain, pure counterexample showing SPE does not generalize to FPE in all nets. The findings illuminate how specific structural restrictions on choice (EC and DC) guarantee SPE implies persistence, with broader implications for scheduling and concurrency in Petri nets. The work also contrasts finite and infinite sequence fairness regimes and outlines open questions about extending these guarantees beyond the studied classes.

Abstract

Persistence is a strong, global, behavioural property of a Petri net, meaning that no activity can disable a different activity. Persistent permutability is a weaker property, pertaining to individual interleavings of a Petri net and stating that a non-persistent sequence can be permuted into a persistent one. We identify Petri net classes for which persistent permutability already suffices to imply overall persistence. These classes generalise free-choice nets and are related to Petri's concept of ``confusion'', while they are distinguished from each other by diverse restrictions on the choice structure of a net. We prove Ochmanski's conjecture to be correct for these classes.
Paper Structure (16 sections, 18 theorems, 20 equations, 22 figures)

This paper contains 16 sections, 18 theorems, 20 equations, 22 figures.

Table of Contents

  1. Introduction
  2. Labelled transition systems and their properties
  3. Petri nets and their reachability graphs
  4. Patterns and embeddings
  5. Persistent sequences
  6. Permutation equivalence
  7. Fairness, SPE, S$\widetilde{\text{P}}$E, FPE, and Ochmański's conjecture
  8. Two Petri net classes satisfying SPE $\Rightarrow$ FPE
  9. Equal conflict Petri nets satisfying S$\widetilde{\text{P}}$E are persistent
  10. Pure DC Petri nets satisfying S$\widetilde{\text{P}}$E are persistent
  11. A plain and pure counterexample to SPE $\Rightarrow$ FPE
  12. Fairness, justice, progress, APE, and JPE
  13. Fairness of finite sequences
  14. Continuous and constant neglecting, weak fairness, progress, APE, and JPE
  15. Concluding remarks
  16. ...and 1 more sections

Key Result

Proposition 3.4

Finite reachability graphs A Petri net $N$ is bounded iff $RG(N)$ is finite. $\square$pn1.prop=0

Figures (22)

  • Figure 1: An LTS $\mathit{TS}_{\ref{['basic-exa.ts']}}$ and a Petri net solution $\mathit{N}_{\ref{['basic-exa.pn']}}$. The net $\mathit{N}_{\ref{['basic-exa.pn']}}$ is plain; pure; safe; and asymmetric choice; but not dissymmetric choice because $({}^\bullet{a}\cap{}^\bullet{b}\neq\emptyset)$, $\neg({}^\bullet{a}\subseteq{}^\bullet{b})$, and $\neg({}^\bullet{b}\subseteq{}^\bullet{a})$; and, a fortiori, not free-choice. It has two deadlocks, $M_6$ and $M_7$.
  • Figure 2: DC excludes the Petri net pattern shown on the left-hand side whereas AC excludes the pattern shown on the right-hand side. An arc with a cross on top means "no such arc".
  • Figure 3: The pattern $\mathit{PT}_{\mathit{nonpers}}=(\{1,2,3\},\{(1,a,2),(1,b,3)\},\{a,b\},\{(2,b)\})$ highlights a violated persistence at state $1$, due to the disabling of $b$ by executing $a$. The set $\{(2,b)\}$ specifies the excluded arrow.
  • Figure 4: An LTS $\mathit{TS}_{\ref{['confuse-exa.ts']}}$ containing the pattern $\mathit{PT}_{\mathit{nonpers}}$, fusing states $2$ and $3$ into $s_1$. The impure, arc-weighted net $\mathit{N}_{\ref{['confuse-exa.pn']}}$ solves $\mathit{TS}_{\ref{['confuse-exa.ts']}}$, and the embedding of $\mathit{PT}_{\mathit{nonpers}}$ into $\mathit{TS}_{\ref{['confuse-exa.ts']}}$ witnesses the non-persistence of $\mathit{N}_{\ref{['confuse-exa.pn']}}$.
  • Figure 5: An LTS $\mathit{TS}_{\ref{['pers-local.ts']}}$ and a Petri net solution $\mathit{N}_{\ref{['pers-local.pn']}}$. The sequence $M_0\xrightarrow{{c}}$ is persistent while the sequences $M_0\xrightarrow{{a}}$ and $M_0\xrightarrow{{b}}$ are not.
  • ...and 17 more figures

Theorems & Definitions (41)

  • Definition 2.1
  • Definition 2.2
  • Definition 3.1
  • Definition 3.2
  • Definition 3.3
  • Proposition 3.4
  • Proposition 3.5
  • Definition 3.6
  • Remark 3.7
  • Example 3.8
  • ...and 31 more