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

Abstract

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