Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the Home-Space Problem for Petri Nets and its Ackermannian Complexity

Petr Jančar, Jérôme Leroux

TL;DR

The paper resolves the semilinear home-space problem for Petri nets by establishing a duality with non-reachability cores, enabling a reduction to reachability and proving decidability with Ackermannian complexity. It shows that for any Petri net and semilinear set $H$, one can effectively compute a semilinear non-reachability core that characterizes when $H$ fails to be a home-space for any $X$, yielding an Ackermannian decision procedure. Additionally, the authors prove that minimal reachable configurations can be computed in Ackermannian time and that inductive semilinear non-reachability cores exist for semilinear sets, enabling constructive witnesses for both positive and negative home-space instances. The results place the semilinear home-space problem at the decidability/complexity boundary and provide practical machinery (cores, inductive invariants, and witnesses) for analyzing reachability and invariance in Petri nets.

Abstract

A set of configurations $H$ is a home-space for a set of configurations $X$ of aPetri net if every configuration reachable from (any configuration in) $X$ can reach (some configuration in) $H$. The semilinear home-space problem for Petri nets asks, given a Petri net and semilinear sets of configurations $X$, $H$, if $H$ is a home-space for $X$. In 1989, David de Frutos Escrig and Colette Johnen proved that the problem is decidable when $X$ is a singleton and $H$ is a finite union of linear sets with the same periods. In this paper, we show that the general (semilinear) problem is decidable. This result is obtained by proving a duality between the reachability problem and the non-home-space problem. In particular, we prove that for any Petri net and any semilinear set of configurations $H$ we can effectively compute a semilinear set $C$ of configurations, called a non-reachability core for $H$, such that for every set $X$ the set $H$ is not a home-space for $X$ if, and only if, $C$ is reachable from $X$. We show that the established relation to the reachability problem yields the Ackermann-completeness of the (semilinear) home-space problem. For this we also show that, given a Petri net with an initial marking, the set of minimal reachable markings can be constructed in Ackermannian time.

On the Home-Space Problem for Petri Nets and its Ackermannian Complexity

TL;DR

The paper resolves the semilinear home-space problem for Petri nets by establishing a duality with non-reachability cores, enabling a reduction to reachability and proving decidability with Ackermannian complexity. It shows that for any Petri net and semilinear set , one can effectively compute a semilinear non-reachability core that characterizes when fails to be a home-space for any , yielding an Ackermannian decision procedure. Additionally, the authors prove that minimal reachable configurations can be computed in Ackermannian time and that inductive semilinear non-reachability cores exist for semilinear sets, enabling constructive witnesses for both positive and negative home-space instances. The results place the semilinear home-space problem at the decidability/complexity boundary and provide practical machinery (cores, inductive invariants, and witnesses) for analyzing reachability and invariance in Petri nets.

Abstract

A set of configurations is a home-space for a set of configurations of aPetri net if every configuration reachable from (any configuration in) can reach (some configuration in) . The semilinear home-space problem for Petri nets asks, given a Petri net and semilinear sets of configurations , , if is a home-space for . In 1989, David de Frutos Escrig and Colette Johnen proved that the problem is decidable when is a singleton and is a finite union of linear sets with the same periods. In this paper, we show that the general (semilinear) problem is decidable. This result is obtained by proving a duality between the reachability problem and the non-home-space problem. In particular, we prove that for any Petri net and any semilinear set of configurations we can effectively compute a semilinear set of configurations, called a non-reachability core for , such that for every set the set is not a home-space for if, and only if, is reachable from . We show that the established relation to the reachability problem yields the Ackermann-completeness of the (semilinear) home-space problem. For this we also show that, given a Petri net with an initial marking, the set of minimal reachable markings can be constructed in Ackermannian time.
Paper Structure (27 sections, 27 theorems, 14 equations, 2 figures)

This paper contains 27 sections, 27 theorems, 14 equations, 2 figures.

Table of Contents

  1. Introduction
  2. A General Approach to the Home-Space Problem
  3. Non-Reachability Cores
  4. Non-Reachability Cores in Finite-State Systems
  5. Non-Reachability Cores for Unions of Sets
  6. Basic Notions, and Main Results
  7. Notation for Vectors of Nonnegative Integers
  8. Linear and Semilinear Sets of Vectors, and their Presentations
  9. Semilinear sets and Presburger arithmetic
  10. Petri Nets
  11. (Semilinear) Reachability Problem
  12. Semilinear Home-Space Problem
  13. Main Results
  14. The Home-Space Problem is Hard
  15. Decidability of Home-Space via Semilinear Non-Reachability Cores
  16. ...and 12 more sections

Key Result

Proposition 2.1

Given $(S,\rightarrow)$ and $H\subseteq S$, let $H=H_1\cup H_2\cdots\cup H_m$ for some $m\geq 1$, and let $C_1,C_2,\dots,C_m$ be non-reachability cores for $H_1,H_2,\dots,H_m$, respectively. For each $X\subseteq S$ we have that $H$ is not a home-space for $X$ if, and only if, there is an execution where $s_0\in X$, and $s_1\in C_1$, $s_2\in C_2$, $\ldots$, $s_m\in C_m$.

Figures (2)

  • Figure 1: $C$ is a non-reachability core for $H$.
  • Figure 2: Let $H=\{s_3,s_4\}$. We have $\textsc{Pre}^*(H)=\{s_0,s_1,s_2,s_3,s_4\}$, and the bottom SCCs of $\overline{\textsc{Pre}^*(H)}$ are $\{s_7,s_8\}$ and $\{s_9,s_{10}\}$. Hence $C=\{s_7,s_9\}$ is one non-reachability core for $H$.

Theorems & Definitions (54)

  • Proposition 2.1
  • proof
  • Proposition 2.2
  • proof
  • Remark 3.1
  • Theorem 3.2
  • Theorem 3.3
  • Remark 3.4
  • Proposition 4.1
  • proof
  • ...and 44 more