Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Lower Bound on Conservative Elementary Object Systems Coverability

Francesco Di Cosmo, Soumodev Mal, Tephilla Prince

TL;DR

The paper addresses the complexity of coverability for conservative Elementary Object Systems (cEOS), a data-rich extension of Petri nets where tokens carry internal nets. It introduces a polynomial reduction by encoding νPNs into cEOS via a simulator construction, mapping νPN configurations to nested tokens and simulating transitions with synchronized events. The main result is that cEOS coverability is $F_{\omega2}$-hard (and non-Primitive Recursive), establishing a strong lower bound and implying substantial computational difficulty for this model. This work clarifies the limits of cEOS as a framework for analyzing data-bearing Petri nets and motivates further exploration of the connections between cEOS, νPN, and data nets.

Abstract

Elementary Object Systems (EOS) are a form of Petri Net (PN) where tokens carry internal PN. This model has been recently proposed for analysis of robustness of Multi Agent Systems. While EOS reachability is known to be undecidable, the decidability of coverability of its conservative fragment (where the type of internal PN cannot be completely deleted and, thus, is conserved) was proved a decade ago, no study charted its complexity. Here, we take a first step in this direction, by showing how to encode $ν$PNs, a well studied form of PN enriched with data, into conservative EOS (cEOS). This yields a non-Primitive Recursive, $F_{\omega2}$ lower-bound on cEOS coverability.

A Lower Bound on Conservative Elementary Object Systems Coverability

TL;DR

The paper addresses the complexity of coverability for conservative Elementary Object Systems (cEOS), a data-rich extension of Petri nets where tokens carry internal nets. It introduces a polynomial reduction by encoding νPNs into cEOS via a simulator construction, mapping νPN configurations to nested tokens and simulating transitions with synchronized events. The main result is that cEOS coverability is -hard (and non-Primitive Recursive), establishing a strong lower bound and implying substantial computational difficulty for this model. This work clarifies the limits of cEOS as a framework for analyzing data-bearing Petri nets and motivates further exploration of the connections between cEOS, νPN, and data nets.

Abstract

Elementary Object Systems (EOS) are a form of Petri Net (PN) where tokens carry internal PN. This model has been recently proposed for analysis of robustness of Multi Agent Systems. While EOS reachability is known to be undecidable, the decidability of coverability of its conservative fragment (where the type of internal PN cannot be completely deleted and, thus, is conserved) was proved a decade ago, no study charted its complexity. Here, we take a first step in this direction, by showing how to encode PNs, a well studied form of PN enriched with data, into conservative EOS (cEOS). This yields a non-Primitive Recursive, lower-bound on cEOS coverability.

Paper Structure

This paper contains 7 sections, 2 theorems, 3 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Binary Relations and Multisets
  3. Petri Nets
  4. Elementary Object Systems
  5. nuPNs
  6. Complexity Lower Bound
  7. Conclusions

Key Result

lemma 1

$M\rightarrow^t M'$ in $\mathcal{D}$ if only if $\overline{M}\rightarrow^{\sigma} \overline{M'}$ in $\mathfrak{E}$ for some minimal run $\sigma$ of $\mathfrak{E}$.

Figures (1)

  • Figure 1: The part of $\mathfrak{E}$ dedicated to the simulation of a transition $t$ of $\mathcal{D}$ such that $\text{Var}(t)=\{x_1,\dots,x_n,\nu\}$. If $\nu\notin\text{Var}(t)$, then, $\text{select}^t_\nu$, $t^\text{select}_\nu$, $t_\nu^\text{run}$, and $t_{\nu}^\text{fire}$ have to be dropped, and $\hat{F}(t^\text{select}_x,t_{x_1}^\text{run})=1$, $\hat{F}(t^\text{select}_x,t_{x_n}^\text{run})=1$, and $\hat{F}(t^\text{report},t^\text{done})=n$ has to be set.

Theorems & Definitions (11)

  • definition 1: EOS
  • definition 2: Nested Markings
  • definition 3: Projection Operators
  • definition 4: Enabledness Condition
  • definition 5: cEOS
  • definition 6
  • definition 7
  • definition 8
  • lemma 1
  • proof
  • ...and 1 more