The Complexity of Synthesis of $b$-Bounded Petri Nets

TL;DR

This paper analyzes the computational complexity of synthesizing and deciding properties of $b$-bounded Petri nets and their extensions, providing a complete characterization for various net types.

Contribution

It offers a comprehensive complexity classification for $ au$-synthesis, $ au$-ESSP, and $ au$-SSP across different bounded Petri net types and their extensions.

Findings

Complexity classifications for $ au$-Solvability, $ au$-ESSP, and $ au$-SSP are provided.

Results cover pure $b$-bounded, $b$-bounded, and $Z_{b+1}$-extensions of Petri nets.

The paper completes the complexity landscape for these synthesis and decision problems.

Abstract

For a fixed type of Petri nets $\tau$, \textsc{$\tau$-Synthesis} is the task of finding for a given transition system $A$ a Petri net $N$ of type $\tau$ ($\tau$-net, for short) whose reachability graph is isomorphic to $A$ if there is one. The decision version of this search problem is called \textsc{$\tau$-Solvability}. If an input $A$ allows a positive decision, then it is called $\tau$-solvable and a sought net $N$ $\tau$-solves $A$. As a well known fact, $A$ is $\tau$-solvable if and only if it has the so-called $\tau$-\emph{event state separation property} ($\tau$-ESSP, for short) and the $\tau$-\emph{state separation property} ($\tau$-SSP, for short). The question whether $A$ has the $\tau$-ESSP or the $\tau$-SSP defines also decision problems. In this paper, for all $b\in \mathbb{N}$, we completely characterize the computational complexity of \textsc{$\tau$-Solvability}, \textsc{$\tau$-ESSP} and \textsc{$\tau$-SSP} for the types of pure $b$-bounded Place/Transition-nets, the $b$-bounded Place/Transition-nets and their corresponding $\mathbb{Z}_{b+1}$-extensions.