The Complexity of Synthesis of -Bounded Petri Nets
arXiv:2106.15256
Abstract
For a fixed type of Petri nets , \textsc{-Synthesis} is the task of finding for a given transition system a Petri net of type (-net, for short) whose reachability graph is isomorphic to if there is one. The decision version of this search problem is called \textsc{-Solvability}. If an input allows a positive decision, then it is called -solvable and a sought net -solves . As a well known fact, 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 has the -ESSP or the -SSP defines also decision problems. In this paper, for all , we completely characterize the computational complexity of \textsc{-Solvability}, \textsc{-ESSP} and \textsc{-SSP} for the types of pure -bounded Place/Transition-nets, the -bounded Place/Transition-nets and their corresponding -extensions.