Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets

Arnaldo Cesco, Roberto Gorrieri

TL;DR

The paper proves the decidability of two truly concurrent equivalences on finite bounded Petri nets: (i) strong fully-concurrent bisimilarity and (ii) i-causal-net bisimilarity, a coarser yet resource-aware variant of causal-net bisimilarity. The authors extend Vogler’s ordered marking technique to bounded nets by introducing indexed markings and ordered indexed markings (OIMs), along with their variants, to capture causality and token individuality. They establish equivalences between fc, icn, and their ordered-indexed counterparts (OIM and OIMC), showing that these relations are decidable because the state spaces are finite and candidate relations are enumerable. The approach yields a concrete, net-based decidability framework for truly concurrent behavioral equivalences, with implications for reasoning about resource-aware and causality-respecting system behavior, and it opens avenues for exploring additional conjunctive equivalences in bounded nets.

Abstract

We prove that the well-known (strong) fully-concurrent bisimilarity and the novel i-causal-net bisimilarity, which is a sligtlhy coarser variant of causal-net bisimilarity, are decidable for finite bounded Petri nets. The proofs are based on a generalization of the ordered marking proof technique that Vogler used to demonstrate that (strong) fully-concurrent bisimilarity (or, equivalently, history-preserving bisimilarity) is decidable on finite safe nets.

Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets

TL;DR

The paper proves the decidability of two truly concurrent equivalences on finite bounded Petri nets: (i) strong fully-concurrent bisimilarity and (ii) i-causal-net bisimilarity, a coarser yet resource-aware variant of causal-net bisimilarity. The authors extend Vogler’s ordered marking technique to bounded nets by introducing indexed markings and ordered indexed markings (OIMs), along with their variants, to capture causality and token individuality. They establish equivalences between fc, icn, and their ordered-indexed counterparts (OIM and OIMC), showing that these relations are decidable because the state spaces are finite and candidate relations are enumerable. The approach yields a concrete, net-based decidability framework for truly concurrent behavioral equivalences, with implications for reasoning about resource-aware and causality-respecting system behavior, and it opens avenues for exploring additional conjunctive equivalences in bounded nets.

Abstract

We prove that the well-known (strong) fully-concurrent bisimilarity and the novel i-causal-net bisimilarity, which is a sligtlhy coarser variant of causal-net bisimilarity, are decidable for finite bounded Petri nets. The proofs are based on a generalization of the ordered marking proof technique that Vogler used to demonstrate that (strong) fully-concurrent bisimilarity (or, equivalently, history-preserving bisimilarity) is decidable on finite safe nets.

Paper Structure

This paper contains 12 sections, 15 theorems, 16 equations, 6 figures, 1 table.

Table of Contents

  1. Introduction
  2. Basic Definitions
  3. Causality-based Semantics
  4. Causal Nets and Processes
  5. Causal-net Bisimilarity and Fully-concurrent Bisimilarity
  6. I-causal-net Bisimilarity
  7. Indexed Marking Semantics
  8. Ordered Indexed Marking Semantics
  9. Ordered indexed marking and causality-based semantics
  10. Fully-concurrent Bisimilarity is Decidable
  11. I-causal-net Bisimilarity is Decidable
  12. Conclusion and Future Research

Key Result

Proposition 3.7

Assume that $\pi = (C, \rho)$ is a process of $N(m_0)$ such that $\pi {\hbox{${\:\stackrel{e}{\longrightarrow}\:}$}} \pi' = (C', \rho')$, i.e. $\pi$ moves in one step trough $e$ to $\pi'$. Then, $\forall b \in Max(C) \, , \, \forall b' \in \hbox{$e^{\bullet}$} , \,$ if $\hbox{$^{\bullet}b$} \leq_{\p

Figures (6)

  • Figure 1: A finite P/T net $N$ and two causal nets: $C_1$ corresponds to the maximal process of $N(s_1)$ and $C_2$ corresponds to the maximal process of $N(s_3)$.
  • Figure 2: Two non-cn-bisimilar markings, but with the same causal nets
  • Figure 3: A finite marked P/T net $N$ and three causal nets
  • Figure 4: Execution of the transition labeled by $v$, then of the transition labeled by $u$, on a net with initial marking $m_0 = s_1 \oplus 3s_2$. Tokens to be consumed are in red, generated ones in blue.
  • Figure 5: The causal net of a process and two possible resulting indexed markings starting from the net of Figure \ref{['fig:token-game-1']}(a).
  • ...and 1 more figures

Theorems & Definitions (51)

  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Definition 2.4
  • Definition 2.5
  • Definition 2.6
  • Definition 3.1
  • Definition 3.2
  • Definition 3.3
  • Definition 3.4
  • ...and 41 more