On the Complexity of Techniques That Make Transition Systems Implementable by Boolean Nets

TL;DR

The paper studies the complexity of modifying labeled transition systems to enable realizations by Boolean τ-nets, focusing on label-splitting and edge/event/state-removal as minimal-change approaches. It establishes NP-completeness for τ-label-splitting and for edge-, event-, and state-removal across most Boolean types of nets of the form τ = {nop, swap} ∪ ω, with ω ⊆ {inp, out, used, free} and particularly for flip-flop variants, by reductions from the 3-Bounded Vertex Cover problem. A key insight is the tractability boundary: when ω = ∅, several problems become polynomial, while introducing any input/output or related interactions (ω ≠ ∅) yields NP-completeness for embedding, and often for language-simulation and realization as well. The work systematically covers 16 subsections of label-splitting and 4 modification techniques across 15–16 τ-types, extending prior results for embedding, language-simulation, and realization to a broad class of Boolean nets. The results have implications for the design of synthesis tools and indicate inherent computational hardness in preserving minimal-change modifications to achieve implementability in Boolean net models. The authors also outline open cases (notably event-removal with ω = ∅) and point to potential parameterized analyses as avenues for future research.

Abstract

Synthesis consists in deciding whether a given labeled transition system (TS) $A$ can be implemented by a net $N$ of type $τ$. In case of a negative decision, it may be possible to convert $A$ into an implementable TS $B$ by applying various modification techniques, like relabeling edges that previously had the same label, suppressing edges/states/events, etc. It may however be useful to limit the number of such modifications to stay close to the original problem, or optimize the technique. In this paper, we show that most of the corresponding problems are NP-complete if $τ$ corresponds to the type of flip-flop nets or some flip-flop net derivatives.

Figures (6)

• Figure 1: All interactions $i$ of $I$. If a cell is empty, then $i$ is undefined on the respective $x$.
• Figure 2: Left: $A_\tau$ for the the type $\tau=\{\textsf{nop},\textsf{inp},\textsf{swap}\}$. Middle: A $\tau$-net $N$ (as usual, the initial marking is indicated by putting a token in the places $p$ such that $M_0(p)=1$). Right: The reachability graph $A_N$ of $N$, where each state $M$ is represented by its marking $(M(R_1),M(R_2))$, and the initial state is indicated by the arrow without source state.
• Figure 3: Left: The TS $A$ with event set $E=\{a\}$. Middle: The TS $B$ with event set $E'=\{a,a'\}$. Right: The image $B^{R_1}$ of the $\tau$-region $R_1=(sup_1,sig_1)$ of $B$, where $sup_1(t_0)=1$, $sup_1(t_1)=sup_1(t_2)=0$, $sig_1(a)=\textsf{inp}$ and $sig_1(a')=\textsf{nop}$, and $\tau=\{\textsf{nop},\textsf{inp},\textsf{swap}\}$. Later, we shall also represent a region by a color convention indicating the support of each state.
• Figure 4: A running graph example $G$; a 2-VC is $\{{\pmb v_0},{\pmb v_2}\}$ (in bold).
• Figure 5: The transition systems $A_G$ (top) and $B_G$ (bottom) that originate from Example \ref{['ex:vc']}. They will serve for illustrating some region constructions in the proofs below.

Theorems & Definitions (45)

• Definition 2.1: Transition Systems
• Definition 2.2: Simulations
• Definition 2.3: Boolean Types txtcs/BadouelBD15
• Definition 2.4: $\tau$-Nets
• Example 2.5
• Definition 2.6: Implementations
• Remark 2.7
• Definition 2.8: $\tau$-Regions
• Definition 2.9: Synthesized net
• Definition 2.10: $\tau$-State Separation and Property