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

Département d'Informatique -
Université Libre de Bruxelles,
Boulevard du Triomphe
C.P. 212, B-1050 Bruxelles, Belgium.
Email<EMAIL_ADDRESS>Ronny TredupAddress  for correspondence

Institut Für Informatik - Universität Rostock, Albert-Einstein-Straße 22, D18059 Rostock, Germany.
Email<EMAIL_ADDRESS>
R. Devillers, R. TredupThe Complexity of the Label-Splitting-Problem for Flip-Flop-Nets

Let $\tau$ be a type of nets.
Synthesis consists in deciding whether a given labeled transition system (TS) $A$ can be implemented by a net $N$ of type $\tau$.
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 $\tau$ corresponds to the type of flip-flop nets or some flip-flop net derivatives.

§ INTRODUCTION

The so-called synthesis problem for nets of type $\tau$ ($\tau$-synthesis, for short) consists in deciding whether for a given
labeled transition system (TS, for short) $A$ there is a net $N$ of type $\tau$ (a $\tau$-net, for short) that implements $A$.
In case of a positive decision, $N$ should be constructed, possibly while minimizing some features (number of places, arc weights, …); in case of a negative decision, some reason(s) should be given.

$\tau$-Synthesis is used to, for example, extract concurrency from sequential specifications like TS and languages [1] and has applications in, for example, process discovery [2], supervisory control [3] and the synthesis of speed independent circuits [4].

However, whether $N$ exists depends crucially on the kind of implementation we are striving at, that is, whether $N$ should be an (exact) realization, meaning that $A$ and $N$'s reachability graph are isomorphic, or a language-simulation or an embedding.
Unfortunately, whatever the kind of implementation, a solution does not always exist.
This observation motivates the search for techniques that modify the given TS (as little as possible) so that the result is an implementable behavior.

Label-splitting [5, 6, 7, 8] is one of the most notorious techniques of this kind:
This approach may convert a non-implementable TS $A$ into an implementable one $A'$ by relabeling differently some edges that previously had the same label.
However, the new events produced by the label-splitting increase the complexity of the derived net, since each new copy will be transformed into a new transition.
Hence, it is desired to find a label-splitting that induces the minimal number of transitions in the sought net.
This allows to consider $\tau$-label-splitting as a decision problem with input $A$ and $\kappa\in \mathbb{N}$;
the question is whether there is a TS $B$  implementable by a $\tau$-net that, firstly, is derived from $A$ by splitting labels and, secondly, has at most $\kappa$ labels (then, by a dichotomic search, an optimal splitting may be found).
Recently, in [9], it has been shown that $\tau$-label-splitting aiming at embedding is NP-complete if $\tau$ equals the type of weighted Place/Transition-nets.
Moreover, in [10], we have shown that $\tau$-label-splitting aiming at language-simulation or realization is also NP-complete for this type.

Since label-splitting is intractable (at least for weighted Place/Transition nets), other techniques with better worst-case complexity would be preferable.
This led to the idea of simplifying an unimplementable TS by removing some edges, events or states until the result is implementable.
Indeed, the removal of components is a strong technique that always leads to implementable behavior, since the result is implementable when only the initial state is left at the end.
However, such extreme modification is certainly not desirable.
Instead, we aim to remove the minimum number $\kappa$ of components so that the result is implementable.
This justifies to consider the decision problems edge-, event-, and state-removal:
given a TS $A$, and a number $\kappa$, the task is to decide whether we can modify $A$ to an implementable TS $B$ by the removal of at most $\kappa$ edges, events or states, respectively.
Unfortunately, it has been shown that these removal techniques are also NP-complete for all implementations - embedding, language simulation, and realization - if we target (weighted) P/T-nets [11, 12].

Naturally, it raises the question whether the decision problems,
and thus the corresponding modification techniques,
are of a different complexity provided the net-type sought or the implementation sought, or both, are different.

A whole class of net-types for which such investigations are certainly of interest is defined by the family of the so-called Boolean types of nets [5, 13, 14, 15, 16, 17, 18], since the respective nets are widely accepted as excellent tools for modeling concurrent and distributed systems.

Boolean nets allow at most one token on each place $p$ in every reachable marking.
Therefore, $p$ is considered a Boolean condition that is true if $p$ is marked and false otherwise.
A place $p$ and a transition $t$ of a Boolean net $N$ are related by one of the following Boolean interactions
(partial functions):
no operation (), input (), output (), unconditionally set to true (), unconditionally
reset to false (), inverting (), test if true (), and test if false ().
The relation between $p$ and $t$ determines which conditions $p$ must satisfy to allow $t$'s firing and which impact has the firing of $t$ on $p$.
Boolean nets are then classified by the interactions of $I=\{\nop,\inp,\out,\res,\set,\swap,\used,\free\}$ that they apply or spare.
More exactly, a subset $\tau\subseteq I$ is called a Boolean type of net and a net $N$ is of type $\tau$ (a $\tau$-net) if it applies at most the interactions of $\tau$.

However, the determination of the complexity of TS modifications allowing $\tau$-synthesis does not actually define an open problem for all Boolean types of nets.
In particular, it is known that $\tau$-synthesis aiming at language-simulation or realization is NP-complete for 84 out of the 128 Boolean types of nets containing  (which allows some kind of independence between places and transitions) [19, 20, 21, 22, 20].
For these types, the NP-completeness of $\tau$-synthesis implies already the NP-completeness of the corresponding problems label-splitting, and edge-, event-, and state-removal, for instance by choosing $\kappa$ in a way that forbids any splitting, or removal, respectively.
This puts the Boolean types with a tractable synthesis problem in focus.
One of the most prominent Boolean type that fulfills this criterion is the so-called flip-flop type of nets, where $\tau=\{\nop,\inp,\out,\used\}$.
Flip-flop nets have been originally introduced in [18] as the Boolean counterpart of the Place/Transition nets.
The latter characterization is mainly based on the fact that synthesis aiming at flip-flop nets is solvable by a polynomial time algorithm [18] that is derived from the algorithm for synthesis aiming at Place/Transition nets, which has been introduced in [23].
In fact, the algorithm for flip-flop nets [18] is extendable to all types $\tau=\{\nop,\swap\}\cup\omega$ with $\omega\subseteq \{\inp,\out,\used,\free\}$ [21], which makes their synthesis problem also tractable.

In this paper, for all 16 types $\tau=\{\nop,\swap\}\cup\omega$ with $\omega \subseteq\{\inp,\out,\used,\free\}$, we investigate the computational complexity of $\tau$-label-splitting and element removing for all introduced implementations: embedding, language-simulation and realization.
In particular, we show that this problem aiming at embedding is NP-complete for all these types.
Moreover, label-splitting aiming at language-simulation or realization is NP-complete if $\omega\not=\emptyset$, otherwise it is tractable.

Furthermore, for all 15 types $\tau=\{\nop,\swap\}\cup\omega$ with $\omega \subseteq\{\inp,\out,\used,\free\}$ and $\omega\not=\emptyset$, we investigate the computational complexity of $\tau$-edge-, event-, and state-removal, and show that these problems are NP-complete for all these types, regardless which of the implementations embedding, language-simulation and realization we are aiming at.

We obtain our NP-completeness results by reductions from a variant of the well-known vertex cover problem.
Our current approach generalizes our methods from [10, 12] and tailors them to flip-flop nets and its aforementioned derivatives.

This paper, which is an extended version of [24], is organized as follows.

The next Section <ref> introduces necessary notions and definitions.
After that, Section <ref> presents our complexity results for label-splitting
while the next ones concentrate on edge/event/state removals.
Finally, Section <ref> briefly closes the paper.

§ PRELIMINARIES AND LABEL-SPLITTING

This section introduces the basic notions used throughout the paper.

A (deterministic, labeled, reduced) transition system (TS) $A=(S,E, \delta)$ is a directed labeled graph with the set of nodes $S$ (called states), the set of labels $E$ (called events) and partial transition function $\delta: S\times E \longrightarrow S$; we shall assume no event is useless, i.e., for every $e\in E$ there are states $s,s'\in S$ such that $\delta(s,e)=s'$.
For convenience, with a little abuse of notation, we often identify $\delta$ and the set $\{(s,e,s')\mid s,s'\in S, e\in E: \delta(s,e)=s'\}$.
Event $e$ occurs at $s$, denoted by $s\edge{e}$, if $\delta(s,e)$ is defined, otherwise we denote it by $s\edge{\neg e}$ or $\neg s\edge{e}$.
We denote $\delta(s,e)=s'$ by $s\edge{e}s'$.
An initialized TS $A=(S,E,\delta, \iota)$ is a TS with a distinct initial state $\iota\in S$ such that
every state $s\in S$ is reachable from $\iota$ by a directed labeled path.
If $w=e_1\dots e_n\in E^*$,
by $\iota\edge{w}$ we denote that there are states
$\iota=s_0,\dots, s_n\in S(A)$ such that $s_i\edge{e_{i+1}}s_{i+1}\in A$ for all $i\in \{0,\dots, n-1\}$,
in which case we also denote $\iota\edge{w}s_n$; we extend this notation by stating that $\iota\edge{\epsilon}\iota$.
The language of $A$ is defined by $L(A)=\{ w \in E^*\mid \iota\edge{w} \}$.
We refer to the components of a TS $A$ by $S(A)$ (states), $E(A)$ (events), $\delta_A$ (transition function) and $\iota_A$ (initial state).

We would like to emphasize that in this paper we deal exclusively with initialized transition systems, which we call TS for short.

Let $A$ and $B$ be TS with the same set of events $E$.
We say $B$ simulates $A$, if there is a mapping $\varphi : S(A)\rightarrow S(B)$ such that $s\edge{e}s'\in A$ implies $\varphi(s)\edge{e}\varphi(s')\in B$;
such a mapping is called a simulation (between $A$ and $B$).
$\varphi$ is an embedding, denoted by $A\hookrightarrow B$, if it is injective;
$\varphi$ is a language-simulation, denoted by $A\triangleright B$, if $\varphi(s)\edge{e}$ implies $s\edge{e}$, implying $L(A)=L(B)$ <cit.>;
$\varphi$ is an isomorphism, denoted by $A\cong B$, if it is both an embedding and a language simulation.

Let $A=(S,E,\delta, \iota)$ be a TS and $e_1,\dots, e_n\in E$ be pairwise distinct events.
The label-splitting of the events $e_1,\dots, e_n$ into the events $e_1^1,\dots, e_1^{m_1}, \dots, e_n^1,\dots, e_n^{m_n}$  (pairwise distinct), where $m_j\geq2$ for all $j\in \{1,\dots, n\}$, yields the event set $E'=(E\setminus \{e_1,\dots, e_n\})\bigcup_{i=1}^{n}\{e_i^j \mid j\in \{1,\dots, m_j\}\}$.
A TS $B=(S, E',\delta',\iota)$ is a $E'$-label-splitting ($E'$-LS, for short) of $A$ if $\vert \delta \vert =\vert\delta' \vert$ and, for all $s,s'\in S$ and all $e\in E$, the following is true:
If  $\delta(s,e)=s'$ and $e\not\in \{e_1,\dots, e_n\}$, then $\delta'(s, e)=s'$;
if $\delta(s,e)=s'$ and $e=e_i$ for some $i\in \{1,\dots, n\}$, then there is exactly one $\ell\in \{1,\dots, m_i\}$ such that $\delta'(s, e_i^\ell)=s'$.
We say that $\mL=\{e_1,\dots, e_n\}$ is the set of events of $A$ that occur split in $B$.
Note that often $e^1_j=e_j$ for some or all $j\in\{1,\ldots,n\}$.

$x$     $\nop(x)$     $\inp(x)$     $\out(x)$     $\set(x)$     $\res(x)$     $\swap(x)$     $\used(x)$     $\free(x)$
$0$     $0$         $1$     $1$     $0$     $1$         $0$

$1$     $1$     $0$         $1$     $0$     $0$     $1$

All interactions $i$ of $I$.
If a cell is empty, then $i$ is undefined on the respective $x$.

[new set = import nodes]

(0) at (0,0) $0$;
(1) at (1.2,0) $1$;

(0) edge [->, out=-120,in=120,looseness=5] node[left] $\nop$ (0);
(1) edge [<-, out=60,in=-60,looseness=5] node[right] $\nop$   (1);

(0) edge [<-, bend right= 30] node[below] $\inp, \swap$ (1);
(0) edge [->, bend  left = 30] node[above] $\swap$ (1);
() at (0.5,-1.2) $A_\tau$;

place=[circle,thick,draw=blue!75,fill=blue!20,minimum size=6mm]
red place=[place,draw=red!75,fill=red!20]
fill=black!20,minimum size=4mm]
every label=[red]
[xshift=5cm, node distance=0.5cm,bend angle=45,auto]
(x) at (0,0) ;
[place] (R1)[tokens =1,left of=x, label=above: $R_1$, node distance =1.5cm];
[transition] (a)[above of =x]$a$
edge [above,] node $\nscale{\inp}$  (R1);
[transition] (b)[below of =x]$a'$
edge [ below] node $\nscale{\nop}$  (R1);

[place] (R2)[right of=x, label=above: $R_2$, node distance =1.5cm]
edge [above] node $\nscale{\swap}$  (a)
edge [below] node $\nscale{\inp}$  (b);
() at (0,-1.2) $N$;

[xshift=8cm,nodes=set=import nodes]
(A) at (1.3,-1.2) $A_N$;
(10) at (0,0) $(1,0)$;
(01) at (1.3,0) $(0,1)$;
(00) at (2.6,0) $(0,0)$;
(import nodes);
10 ->["$a$"]01;
01 ->["$a'$"]00;

$A_\tau$ for the the type $\tau=\{\nop,\inp,\swap\}$, a $\tau$-net $N$ and its reachability graph $A_N$.

[new set = import nodes]
[nodes=set=import nodes]

ıin 0,...,2 (ı) at (ı*1.2cm,0) $t_\i$;
() at (1,-0.5) $A$;

(import nodes);

[xshift=4cm,nodes=set=import nodes]

ıin 0,...,2 (ı) at (ı*1.2cm,0) $t_\i$;
() at (1,-0.5) $B$;

(import nodes);

[xshift=8cm,nodes=set=import nodes]

ıin 0 (ı) at (ı*1.2cm,0) $1$;
ıin 1,2 (ı) at (ı*1.2cm,0) $0$;
() at (1,-0.5) $B^{R_1}$;

(import nodes);

The TS $A$ with event set $E=\{a\}$,
a $E'$-label-splitting $B$ of $A$, where $E'=(E\setminus \{a\})\cup\{a,a'\}=\{a,a'\}$ and the image $B^{R_1}$ of the $\tau$-region $R_1=(sup_1,sig_1)$, where $sup_1(t_0)=1$, $sup_1(t_1)=sup_1(t_2)=0$, $sig_1(a)=\inp$ and $sig_1(a')=\nop$.

A Boolean type is a subset $\tau$ of the 8 Boolean interactions $I=\{\nop, \inp, \out, \set, \res, \swap, \used, \free\}$, i.e.,
the partial functions $\{0,1\}\to\{0,1\}$ schematized in Figure <ref>.
In fact there are $(2+1)^2=9$ such partial functions, but the empty one (defined nowhere) is of no interest here, since it may never occur as the label of an event.
To each type $\tau$, we may associate a Boolean TS $A_\tau=(\{0,1\},E_\tau,\delta_\tau)$, where $E_\tau=\tau$
and, for each $x\in \{0,1\}$ and $i\in E_\tau$, $\delta_\tau(x,i)$ is defined if so is $i(x)$, in which case $\delta_\tau(x,i)=i(x)$.
Since the correspondence is unique, we often  identify $\tau$ with $A_\tau$.

Let $\tau\subseteq I$.
A Boolean net $N = (P, T, f, M_0)$ of type $\tau$ (a $\tau$-net) is given by finite disjoint sets $P$ of places and $T$ of transitions, a (total) flow function $f: P \times T \rightarrow \tau$, and an initial marking $M_0: P\longrightarrow  \{0,1\}$.

A transition $t \in T$ can fire in a marking $M: P\longrightarrow  \{0,1\}$ if $\delta_\tau(M(p), f(p,t))$ is defined for all $p\in P$.
By firing, $t$ produces the marking $M' : P\longrightarrow  \{0,1\}$ where $M'(p)=\delta_\tau(M(p), f(p,t))$ for all $p\in P$, denoted by $M \edge{t} M'$.
The behavior of $\tau$-net $N$ is captured by a transition system $A_N$, called the reachability graph of $N$.
The states set $RS(N)$ of $A_N$ consists of all markings that can be reached from initial state $M_0$ by sequences of transition firings.

Figure <ref> shows the transition system $A_\tau$ for the type $\tau=\{\nop,\inp,\swap\}$, the $\tau$-net
$N=(\{R_1,R_2\}, \{a,a'\}, f, M_0)$ with places $R_1, R_2$, flow-function $f(R_1,a)=f(R_2, a')=\inp$, $f(R_1,a')=\nop$, $f(R_2,a)=\swap$ and initial marking $M_0$ defined by $(M_0(R_1),M_0(R_2))=(1,0)$.
Since $1\edge{\inp}0\in \tau$ and $0\edge{\swap}1\in \tau$, the transition $a$ can fire in $M_0$, which leads to the marking $M=(M(R_1), M(R_2))=(0,1)$.
After that, $a'$ can fire, which results in the marking $M'=(M'(R_1), M'(R_2))=(0,0)$.
The reachability graph $A_N$ of $N$ is depicted on the right hand side of Figure <ref>.

Let $A$ be a TS, $\tau$ be a Boolean type and $N$ a $\tau$-net.
We say $N$ is a (exact) realization of $A$ if $A\cong A_N$.
If $A\triangleright A_N$, then $N$ is a language-simulation of $A$;
if $A\hookrightarrow A_N$, then $N$ is an embedding of $A$.

Let $\tau$ be a Boolean type of nets.
If a TS $A$ is implementable by a $\tau$-net $N$, then we want to construct $N$ purely from $A$.
Since $A_N$ has to simulate $A$, $N$'s transitions correspond to $A$'s events.
The connection between global states in TS and local states in the sought net is given by regions of TS that mimic places:
A $\tau$-region $R=(sup, sig)$ of $A=(S, E, \delta, \iota)$ consists of the support $sup: S \rightarrow \{0,1\}$ and the signature $sig: E \rightarrow E_\tau$ where every edge $s \edge{e} s'$ of $A$ leads to an edge $sup(s) \ledge{sig(e)} sup(s')$ of type $\tau$.
If $P=q_0\edge{e_1}\dots \edge{e_n}q_n$ is a path in $A$, then $P^R=sup(q_0)\ledge{sig(e_1)}\dots\ledge{sig(e_n)}sup(q_n)$ is a path in $\tau$.
We say $P^R$ is the image of $P$ (under $R$).
Notice that $R$ is implicitly completely defined by $sup(\iota)$ and $sig$:
Since $A$ is reachable, for every state $s\in S(A)$, there is a path $\iota\edge{e_1}\dots \edge{e_n}s_n$ such that $s=s_n$.
Thus, since $\tau$ is deterministic, we inductively obtain $sup(s_{i+1})$ by $sup(s_{i+1})=\delta_\tau(sup(s_i) ,sig(e_{i+1}))$ for all $i\in \{0,\dots, n-1\}$ and $s_0 = \iota$.
Consequently, we can compute $sup$ and thus $R$ purely from $sup(\iota)$ and $sig$ (and $A$), provided that when two paths lead to a same state the corresponding supports are the same; this is illustrated in Figure <ref>.
A region $(sup, sig)$ models a place $p$ and the associated part of the flow function $f$.
In particular, $f(p,e) = sig(e)$ and $M(p) = sup(s)$, for marking $M\in RS(N)$ that corresponds to $s\in S(A)$.
Every set $\mathcal{R} $ of $\tau$-regions of $A$ defines the synthesized $\tau$-net $N^{\mathcal{R}}_A=(\mathcal{R}, E, f, M_0)$ with  $f((sup, sig),e)=sig(e)$ and $M_0((sup, sig))=sup(\iota)$ for all $(sup, sig)\in \mathcal{R}, e\in E$.

To ensure that the input behavior is captured by the synthesized net, we have to distinguish global states, and prevent the firings of transitions when their corresponding events are not present in TS.
This is stated as so called separation atoms and properties.
A pair $(s, s')$ of distinct states of $A$ defines a states separation atom (SSP atom).
A $\tau$-region $R=(sup, sig)$ solves $(s,s')$ if $sup(s)\not=sup(s')$.
If every SSP atom of $A$ is $\tau$-solvable then $A$ has the $\tau$-states separation property ($\tau$-SSP, for short).
A pair $(e,s)$ of event $e\in E $ and state $s\in S$ where $e$ does not occur, that is $\neg s\edge{e}$, defines an event/state separation atom (ESSP atom).
A $\tau$-region $R=(sup, sig)$ solves $(e,s)$ if $sig(e)$ is not defined on $sup(s)$ in $\tau$, that is, $\neg sup(s)\ledge{sig(e)}$.
If every ESSP atom of $A$ is $\tau$-solvable then $A$ has the $\tau$-event state separation property ($\tau$-ESSP, for short).
A set $\mathcal{R}$ of $\tau$-regions of $A$ is called a $\tau$-witness for $A$'s $\tau$-SSP, respectively $\tau$-ESSP, if for each SSP atom, respectively ESSP atom, there is a $\tau$-region $R$ in $\mathcal{R}$ that solves it.

The next lemma (<cit.>, Proposition 5.10) establishes the connection between the existence of $\tau$-witnesses and the existence of an implementing $\tau$-net $N$ in dependence of the testified property:

If $A$ is a TS, $\tau$ a Boolean type and $N$ a $\tau$-net, then $A\hookrightarrow A_N$, respectively $A \triangleright A_N$, respectively $A\cong A_N$, if and only if there is a $\tau$-witness $\mathcal{R}$ that testifies $A$'s $\tau$-SSP, respectively $\tau$-ESSP, respectively both $\tau$-SSP and $\tau$-ESSP, and $N=N^{\mathcal{R}}_A$.

By Lemma <ref>, deciding the existence of an implementing net is equivalent to deciding if the input TS has the property that corresponds to the implementation.
Our NP-completeness proofs substantially exploit this deep connection between the existence of a witness (for the demanded property) and the existence of an implementing system, which is testified by the witness.
Finally, this leads to the following three decision problems that are the main subject of this paper:

a TS $A=(S,E,\delta, \iota)$, a natural number $\kappa$.
Does there exist a $E'$-LS $B$ of $A $ with $\vert E' \vert \leq \kappa$ that has the $\tau$-SSP?

LS-$\tau$-Language Simulation
a TS $A=(S,E,\delta, \iota)$, a natural number $\kappa$.
Does there exist a $E'$-LS $B$ of $A $ with $\vert E' \vert \leq \kappa$ that has the $\tau$-ESSP?

a TS $A=(S,E,\delta, \iota)$, a natural number $\kappa$.
Does there exist a $E'$-LS $B$ of $A $ with $\vert E' \vert \leq \kappa$ that has both the $\tau$-SSP and the $\tau$-ESSP?

Let $\tau$ be defined like in Figure <ref> and $A,B,B^{R_1}$ like in Figure <ref>.
The TS $A$ has neither the $\tau$-SSP nor the $\tau$-ESSP, since the atoms $(t_0,t_2)$ and $(a, t_2)$ are not $\tau$-solvable.
The TS $B$ is a $E'$-label-splitting of $A$, where $E'=(E\setminus\{a\})\cup \{a,a'\}$, and has both the $\tau$-SSP and $\tau$-ESSP.
The region $R_1=(sup_1,sig_1)$ that solves $(t_0,t_1)$, $(t_0,t_2)$, $(a,t_1)$ and $(a, t_2)$ is implicitly defined by $sup_1(t_0)=1$, $sig_1(a)=\inp$ and $sig_1(a')=\nop$.
We obtain $sup_1$ and thus $R_1$ explicitly by $sup_1(t_1)=\delta_{\tau}(1,\inp)=0$ and $sup_1(t_2)=\delta_{\tau}(0,\nop)=0$.
$B^{R_1}$ shows the image of $B$ under $R_1$.
The remaining (E)SSP atoms $(t_1,t_2)$, $(a',t_0)$ and $(a', t_1)$ are solved by the following region $R_2=(sup_2,sig_2)$ that is implicitly defined by $sup_2(t_0)=0$, $sig_2(a)=\swap$ and $sig_2(a')=\inp$.
The set $\mathcal{R}=\{R_1,R_2\}$ is a witness for the $\tau$-(E)SSP of $A$ and the net $N^\mathcal{R}_A$ is exactly the net $N$ that is depicted in Figure <ref>.
$N$ is a realization of $A$, since a bijective simulation $\varphi$ between $A$ and $A_N$ is given by $\varphi(t_0)=(1,0)$, $\varphi(t_1)=(0,1)$ and $\varphi(t_2)=(0,0)$.

§ THE COMPLEXITY OF LABEL SPLITTING

The following theorem presents the main result of this section:

If $\tau=\{\nop,\swap\}\cup\omega$ with $\omega\subseteq \{\inp,\out,\used,\free\}$, then

LS-$\tau$-Embedding is NP-complete,

LS-$\tau$-Language Simulation, and LS-$\tau$-Realisation are NP-complete if $\omega\not=\emptyset$, otherwise they are in P.

First of all, we argue for the polynomial part:
If $\tau=\{\nop,\swap\}$, and more generally if $\tau\subseteq\{\nop,\swap,\set,\res\}$, then a TS $A=(S,E,\delta,\iota)$ has the $\tau$-ESSP if and only if every event occurs at every state.
This is because all those functions are defined on both $0$ and $1$.
Thus, any ESSP atom $(e,s)$ of $A$ would be unsolvable.
This implies that an $E'$-label-splitting $B$ of $A$ that reflects an actual splitting, meaning that $\vert E'\vert > \vert E\vert$, can never yield a TS that has the $\tau$-ESSP, since it would produce unsolvable ESSP atoms:
If $\vert E'\vert > \vert E\vert$, then there is an event $e_i$ in $A$ for which there are edges $s\Edge{e_i^j}s'$, and $t\Edge{e_i^\ell}t'$ in $B$ with $s\not=t$, and $e_i^j\not=e_i^\ell$ (since $A$, and $B$ are deterministic, and every event has an occurrence by Definition <ref>), which were previously both labeled by $e_i$.
This implies $\neg s\Edge{e_i^\ell}$ (by determinism of $A$), and thus $(s, e_i^\ell)$ is not solvable.
Moreover, if $A$ is such that every event occurs at every state, but has an unsolvable SSP atom, then (by similar reasons) any label-splitting for this atom would destroy the ESSP.
Hence, for this type, the decision problems are trivial, since either $A$ is already implementable or it has to be rejected.
Thus, for the proof of Theorem <ref>(<ref>), it remains to consider the cases when $\omega\not=\emptyset$, hence the NP-completeness results.

The decision problems LS-$\tau$-Embedding, LS-$\tau$-Language Simulation as well as LS-$\tau$-Realisation are in NP:
If a sought $E'$-label-splitting $B=(S,E', \delta',\iota)$ of a TS $A=(S,E, \delta,\iota )$ exists, then a Turing-machine $M$ can compute $B$ in a non-deterministic computation in time polynomial in the size $\vert \delta\vert$ of $A$, since $\vert \delta\vert =\vert \delta'\vert$.
After that, $M$ verifies in time polynomial in the size $\vert \delta'\vert$ of $B$ (and thus of $A$) that it allows the sought implementation [18, 21].

Our NP-completeness proofs are based on reductions from the following classical variant of the vertex cover (VC) problem <cit.>:

3-Bounded Vertex Cover (3BVC)
a non-directed  Graph $G=(\U, M)$ such every vertex $v\in \U$ is a member of at most three distinct edges $M_0,M_1,M_2\in M$, a natural number $\lambda\in \mathbb{N}$.
Does there exist a $\lambda$-VC of $G$, that is, a subset $\Ss\subseteq \U$ with $\vert \Ss\vert \leq \lambda$ and $\Ss\cap \mathfrak{e}\not=\emptyset$ for all $\mathfrak{e}\in M$?

The instance $(G,2)$, illustrated in Figure <ref>, where $G=(\U,M)$ such that $\U=\{v_0,v_1,v_2,v_3\}$ and $M=\{ M_0,\dots, M_4\}$, where $M_0=\{v_0,v_1\}, M_1=\{v_0,v_2\}, M_2=\{v_0,v_3\}, M_3=\{v_1,v_2\}$, and $M_4=\{v_2,v_3\} $, is a yes-instance of 3BVC, since $\Ss=\{v_0,v_2\}$ is a suitable vertex cover of $G$.

[circle,fill=black!100,inner sep=0.05cm](0)at(0,0)[label=left:$\pmb v_0$];
[circle,fill=black!100,inner sep=0.05cm](1)at(0,5)[label=left:$v_1$];
[circle,fill=black!100,inner sep=0.05cm](2)at(5,5)[label=right:$\pmb v_2$];
[circle,fill=black!100,inner sep=0.05cm](3)at(5,0)[label=right:$v_3$];

[-](0)to node[auto,left](1);
[-](0)to node[auto,above,pos=0.3](2);
[-](0)to node[auto,right,pos=0.3](3);
[-](1)to node[auto,right](2);
[-](2)to node[auto,right](3);

A running graph example $G$; a 2-covering is $\{{\pmb v_0},{\pmb v_2}\}$ (in bold).

In the remainder of this paper, let $(G,\lambda)$ be an input of 3BVC, where $G=(\U,M)$ is a graph with $n$ vertices $\U=\{v_0,\dots, v_{n-1}\}$ and $m$ edges $M=\{M_0,\dots, M_{m-1}\}$ such that $M_i=\{v_{i_0}, v_{i_1}\}$ and $i_0 < i_1$ for all $i\in \{0,\dots, m-1\}$.

For the proof of Theorem <ref>, we polynomially reduce $(G,\lambda)$ to a pair $(A_G,\kappa)$ of TS
$A_G=(S,E,\delta,\bot_0)$ and natural number $\kappa$ such that the following conditions are satisfied:

If there is an $E'$-label-splitting of $A_G$ that satisfies $\vert E'\vert \leq \kappa$ and has the $\tau$-SSP or the $\tau$-ESSP, then $G$ has a $\lambda$-VC.

If $G$ has a $\lambda$-VC, then there is an $E'$-label-splitting of $A_G$ that satisfies $\vert E'\vert \leq \kappa$ and has both the $\tau$-SSP and the $\tau$-ESSP.

Obviously, a polynomial-time reduction that satisfies Condition <ref> and Condition <ref> ensures that $G$ allows a $\lambda$-VC if and only if $A_G$ allows a $E'$-label-splitting that satisfies $\vert E'\vert \leq \kappa$ and has the $\tau$-SSP, the $\tau$-ESSP or both, according to which property is sought.
Hence, it proves Theorem <ref>.

§.§ The Proof of Theorem <ref>(<ref>)

[new set = import nodes]
[nodes=set=import nodes]
(bot1) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
(bot1) at (bot1) $\bot_0$;
ıin 0,...,4 (ı) at (ı) $t_{0,\i}$;

(import nodes);

[yshift=-1cm, nodes=set=import nodes]
(bot2) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
(bot2) at (bot2) $\bot_1$;
ıin 0,...,4 (ı) at (ı) $t_{1,\i}$;

(import nodes);

[yshift=-2cm, nodes=set=import nodes]
(bot3) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
(bot3) at (bot3) $\bot_2$;
ıin 0,...,4 (ı) at (ı) $t_{2,\i}$;

(import nodes);

[yshift=-3cm, nodes=set=import nodes]
(bot4) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
(bot4) at (bot4) $\bot_3$;
ıin 0,...,4 (ı) at (ı) $t_{3,\i}$;

(import nodes);

[yshift=-4cm,nodes=set=import nodes]
(bot5) at (0,0);
(bot5) at (0,0) $\bot_4$;
ıin 0,...,4  (ı) at (1.8cm+ ı*1.8cm,0) ;
ıin 0,...,4  (ı) at (ı) $t_{4,\i}$;

(import nodes);

(bot1) edge [->] node[left] $\ominus_1$  (bot2);
(bot2) edge [->] node[left] $\ominus_2$  (bot3);
(bot3) edge [->] node[left] $\ominus_3$  (bot4);
(bot4) edge [->] node[left] $\ominus_4$  (bot5);

[new set = import nodes]
[nodes=set=import nodes]
(bot1) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
(bot1) at (bot1) $\bot_0$;
ıin 0,...,4 (ı) at (ı) $t_{0,\i}$;

(import nodes);

[yshift=-1cm, nodes=set=import nodes]
(bot2) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
(bot2) at (bot2) $\bot_1$;
ıin 0,...,4 (ı) at (ı) $t_{1,\i}$;

(import nodes);

[yshift=-2cm, nodes=set=import nodes]
(bot3) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);

(bot3) at (bot3) $\bot_2$;
ıin 0,...,4 (ı) at (ı) $t_{2,\i}$;

(import nodes);

[yshift=-3cm, nodes=set=import nodes]
(bot4) at (0,0);

ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
(bot4) at (bot4) $\bot_3$;
ıin 0,...,4 (ı) at (ı) $t_{3,\i}$;

(import nodes);

[yshift=-4cm,nodes=set=import nodes]
(bot5) at (0,0);

(bot5) at (0,0) $\bot_4$;
ıin 0,...,4  (ı) at (1.8cm+ ı*1.8cm,0) ;
ıin 0,...,4  (ı) at (ı) $t_{4,\i}$;

(import nodes);

(bot1) edge [->] node[left] $\ominus_1$  (bot2);
(bot2) edge [->] node[left] $\ominus_2$  (bot3);
(bot3) edge [->] node[left] $\ominus_3$  (bot4);
(bot4) edge [->] node[left] $\ominus_4$  (bot5);

The transition systems  $A_G$ (top) and  $B_G$ (bottom) that originate from Example <ref>.
They will serve for illustrating some region constructions in the proofs below.

In the remainder of this section, unless stated explicitly otherwise, we assume that

$\tau=\{\nop,\swap\}\cup\omega$, with an arbitrary but fixed subset $\omega\subseteq\{\inp,\out,\used,\free\}$.

For a start, we define $\kappa=n+2m-1+\lambda$, where $n+2m-1$ is the number of events of the aforementioned TS $A_G$.
Hence, $\lambda$ is the maximum number of events of $A_G$ that could potentially be split in a $E'$-label-splitting $B_G$ of $A_G$.

For every $i\in \{0,\dots, m-1\}$, the TS $A_G$ has the following directed path $T_i$ that uses the vertices $v_{i_0}$ and $v_{i_1}$ of the edge $M_i$ as events:

[new set = import nodes, scale =0.8]
[nodes=set=import nodes]
(T) at (-0.75,0) $T_i=$;
ıin 0,...,4  (ı) at (ı*2cm, 0) ;
ıin 0,...,4  (ı) at (ı) $t_{i,\i}$;
(import nodes);
0 ->["$v_{i_0}$"]1->["$v_{i_1}$"]2->["$v_{i_0}$"]3->["$v_{i_1}$"]4;

Finally, for all $i\in \{0,\dots, m-1\}$, we apply the edge $\bot_i\edge{w_i}t_{i,0}$ and, if $i < m-1$, then also the edge $\bot_{i}\edge{\ominus_{i+1}}\bot_{i+1}$ to connect the paths $T_0,\dots, T_{m-1}$ into the TS $A_G$, cf. Figure <ref>.
Let $\bot=\{\bot_0,\dots, \bot_{m-1}\}$ and $W=\{w_0,\dots, w_{m-1}\}$ and $\ominus=\{\ominus_1,\dots, \ominus_{m-1}\}$.
The TS $A_G$ has exactly $\vert V \cup W\cup \ominus\vert= n+2m-1$ events.

In order to prove Theorem <ref>(<ref>) we shall show that $A_G$ allows a label-splitting $B_G$ restricted by $\kappa$, and having the $\tau$-SSP if and only if there is a suitable vertex cover for $G$.

The following lemma implies that if a TS has any of the introduced paths, then it does not have the $\tau$-SSP:

Let $A$ be a TS that has the path $P_0=s_0\edge{a}s_1\edge{b}s_2\edge{a}s_3\edge{b}s_4$.
If $R=(sup, sig)$ is a $\tau$-region of $A$, then $sup(s_0)=sup(s_4)$.

Let $R=(sup, sig)$ be an arbitrary but fixed region of $A$.
If $sup(s_0)\not=sup(s_4)$, then the image $P^R$ is a path from $0$ to $1$ or from $1$ to $0$ in $\tau$.
This implies that the number of state changes between $0$ and $1$ on $P^R$ must be odd.
Since $sig(a), sig(b)\in \{\nop,\inp,\out,\swap,\used,\free\}$ and both $a$ and $b$ occur twice, i.e. an even number of times, this is impossible.

Note that this lemma would not be true if  and/or  would be allowed in $\tau$:
for instance, we have $0\edge{\set}1\edge{\nop}1\edge{\set}1\edge{\nop}1$.

Hence, if a TS has the path $T_i$ for some $i\in \{0,\dots, m-1\}$, then the SSP atom $(t_{i,0},t_{i,4})$ is not $\tau$-solvable by Lemma <ref>.
The following lemma states that this implies a $\lambda$-VC of $G$ if a sought $E'$-label-splitting $B_G$ of $A_G$ exists:

If there is a $E'$-label-splitting $B_G$ of $A_G$ such that $\vert E' \vert \leq \kappa$ that has the $\tau$-SSP, then $G$ has a $\lambda$-vertex cover.

Let $i\in \{0,\dots, m-1\}$ be arbitrary but fixed, and let $\mL$ be the set of events of $A_G$ that occur split in $B_G$.
By Lemma <ref>, the SSP atom $\alpha_i=(t_{i,0},t_{i,4})$ is not $\tau$-solvable by regions of $A_G$.
However, since $B_G$ has the $\tau$-SSP, the atom $\alpha_i$ is $\tau$-solvable in $B_G$.
This implies $\{v_{i_0}, v_{i_1}\}\cap \mL \not=\emptyset$.
Since $i$ was arbitrary, this is simultaneously true for all paths $T_0,\dots, T_{m-1}$ and thus the set $\Ss=\U\cap \mL$ intersects with every edge of $G$.
Moreover, by $\vert E'\vert \leq \kappa=n+2(m-1)+\lambda$, we have $\vert \Ss\vert \leq \vert \mL\vert \leq \kappa$.
Hence, $\Ss$ defines a $\lambda$-VC of $G$.
This proves the claim.

Conversely, let $\Ss=\{v_{j_0},\dots, v_{j_{\lambda-1}}\}\subseteq \U$ be a $\lambda$-VC of $G$.
In the remainder of this section, we argue that there is a sought $E'$-label-splitting $B_G$ of $A_G$.
For every $i\in \{0,\dots, \lambda-1\}$, we split the event $v_{j_i}$ into the two events $v_{j_i}$  and $v_{j_i}'$.
This yields $E'=(E\setminus \Ss)\cup\bigcup_{i=0}^{\lambda-1}\{v_{j_i}, v_{j_i}'\}$.
To define the aforementioned $E'$-label-splitting $B_G=(S, E',\delta', \bot_0)$ of $A_G$, it suffices to define $\delta'$ on the states of $T_0,\dots, T_{m-1}$.
In particular, for all $i\in \{0,\dots, m-1\}$, $\delta'$ restricted to $S(T_i)$ and $E(T_i)$ yields the path $T_i'$ as follows:

* if $v_{i_0}\in \Ss$ and $v_{i_1}\not\in \Ss$, then $T_i'=t_{i,0}\lEdge{v_{i_0}'}t_{i,1}\lEdge{v_{i_1}}t_{i,2},\lEdge{v_{i_0}}t_{i,3}\lEdge{v_{i_1}} t_{i,4}$;

* if $v_{i_0}, v_{i_1}\in \Ss$, then $T_i'=t_{i,0}\lEdge{v_{i_0}}t_{i,1}\lEdge{v_{i_1}}t_{i,2},\lEdge{v_{i_0}'}t_{i,3}\lEdge{v_{i_1}'} t_{i,4}$;

* if $v_{i_0}\not\in \Ss$ and $v_{i_1}\in \Ss$, then $T_i'=t_{i,0}\lEdge{v_{i_0}}t_{i,1}\lEdge{v_{i_1}}t_{i,2},\lEdge{v_{i_0}}t_{i,3}\lEdge{v_{i_1}'} t_{i,4}$.

The following lemma essentially states that if $sup: S(B_G)\rightarrow\{0,1\}$ and $sig: E(B_G)\rightarrow \tau$ are mappings that define regions when restricted to $T_0',\dots, T_{m-1}'$, then they can be extended suitably to a region of $B_G$:

If $sup: S(B_G)\setminus \bot \rightarrow \{0,1\}$ and $sig: E'\setminus (W\cup\ominus) \rightarrow \tau$ are mappings such that $s\edge{e}s'\in B_G$ and $e\not\in W\cup\ominus$ imply $sup(s)\ledge{sig(e)}sup(s')\in A_\tau$,
then there is a $\tau$-region $R=(sup', sig')$ of $B_G$ that preserves $sup$ and $sig$ as follows:

* For all $s\in S(B_G)$, if $s\not\in \bot$ then $sup'(s)=sup(s)$, otherwise $sup'(s)=0$.

* For all $e\in E'$, if $e\not\in W\cup\ominus$ then $sig'(e)=sig(e)$;
if $e\in \ominus$, then $sig(e)=\nop$;
if $i \in \{0,\dots, m-1\}$ and $e=w_i$, if $sup(t_{i,0})=0$ then $sig(e)=\nop$, otherwise $sig(e)=\swap$.

We argue that $s\edge{e}s'\in B_G$ implies $sup'(s)\ledge{sig'(e)}sup'(s')\in \tau$.
If $e\in W\cup\ominus$, then this is easy to see, since $sup'(\bot_i)=0$ for all $i\in \{0,\dots, m-1\}$.
For $e\not\in W\cup\ominus$, the claim follows by the assumptions about $sup$ and $sig$.

By the next lemma, a $\tau$-region of $T_i'$, where $T_i'$ is considered as a TS, whose signature gets along with $\nop$ and $\swap$ is always extendable to a region of $B_G$:

Let $i\in \{0,\dots, m-1\}$.
Let $sup: S(T_i') \rightarrow \{0,1\}$ and $sig: E(T_i') \rightarrow \{\nop,\swap\}$ be mappings such that $s\edge{e}s'\in T_i'$ implies $sup(s)\ledge{sig(e)}sup(s')\in \tau$.
There is a $\tau$-region $R=(sup', sig')$ of $B_G$ such that $sup'(s)=sup(s)$ and $sig'(e)=sig(e)$ for all $s\in S(T_i')$ and $e\in E(T_i')$.

By Lemma <ref>, it suffices to argue that $sup$ and $sig$ are consistently extendable to
$T_0',\dots T_{i-1}',$ $T_{i+1}',\dots, T_{m-1}'$.
Let $j\in \{0,\dots, m-1\}\setminus\{i\}$, be arbitrary but fixed,

and let $T_j'=t_{j,0}\edge{e_{j,1}}t_{j,1}\edge{e_{j,2}}t_{j,2}\edge{e_{j,3}}t_{j,3}\edge{e_{j,4}}t_{j,4}$, where $e_{j,1},\dots,e_{j,4}\in E(T_j')$ in accordance to the definition of $B_G$.
We obtain $R=(sup',sig')$ as follows.
For all $e\in E(B_G)\setminus (W\cup\ominus)$, if $e\in E(T_i')$, then $sig'(e)=sig(e)$ and otherwise $sig(e)=\nop$;
for all $s\in S(T_i')$, we define $sup'(s)=sup(s)$;
for all $j\in \{0,\dots, m-1\}\setminus\{i\}$, we define $sup(t_{j,0})=0$ and inductively $sup(t_{j,\ell})=\delta_G(sup(t_{j,\ell-1}), e_{j,\ell})$ for all $\ell\in \{1,\dots,4\}$.
Since $sig$ maps to $\{\nop,\swap\}$, so does $sig'$.
Thus, if $s\edge{e}s'\in T_j'$, then $sup'(s)\ledge{sig'(e)}sup'(s')\in A_\tau$.
Since j was arbitrary, this proves the lemma.

The TS $B_G$ has the $\tau$-SSP.

It is easy to see that $(\bot_i,s)$ is $\tau$-solvable for all $i\in \{0,\dots,m-1\}$ and all $s\in S(B_G)\setminus \{\bot_i\}$:
one may choose $sup(\bot_i)=1$, $sup(s)=0$ if $s\neq\bot_i$, $sig(e)=\swap$ if $\edge{e}\bot_i$ or $\bot_i\edge{e}$, $sig(e)=\nop$ otherwise.

Similarly, the atom $(s,s')$ where $s\in S(T_i')$ and $s'\in S(B_G)\setminus S(T_i')$ is $\tau$-solvable for all $i\in \{0,\dots, m-1\}$:
one may choose $sup(s)=1$ if $s\in S(T_i)$ and $0$ otherwise, $sig(e)=\swap$ if $e=w_i$ and $\nop$ otherwise.

Thus, it remains to argue that an atom $(s, s')$ is also solvable if $s\not=s'\in S(T_i')$, for all $i\in \{0,\dots, m-1\}$.
By Lemma <ref>, it suffices to present corresponding regions for $T_i'$.

Let $i\in \{0,\dots, m-1\}$ be arbitrary but fixed, and, for a start, let's consider the case where $v_{i_0}\in M$ and $v_{i_1}\not\in M$.
That is, $T_i'=t_{i,0}\Edge{v_{i_0}'}t_{i,1}\Edge{v_{i_1}}t_{i,2}\Edge{v_{i_0}}t_{i,2}\Edge{v_{i_1}}t_{i,4}$.
For all $\ell\in \{1,2,3\}$, let $R_\ell=(sup_\ell, sig_\ell)$ be a pair of mappings $sup_\ell:S(T_i')\rightarrow \{0,1\}$, $sig_\ell:E(T_i')\rightarrow \{\nop,\swap\}$, (implicitly) defined by $sup_1(t_{i,0})=0$, $sig_1(v_{i_0}')=sig_1(v_{i_0})=\nop$ and $sig_1(v_{i_1})=\swap$;
and $sup_2(t_{i,0})=0$, $sig_2(v_{i_0}')=sig_2(v_{i_1})=\nop$ and $sig_2(v_{i_0})=\swap$;
and $sup_3(t_{i,0})=0$, $sig_3(v_{i_0})=sig_3(v_{i_1})=\nop$ and $sig_3(v_{i_0}')=\swap$.
The images of $T_i'$ under $R_1,R_2$ and $R_3$ are as follows:

\begin{align*}
\textcolor{white}{ and } {T_i'}^{R_2}=0\ledge{\nop}0\ledge{\nop}0\ledge{\swap}1\ledge{\nop}1\\
\end{align*}

By Lemma <ref>, $R_\ell$ can be extended to a $\tau$-region of $B_G$ that preserves $sup$ for all $\ell\in \{1,2,3 \}$.
Moreover, obviously, for every SSP atom $(s,s')$ of $T_i'$, there is an $\ell\in \{1,2,3\}$ such that $sup_\ell(s)\not= sup_\ell(s')$.
Thus, $(s,s')$ is $\tau$-solvable in $B_G$.

The arguments for the case $v_{i_0}\not\in M$ and $v_{i_1}\in M$ is similar (the situation is symmetrical);
the case  $v_{i_0},v_{i_1}\in M$ is simpler since no two events are the same.

By the arbitrariness of $i$, this proves the lemma.

§.§ The Proof of Theorem <ref>(<ref>) when $\tau\cap\{\inp,\out\}\not=\emptyset$

Let $\tau=\{\nop,\swap\}\cup\omega$ be a type of nets such that $\omega\subseteq\{\inp,\out,\used,\free\}$ and $\omega\cap\{\inp,\out\}\not=\emptyset$, and let $A_G$ and $\kappa$ be defined as in Section <ref>.

If there is an $E'$-label-splitting $B_G$ of $A_G$ such that $\vert E'\vert\leq \kappa$ that has the $\tau$-ESSP, then $G$ has a $\lambda$-vertex cover.

Let $i\in \{0,\dots, m-1\}$ be arbitrary but fixed and $\mL$ be the set of events of $A_G$ that occur split in $B_G$.
If $R=(sup, sig)$ is a $\tau$-region of $A_G$, then $sup(t_{i,0})=sup(t_{i,4})$ by Lemma <ref>.
Thus, $\alpha_i=(v_{i_0}, t_{i,4})$ is not $\tau$-solvable, since $sup(t_{i,0})\lEdge{sig(v_{i_0})}$ implies $sup(t_{i,4})\lEdge{sig(v_{i_0})}$.
On the other hand, $B_G$ has the $\tau$-ESSP, implying the $\tau$-solvability of $\alpha_i$.
This implies $\{v_{i_0}, v_{i_1}\}\cap\mL\not=\emptyset$.
Since $i$ was arbitrary, this is  true for all $T_0,\dots, T_{m-1}$.
Thus, just like for Lemma <ref>, we get that $\Ss=\mL\cap \U$ defines a $\lambda$-VC of $G$.
This proves the lemma.

Conversely, let $\Ss$ be a $\lambda$-VC of $G$, and $B_G$ be the $E'$-label-splitting of $A_G$ as defined in Section <ref>.
By the following lemma, $B_G$ has an exact net realization:

The TS $B_G$ has the $\tau$-SSP, and the $\tau$-ESSP.

By Lemma <ref>, the TS $B_G$ has the $\tau$-SSP.
It remains to argue for the $\tau$-ESSP.
Without loss of generality, we assume that $\inp\in\tau$ and present $\tau$-regions $R=(sup, sig)$ that get along with $\nop,\inp$ and $\swap$.
Indeed, if $\inp\not\in \tau$, then $\out\in \tau$ and one gets corresponding (complement) regions $R'=(sup', sig')$ simply by $sup'(s)=1-sup(s)$, $sig'(e)=sig(e)$ if $sig(e)\in \{\nop,\swap\}$, and $sig'(e)=\out$ if $sig(e)=\inp$ for all $s\in S(B_G)$ and all $e\in E'$.

The general idea to solve an ESSA $(e,s)$ is to choose $sup(s)=0$, $sig(e)=\inp$,
and $sig(e')\in\{\nop,\swap\}$ as needed, and $sup(s')$ accordingly for the other events $e'$, and states $s'$ of $A_G$.
For instance, if $e\in W \cup\ominus$, one may choose $sup(s')=1$ if $s'\edge{e}$ and $sup(s')=0$ otherwise; $sig(e)=\inp$, $sig(e')=\swap$ when $e'$ leads to or originates from the unique state with support $1$, and $\nop$ otherwise:
all the ESSAs $(e,s)$ will then be solved.

For the other events, we proceed as follows.
Let $v$ be some node of the graph $G$.

If $v\not\in \Ss$, it may only occur in at most three paths of $B_G$ of the form

$T_i' =t_{i,0}\Edge{v}t_{i,1}\Edge{v_{i}}t_{i,2}\Edge{v}t_{i,3}\Edge{v_{i}'} t_{i,4}$ or $T_i' =t_{i,0}\Edge{v_{i}'}t_{i,1}\Edge{v}t_{i,2}\Edge{v_{i}}t_{i,3}\Edge{v} t_{i,4}$, since the companion vertex $v_i$ must be in $\Ss$; moreover, if $v$ belongs to several edges of $B_G$, all the corresponding companions must be different. Also, $v$ occurs twice, with a $v_i$ in between.
We may thus choose $sig(v)=\inp$, $sup(s)=1$ and $sup(s')=0$ if $s\edge{v}s'$, $sig(e)=\swap$ if $\edge{e}s$, in each path $T'_i$ containing $v$.
All the other events will have a signature $\nop$.
For any $T'_j$ not containing $v$, hence only containing signatures $\nop$ and $\swap$, the latter will introduce states with support $1$ while we would like to have supports $0$ to exclude $v$;
if this occurs, we shall thus consider two choices for the support of $t_{j,0}$: 0 (region $R_0$) and 1 (region $R_1$, with $sig(w_j)=\swap$); then the corresponding supports for the various $t_{j,\ell}$ will be complementary too.
In any case, we shall get regions separating $v$ from all the needed states.

[new set = import nodes]
[nodes=set=import nodes]
(bot1) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 1,3 [red!20] (ı) circle (0.3cm);
(bot1) at (bot1) $\bot_0$;
ıin 0,...,4 (ı) at (ı) $t_{0,\i}$;

(import nodes);

[yshift=-1cm, nodes=set=import nodes]
(bot2) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 1,2 [red!20] (ı) circle (0.3cm);
(bot2) at (bot2) $\bot_1$;
ıin 0,...,4 (ı) at (ı) $t_{1,\i}$;

(import nodes);

[yshift=-2cm, nodes=set=import nodes]
(bot3) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 1,2 [red!20] (ı) circle (0.3cm);
(bot3) at (bot3) $\bot_2$;
ıin 0,...,4 (ı) at (ı) $t_{2,\i}$;

(import nodes);

[yshift=-3cm, nodes=set=import nodes]
(bot4) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 0,2 [red!20] (ı) circle (0.3cm);
(bot4) at (bot4) $\bot_3$;
ıin 0,...,4 (ı) at (ı) $t_{3,\i}$;

(import nodes);

[yshift=-4cm,nodes=set=import nodes]
(bot5) at (0,0);
(bot5) at (0,0) $\bot_4$;
ıin 0,...,4  (ı) at (1.8cm+ ı*1.8cm,0) ;
ıin 3,4 [red!20] (ı) circle (0.3cm);
ıin 0,...,4  (ı) at (ı) $t_{4,\i}$;

(import nodes);

(bot1) edge [->] node[left] $\ominus_1$  (bot2);
(bot2) edge [->] node[left] $\ominus_2$  (bot3);
(bot3) edge [->] node[left] $\ominus_3$  (bot4);
(bot4) edge [->] node[left] $\ominus_4$  (bot5);

Region $R_0=(sup,sig)$ for $v=v_1$. $v$ occurs in $T'_0$ and $T'_3$. The supports of $t_{1,0},t_{2,0},t_{4,0}$ are chosen 0. The colored nodes have support 1, otherwise 0. When not indicated, signatures are $\nop$.

[new set = import nodes]
[nodes=set=import nodes]
(bot1) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 1,3 [red!20] (ı) circle (0.3cm);
(bot1) at (bot1) $\bot_0$;
ıin 0,...,4 (ı) at (ı) $t_{0,\i}$;

(import nodes);

[yshift=-1cm, nodes=set=import nodes]
(bot2) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 0,3,4 [red!20] (ı) circle (0.3cm);
(bot2) at (bot2) $\bot_1$;
ıin 0,...,4 (ı) at (ı) $t_{1,\i}$;

(import nodes);

[yshift=-2cm, nodes=set=import nodes]
(bot3) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 0,3,4 [red!20] (ı) circle (0.3cm);
(bot3) at (bot3) $\bot_2$;
ıin 0,...,4 (ı) at (ı) $t_{2,\i}$;

(import nodes);

[yshift=-3cm, nodes=set=import nodes]
(bot4) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 0,2 [red!20] (ı) circle (0.3cm);
(bot4) at (bot4) $\bot_3$;
ıin 0,...,4 (ı) at (ı) $t_{3,\i}$;

(import nodes);

[yshift=-4cm,nodes=set=import nodes]
(bot5) at (0,0);
(bot5) at (0,0) $\bot_4$;
ıin 0,...,4  (ı) at (1.8cm+ ı*1.8cm,0) ;
ıin 0,1,2 [red!20] (ı) circle (0.3cm);
ıin 0,...,4  (ı) at (ı) $t_{4,\i}$;

(import nodes);

(bot1) edge [->] node[left] $\ominus_1$  (bot2);
(bot2) edge [->] node[left] $\ominus_2$  (bot3);
(bot3) edge [->] node[left] $\ominus_3$  (bot4);
(bot4) edge [->] node[left] $\ominus_4$  (bot5);

Region $R_1=(sup,sig)$ for $v=v_1$. $v$ occurs in $T'_0$ and $T'_3$. The supports of $t_{1,0},t_{2,0},t_{4,0}$ are chosen 1. The colored nodes have support 1, otherwise 0. When not indicated, signatures are $\nop$.

If $v\in \Ss$, it may only occur in at most three paths of $B_G$ of the form

$T_i' =t_{i,0}\Edge{v'}t_{i,1}\Edge{v_{i}}t_{i,2}\Edge{v}t_{i,3}\Edge{v_{i}} t_{i,4}$ or $T_i' =t_{i,0}\Edge{v_{i}}t_{i,1}\Edge{v}t_{i,2}\Edge{v_{i}}t_{i,3}\Edge{v'} t_{i,4}$, or $T_i' =t_{i,0}\Edge{v}t_{i,1}\Edge{v_{i}}t_{i,2}\Edge{v'}t_{i,3}\Edge{v'_{i}} t_{i,4}$ or $T_i' =t_{i,0}\Edge{v_{i}}t_{i,1}\Edge{v}t_{i,2}\Edge{v'_{i}}t_{i,3}\Edge{v'} t_{i,4}$, depending on the fact that the companion vertex $v_i$ belongs to $\Ss$ or not.
Again, if $v$ belongs to several edges, all the corresponding companions must be different.
Also, $v$ occurs only once, as well as $v'$.
For $v$, we may thus choose $sig(v)=\inp$, $sup(s)=1$ and $sup(s')=0$ if $s\edge{v}s'$, $sig(e)=\swap$ if $\edge{e}s$, in each path $T'_i$ containing $v$.
All the other events will have a signature.
For any $T'_j$ not containing $v$, we may have some events with signature $\swap$, hence some states with support $1$ while we would like to only have supports $0$ in order to exclude $v$;
hence, if needed, we shall again consider two choices for the support of $t_{j,0}$: 0 (region $R_2$) and 1 (region $R_3$);
then the corresponding supports for the various $t_{j,\ell}$ will be complementary too.
In any case, we shall get regions separating $v$ from all the needed states.
However, for the first two kinds of configuration, since $v$ is between two $v_i$'s, after the second $v_i$ (with signature $\swap$), we shall have states with support $1$ after $v$, while we would like to have supports $0$ to exclude $v$;
hence we will also use a region where $w_i$ has signature $\swap$ and $v_i$ has signature $\nop$ (region $R_3$).
Note that, in this case, no event in any $T'_j$ not containing $v$ has a signature $\swap$ and all the states have support $0$;
hence we do not need here to introduce an additional region with $sig(w_j)=\swap$ to get complementary supports.
In any case, we shall get regions separating $v$ from all the needed states.

For $v'$, we proceed similarly.

[new set = import nodes]
[nodes=set=import nodes]
(bot1) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 2,4 [red!20] (ı) circle (0.3cm);
(bot1) at (bot1) $\bot_0$;
ıin 0,...,4 (ı) at (ı) $t_{0,\i}$;

(import nodes);

[yshift=-1cm, nodes=set=import nodes]
(bot2) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 0 [red!20] (ı) circle (0.3cm);
(bot2) at (bot2) $\bot_1$;
ıin 0,...,4 (ı) at (ı) $t_{1,\i}$;

(import nodes);

[yshift=-2cm, nodes=set=import nodes]
(bot3) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 2,4 [red!20] (ı) circle (0.3cm);
(bot3) at (bot3) $\bot_2$;
ıin 0,...,4 (ı) at (ı) $t_{2,\i}$;

(import nodes);

[yshift=-3cm, nodes=set=import nodes]
(bot4) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 1,2 [red!20] (ı) circle (0.3cm);
(bot4) at (bot4) $\bot_3$;
ıin 0,...,4 (ı) at (ı) $t_{3,\i}$;

(import nodes);

[yshift=-4cm,nodes=set=import nodes]
(bot5) at (0,0);
(bot5) at (0,0) $\bot_4$;
ıin 0,...,4  (ı) at (1.8cm+ ı*1.8cm,0) ;
ıin 2,3 [red!20] (ı) circle (0.3cm);
ıin 0,...,4  (ı) at (ı) $t_{4,\i}$;

(import nodes);

(bot1) edge [->] node[left] $\ominus_1$  (bot2);
(bot2) edge [->] node[left] $\ominus_2$  (bot3);
(bot3) edge [->] node[left] $\ominus_3$  (bot4);
(bot4) edge [->] node[left] $\ominus_4$  (bot5);

Region $R_2=(sup,sig)$ for $v=v_0$. $v$ occurs in $T'_0$, $T'_1$ and $T'_2$. The supports of $t_{3,0},t_{4,0}$ are chosen 0.
The colored nodes have support 1, otherwise 0. When not indicated, signatures are $\nop$.

[new set = import nodes]
[nodes=set=import nodes]
(bot1) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 0,1,2 [red!20] (ı) circle (0.3cm);
(bot1) at (bot1) $\bot_0$;
ıin 0,...,4 (ı) at (ı) $t_{0,\i}$;

(import nodes);

[yshift=-1cm, nodes=set=import nodes]
(bot2) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 0 [red!20] (ı) circle (0.3cm);
(bot2) at (bot2) $\bot_1$;
ıin 0,...,4 (ı) at (ı) $t_{1,\i}$;

(import nodes);

[yshift=-2cm, nodes=set=import nodes]
(bot3) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 0,1,2 [red!20] (ı) circle (0.3cm);
(bot3) at (bot3) $\bot_2$;
ıin 0,...,4 (ı) at (ı) $t_{2,\i}$;

(import nodes);

[yshift=-3cm, nodes=set=import nodes]
(bot4) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
(bot4) at (bot4) $\bot_3$;
ıin 0,...,4 (ı) at (ı) $t_{3,\i}$;

(import nodes);

[yshift=-4cm,nodes=set=import nodes]
(bot5) at (0,0);
(bot5) at (0,0) $\bot_4$;
ıin 0,...,4  (ı) at (1.8cm+ ı*1.8cm,0) ;
ıin 0,...,4  (ı) at (ı) $t_{4,\i}$;

(import nodes);

(bot1) edge [->] node[left] $\ominus_1$  (bot2);
(bot2) edge [->] node[left] $\ominus_2$  (bot3);
(bot3) edge [->] node[left] $\ominus_3$  (bot4);
(bot4) edge [->] node[left] $\ominus_4$  (bot5);

Region $R_3=(sup,sig)$ for $v=v_0$.
$v$ occurs in $T'_0$, $T'_1$ and $T'_2$.
The supports of $t_{3,0},t_{4,0}$ are chosen 0.
The colored nodes have support 1, otherwise 0.
When not indicated, signatures are $\nop$.
Note that here no $v_i$ with $i\neq 0$ needs to have a signature $\swap$;
hence we do not need to add a region with signature $\swap$ for $w_j$ when $T'_j$ does not contain $v$.

This proves the lemma.

§.§ The Proof of Theorem <ref>(<ref>), when  $\tau\cap\{\inp,\out\}=\emptyset$

Since we already handled the case $\tau=\{\nop,\swap\}$, we may assume $\tau=\{\nop,\swap\}\cup\omega$ with $\emptyset\not=\omega\subseteq \{\used,\free\}$.
Then, if we have to solve an ESSA $(e,s)$, we have to try to find a $\tau$-region where $sig(e)=\used$ and $\sup(s)=0$, or  $sig(e)=\free$ and $\sup(s)=1$, but if $s'\edge{e}s\edge{\neg e}$, in either case $sup(s')=sup(s)$ and we may not solve $(e,s)$.

Thus, there is no $E'$-label-splitting of the TS $A_G$ of Section <ref>, that has the $\tau$-ESSP.
To overcome this obstacle, with as little effort as possible, we shall use transition systems $\overline{A}_G$ and $\overline{B}_G$ which extend $A_G$ and $B_G$ by backward-edges (see Figure <ref>).

For all $i\in \{0,\dots, m-1\}$, the current TS $A_G$ has the following bi-directed path $T_i$:

[new set = import nodes, scale =0.8]

[nodes=set=import nodes]
(T) at (-0.75,0) $T_i=$;
ıin 0,...,4  (ı) at (ı*2cm, 0) ;
ıin 0,...,4  (ı) at (ı) $t_{i,\i}$;
(import nodes);
0 <->["$v_{i_0}$"]1<->["$v_{i_1}$"]2<->["$v_{i_0}$"]3<->["$v_{i_1}$"]4;

Moreover, the TS $A_G$ has, for all $i\in \{0,\dots, m-1\}$, the bi-directed edge $\bot_i\fbedge{w_i}t_{i,0}$; and, for all $i \in \{0,\dots, m-2\}$, the bi-directed edge $\bot_{i}\fbedge{\ominus_{i+1}}\bot_{i+1}$ to join the paths $T_0,\dots, T_{m-1}$.
Again, $A_G$ has $n+2m-1$ events, and we define $\kappa=n+2m-1+\lambda$.

[new set = import nodes]
[nodes=set=import nodes]
(bot1) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
(bot1) at (bot1) $\bot_0$;
ıin 0,...,4 (ı) at (ı) $t_{0,\i}$;

(import nodes);

[yshift=-1cm, nodes=set=import nodes]
(bot2) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
(bot2) at (bot2) $\bot_1$;
ıin 0,...,4 (ı) at (ı) $t_{1,\i}$;

(import nodes);

[yshift=-2cm, nodes=set=import nodes]
(bot3) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
(bot3) at (bot3) $\bot_2$;
ıin 0,...,4 (ı) at (ı) $t_{2,\i}$;

(import nodes);

[yshift=-3cm, nodes=set=import nodes]
(bot4) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
(bot4) at (bot4) $\bot_3$;
ıin 0,...,4 (ı) at (ı) $t_{3,\i}$;

(import nodes);

[yshift=-4cm,nodes=set=import nodes]
(bot5) at (0,0);
(bot5) at (0,0) $\bot_4$;
ıin 0,...,4  (ı) at (1.8cm+ ı*1.8cm,0) ;
ıin 0,...,4  (ı) at (ı) $t_{4,\i}$;

(import nodes);

(bot1) edge [<->] node[left] $\ominus_1$  (bot2);
(bot2) edge [<->] node[left] $\ominus_2$  (bot3);
(bot3) edge [<->] node[left] $\ominus_3$  (bot4);
(bot4) edge [<->] node[left] $\ominus_4$  (bot5);

[new set = import nodes]
[nodes=set=import nodes]
(bot1) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
(bot1) at (bot1) $\bot_0$;
ıin 0,...,4 (ı) at (ı) $t_{0,\i}$;

(import nodes);

[yshift=-1cm, nodes=set=import nodes]
(bot2) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
(bot2) at (bot2) $\bot_1$;
ıin 0,...,4 (ı) at (ı) $t_{1,\i}$;

(import nodes);

[yshift=-2cm, nodes=set=import nodes]
(bot3) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
(bot3) at (bot3) $\bot_2$;
ıin 0,...,4 (ı) at (ı) $t_{2,\i}$;

(import nodes);

[yshift=-3cm, nodes=set=import nodes]
(bot4) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
(bot4) at (bot4) $\bot_3$;
ıin 0,...,4 (ı) at (ı) $t_{3,\i}$;

(import nodes);

[yshift=-4cm,nodes=set=import nodes]
(bot5) at (0,0);
(bot5) at (0,0) $\bot_4$;
ıin 0,...,4  (ı) at (1.8cm+ ı*1.8cm,0) ;
ıin 0,...,4  (ı) at (ı) $t_{4,\i}$;

(import nodes);

(bot1) edge [<->] node[left] $\ominus_1$  (bot2);
(bot2) edge [<->] node[left] $\ominus_2$  (bot3);
(bot3) edge [<->] node[left] $\ominus_3$  (bot4);
(bot4) edge [<->] node[left] $\ominus_4$  (bot5);

The new transition systems  $\overline{A}_G$ (top) and  $\overline{B}_G$ (bottom) that originate from Example <ref>.

If there is a $E'$-label-splitting of $\overline{A}_G$ such that $\vert E'\vert\leq \kappa$ that has the $\tau$-ESSP, then $G$ has a $\lambda$-vertex cover.

The proof is similar to the one of Lemma <ref>.

Conversely, let $\Ss$ be a $\lambda$-VC of $G$, and let $\overline{B}_G=(S(B_G),E', \delta'', \bot_0)$ be the bi-directed extension of the TS $B_G=(S(B_G), E',\delta',\bot_0)$, which has been defined in Section <ref>.
That is, for all $s,s'\in S(B_G)$ and all $e\in E'$ if $\delta'(s,e)=s'$, then $\delta''(s,e)=s'$ and $\delta''(s',e)=s$.
To complete the proof of Theorem <ref>.2 it remains to argue that $\overline{B}_G$ has the $\tau$-ESSP and the $\tau$-SSP.
Recall that the signatures of the regions that have been presented for the proof of Lemma <ref> get along with $\nop$ and $\swap$.
Thus, they can be directly applied to $\overline{B}_G$, which proves $\overline{B}_G$'s $\tau$-SSP.
Hence, it remains to argue for $\overline{B}_G$'s ESSP.
The following lemma confirms both properties for $\overline{B}_G$ and thus completes the proof of Theorem <ref>.

The TS $\overline{B}_G$ has the $\tau$-SSP, and the $\tau$-ESSP.

First, we may observe that the signatures of the regions that have been presented for the proof of Lemma <ref> get along with $\nop$ and $\swap$.
Thus, they can be directly applied to $\overline{B}_G$, which proves $\overline{B}_G$'s $\tau$-SSP.

We now argue that $\overline{B}_G$ has the $\tau$-ESSP.
Without loss of generality, we assume $\used\in \tau$.
(Otherwise $\free\in \tau$ and this case is similar.)
We thus have to find, for each ESSA $(e,s)$, a region $R=(sup,sig)$ such that $sig(e)=\used$ and $sup(s)=0$.
The proof is very similar to the one for Lemma <ref>.

For instance, if $e\in W \cup\ominus$, one may choose $sup(s')=1$ if $s'\edge{e}$ and $sup(s')=0$ otherwise;
$sig(e)=\used$, $sig(e')=\swap$ when $e'$ leads to or originates from the unique state with support $1$, and $\nop$ otherwise:
all the ESSAs $(e,s)$ will then be solved.
For the other events, we proceed as follows.

Let $v$ be some node of the graph $G$.

If $v\not\in \Ss$, it may only occur in at most three edges of $G$ (in each case, the companion vertex must be in $\Ss$, and if $v$ belongs to several edges of $G$, all the corresponding companions must be different), which leads to the two kinds of decorated paths in $\overline{B}_G$:

$\bot_i:0\FBedge{w_i:\swap}t_{i,0}:1\FBedge{v:\used}t_{i,1}:1\FBedge{v_{i}:\nop}t_{i,2}:1\FBedge{v:\used}t_{i,3}:1\FBedge{v_{i}':\swap} t_{i,4}:0$

or $t_{i,0}:0\FBedge{v_{i}':\swap}t_{i,1}:1\FBedge{v:\used}t_{i,2}:1\FBedge{v_{i}:\nop}t_{i,3}:1\FBedge{v:\used} t_{i,4}:1$.

For any $T'_j$ not containing $v$, hence only containing signatures $\nop$ and $\swap$, this may introduce states with support $1$ while we would like to have supports $0$ to exclude $v$;
if this occurs, we may consider two choices for the support of $t_{j,0}$: 0 (region $R_0$) and 1 (region $R_1$, with $sig(w_j)=\swap$);
then the corresponding supports for the various $t_{j,\ell}$ will be complementary too.
In any case, we shall get regions separating $v$ from all the needed states.

If $v\in \Ss$, this leads us to four kinds of decorated paths in $\overline{B}_G$, depending on the fact that the companion vertex $v_i$ belongs to $\Ss$ or not, and if $v$ is smaller than $v_i$ or not:

$t_{i,0}:0\FBedge{v':\nop}t_{i,1}:0\FBedge{v_{i}:\swap}t_{i,2}:1\FBedge{v:\used}t_{i,3}:1\FBedge{v_{i}:\swap} t_{i,4}:0$

or $t_{i,0}:0\FBedge{v_{i}:\swap}t_{i,1}:1\FBedge{v:\used}t_{i,2}:1\FBedge{v_{i}:\swap}t_{i,3}:0\FBedge{v':\nop} t_{i,4}:0$

or $\bot_i:0\FBedge{w_i:\swap}t_{i,0}:1\FBedge{v:\used}t_{i,1}:1\FBedge{v_{i}:\swap}t_{i,2}:0\FBedge{v':\nop}t_{i,3}:0\FBedge{v'_{i}:\nop} t_{i,4}:0$

or $t_{i,0}:0\FBedge{v_{i}:\swap}t_{i,1}:1\FBedge{v:\used}t_{i,2}:1\FBedge{v'_{i}:\swap}t_{i,3}:0\FBedge{v':\nop} t_{i,4}:0$.

Again, if $v$ belongs to several edges, all the corresponding companions must be different.
Also, $v$ occurs only once, as well as $v'$.
For any $T'_j$ not containing $v$, we may have some events with signature $\swap$ (the other ones having $\nop$), hence some states with support $1$ while we would like to only have supports $0$ in order to exclude $v$;
hence, if needed, we shall again consider two choices for the support of $t_{j,0}$: 0 (region $R_2$) and 1(region $R_3$);
then the corresponding supports for the various $t_{j,\ell}$ will be complementary too.
In any case, we shall get regions separating $v$ from all the needed states.

For $v'$, we proceed similarly.

Altogether, by the arbitrariness of $v$, we proved the $\tau$-ESSP for $\overline{B}_G$ and this thus completes the proof of Lemma <ref>.

§ THE COMPLEXITY OF EDGE REMOVAL

In order to make a TS implementable, i.e., to satisfy SSP and/or ESSP, the removal of edges can also be an appropriate way of modification:

Let $A=(S,E,\delta,\iota)$ be a TS.
A TS  $B=(S, E,\delta',\iota)$ is an edge-removal of $A$ if, for all $e\in E'$ and all $s,s'\in S'$, holds: if $s\edge{e}s'\in B$, then $s\edge{e}s'\in A$.
By $\K=\{s\edge{e}s'\in A\mid s\edge{e}s'\not\in B\}$ we refer to the (set of) removed edges.

We would like to emphasize that $B$, and $A$ have the same set of states, and events.
Moreover, $B$ is a valid system, i.e., each state remains reachable from the initial one and each event occurs at least once in $\delta'$.

$\tau$-Edge-Removal for Embedding
A TS  $A=(S,E,\delta,\iota)$, a natural number $\kappa$.
Does there exist an edge-removal $B$ for $A$ by $\K$ that has the $\tau$-SSP and satisfies $\vert\K\vert\leq \kappa$?

$\tau$-Edge-Removal for Language-Simulation
A TS  $A=(S,E,\delta,\iota)$, a natural number $\kappa$.
Does there exist an edge-removal $B$ for $A$ by $\K$ that has the $\tau$-ESSP and satisfies $\vert\K\vert\leq \kappa$?

$\tau$-Edge-Removal for Realization
A TS  $A=(S,E,\delta,\iota)$, a natural number $\kappa$.
Does there exist an edge-removal $B$ for $A$ by $\K$ that has the $\tau$-ESSP and the $\tau$-SSP and satisfies $\vert\K\vert\leq \kappa$?

The following theorem characterizes the complexity of edge removal for all implementations and types under consideration:

If $\omega\subseteq\{\inp,\out, \free,\used\}$, and $\tau=\{\nop,\swap\}\cup\omega$, then

$\tau$-Edge Removal for Embedding is NP-complete.

$\tau$-Edge Removal for Language Simulation, and

$\tau$-Edge Removal for Realization are NP-complete if $\omega\not=\emptyset$, otherwise they are solvable in polynomial time.

First of all, we argue for the polynomial part:
If $\tau=\{\nop,\swap\}$, then a TS $A=(S,E,\delta,\iota)$ has the $\tau$-ESSP if and only if every event occurs at every state,
since the functions , are defined on both $0$ and $1$.
Thus, any ESSP atom $(e,s)$ of $A$ would be unsolvable.
This implies that an edge-removal may neither render nor keep the $\tau$-ESSP valid, since the removal of an edge would produce an unsolvable ESSA.
Hence, the decision problems are polynomial, since either $A$ is already implementable, which can be checked in polynomial time [21], or it has to be rejected.
Thus, for the proof of Theorem <ref>, it remains to consider the NP-completeness results.

In order to prove Theorem <ref>,  we present suitable reductions of 3BVC, where we reduce an input $G=(\U,M)$ to an instance $(A_G,\kappa)$, such that $G$ has a vertex cover of size at most $\lambda$ if and only if $A_G$ allows an implementable edge removal $B_G$ that satisfies $\vert \K\vert\leq \kappa$.
However, due to their different ability to solve ESSAs, when it comes to language simulation or realization, we have to distinguish again between the types $\tau$ that have at least one of $\inp$ or $\out$, and the ones that do not have any of them.

§.§ The Proof of Theorem <ref>(<ref>), and the Proof of  Theorems <ref>(<ref>) for the Types with  or

In this section, we shall prove Theorem <ref>(<ref>) for all types $\tau=\{\nop,\swap\}\cup\omega$ with $\omega\subseteq\{\inp, \out, \free, \used\}$, and we prove Theorems <ref>(<ref>) for the types that additionally satisfy $\omega\cap\{\inp,\out\}\not=\emptyset$.
We deal with these proofs simultaneously, since they get along with the same reduction.
In particular, according to our general approach, we start from an input $(G, \lambda)$ of 3BVC, and construct an instance TS $(A_G, \kappa)$ as follows:

If $\tau=\{\nop,\swap\}\cup\omega$ with $\omega\subseteq\{\inp, \out, \free, \used\}$, then $A_G$ allows an edge-removal $B_G$ that respects $\kappa$, and has the $\tau$-SSP if and only if $G$ has a $\lambda$-vertex-cover;

If $\tau=\{\nop,\swap\}\cup\omega$ with $\omega\subseteq\{\inp, \out, \free, \used\}$, and $\omega\cap\{\inp,\out\}\not=\emptyset$, then $A_G$ allows an edge-removal $B_G$ that respects $\kappa$, and has the $\tau$-ESSP if and only if $G$ has a $\lambda$-vertex-cover.

Hence, in the remainder of this section, as long as not stated explicitly otherwise, let $\tau=\{\nop,\swap\}\cup\omega$ with $\omega\subseteq\{\inp, \out, \free, \used\}$, whenever we deal with the $\tau$-SSP,  and let additionally $\omega\cap\{\inp,\out\}\not=\emptyset$, whenever we deal with the $\tau$-ESSP (where the TS in question is clear from the context).

We now define the announced instance $(A_G,\kappa)$.
First of all, $\kappa=\lambda$.
Moreover, for every $i\in \{0,\dots, m-1\}$, the TS $A_G$ has the following path $T_i$, that uses the vertices of $\mathfrak{e}_i=\{v_{i_0}, v_{i_1}\}$ (assuming $i_0<i_1$) as events:

[new set = import nodes]

[nodes=set=import nodes]
(T) at (-0.75,0) $T_i=$;
ıin 0,...,2  (ı) at (ı*2cm, 0) ;
ıin 0,...,2  (ı) at (ı) $t_{i,\i}$;
(import nodes);
0 ->["$v_{i_0}$"]1->["$v_{i_1}$"]2;

Furthermore, for every $i\in \{0,\dots, n-1\}$, the TS $A$ has the following gadget $F_i$ that uses the node $v_i$ as event, and, for all $j\in \{0,\dots, \kappa\}$, has an $a_j$-labeled edge which directs in the same direction as the $v_i$-labeled edge:

[new set = import nodes]
[xshift=7.5cm, nodes=set=import nodes]
(F) at (-0.75, 0) $F_i=$;
(0) at (0,0);
(1) at (3,0);
(0) at (0) $f_{i,0}$;
(1) at (1) $f_{i,1}$;
(dots) at (1.5,0.4) $\vdots$;

(import nodes);

0->[ swap, bend right=90,  "$v_j$"]1;
0->[swap, bend right =35, "$a_0$"]1;
0->[ bend right  =5, swap,"$a_1$"]1;
0->[swap, bend left =35,swap , "$a_{\kappa-1}$"]1;
0->[swap, bend left =90, swap, "$a_\kappa$"]1;

The TS $A_G$ has the initial state $\iota$;
for all $i\in \{0,\dots, m-1\}$, and all $j\in \{0,1,2\}$, it has the edge $\iota\edge{y_i^j}t_{i,j}$;
finally, for all $\ell\in \{0,\dots, n-1\}$, it has the edge $\iota\edge{z_\ell}f_{\ell,0}$.
The $y_i^j$-, and $z_\ell$-labeled edges serve to ensure reachability.
For the sake of simplicity, we summarize these events by $Y=\bigcup_{i=0}^{m-1}\{y_i^0,y_i^1,y_i^2\}\cup\{z_0,\dots, z_{n-1}\}$.

If there is an edge removal $B_G$ of $A_G$ that satisfies $\vert \K\vert \leq \kappa$, and has the $\tau$-SSP, respectively the $\tau$-ESSP, then there is a vertex cover of size at most $\lambda=\kappa$ for $G=(\U,M)$.

Let $B_G$ be an edge removal of $A_G$ that satisfies $\vert \K\vert \leq \kappa$, and has the $\tau$-SSP, respectively the $\tau$-ESSP, and let
$\Ss=\U\cap \{e\in E(A_G)\mid \exists s,s'\in S(A_G): s\edge{e}s'\in \K \}$ be the set of events of $A_G$ that label an edge of $A_G$ that is removed to obtain $B_G$.
First of all, we note that $\vert \Ss\vert \leq \vert \K\vert \leq \kappa=\lambda$.
Moreover, in the following, we will argue that $\Ss$ defines a vertex cover of $G$.

Let $i\in \{0,\dots, m-1\}$ be arbitrary but fixed.
We show that $\Ss\cap\{v_{i_0}, v_{i_1}\}\not=\emptyset$.
If $t_{i,0}\edge{v_{i_0}}t_{i,1}\in \K$ or $t_{i,1}\edge{v_{i_1}}t_{i,2}\in \K$, then we are finished.
Otherwise, since $B_G$ has the $\tau$-SSP, respectively the $\tau$-ESSP, there is a $\tau$-region $R=(sup, sig)$ that solves $(t_{i,0}, t_{i,2})$, respectively $(v_{i_0}, t_{i,2})$, and thus satisfies $sup(t_{i,0})\not=sup(t_{i,2})$.
This implies either $sup(t_{i,0})=sup(t_{i,1})$, and thus $sig(v_{i_0})\in \{\nop,\free,\used\}$, and $sig(v_{i_1})\in \{\inp, \out, \swap\}$, or $sup(t_{i,1})=sup(t_{i,2})$, and thus $sig(v_{i_0})\in \{\inp,\out, \swap\} $, and $sig(v_{i_1})\in \{\nop,\free,\used\}$.
We show that this implies $\K\cap\{f_{i_0}\edge{v_{i_0}}f_{i_0,1}, f_{i_1}\edge{v_{i_1}}f_{i_1,1}\}\not=\emptyset$:
Assume, for a contradiction, that the opposite is true.
Since $\vert \K\vert \leq \kappa$, there is a $j\in \{0,\dots, \kappa\}$, such that both $f_{i_0}\edge{a_j}f_{i_0,1}$, and $f_{i_1}\edge{a_j}f_{i_1,1}$ are present in $B_G$.
If $sig(v_{i_0})\in \{\nop,\free,\used\}$, and $sig(v_{i_1})\in \{\inp, \out, \swap\}$, we have $sup(f_{i_0,0})=sup(f_{i_0,1})$, and $sup(f_{i_1,0}) \not= sup(f_{i_1,1})$, which simultaneously implies $sig(a_j)\in \{\nop,\free,\used\}$, and $sig(a_j)\in \{\inp,\out,\swap\}$, which is a contradiction.
Hence, we have $\K\cap\{f_{i_0}\edge{v_{i_0}}f_{i_0,1}, f_{i_1}\edge{v_{i_1}}f_{i_1,1}\}\not=\emptyset$.
Analogously, if $sig(v_{i_0})\in \{\inp,\out, \swap\} $, and $sig(v_{i_1})\in \{\nop,\free,\used\}$, then we get $\K\cap\{f_{i_0}\edge{v_{i_0}}f_{i_0,1}, f_{i_1}\edge{v_{i_1}}f_{i_1,1}\}\not=\emptyset$ as well.

By the arbitrariness of $i$, this implies that $\Ss$ is a vertex cover of $G$.

For the converse direction, we have to show that the existence of a suitable vertex cover implies that $A_G$ has an implementable edge removal.
So let $\mS=\{v_{\ell_0},\dots, v_{\ell_{\lambda-1}}\}$ be a vertex cover of $G$, and let $B_G$ be the TS that originates from $A_G$ be removing the edge $f_{\ell_i,0}\edge{v_{\ell_i}}f_{\ell_i,1}$ for all $i\in \{0,\dots, \lambda-1\}$, and nothing else.
One easily verifies that $B_G$ is a well-defined reachable edge removal of $A_G$ that satisfies $\vert \K\vert \leq \kappa$.

In the following, we will show that $B_G$ has the  $\tau$-SSP as well as the $\tau$-ESSP, by presenting regions that altogether solve the individual separation atoms of $B_G$.
Let $I=\{t_{0,0},t_{1,0},\dots, t_{m-1,0}\}\cup\{f_{0,0}, f_{1,0},\dots, f_{n-1,0}\}$ be the set of the initial states of the gadgets of $B_G$, and $E=E(A_G)\setminus Y$ be the set of events in those gadgets (i.e., the vertices of $G$ and the $a_j$'s).

For the sake of simplicity, we often restrict the presentation of a region $R=(sup, sig)$ to the states of $I$ and the events of $E$.
This is justified, since we can easily extend $R$ to $B_G$, when this is possible.
choosing as we want $sup(\iota)$, for any $s\in I$ and $\iota\edge{e}s$ (then $e\in Y$ and is unique), we may choose $sig(e)=\nop$ if $sup(\iota)=sup(s)$ and $sig(e)=\swap$ otherwise;
for any $i\in\{0,\ldots,m-1\}$, from the support of $t_{i,0}$, the signatures of $v_{i_0}$ and $v_{i_1}$ determine the supports of $t_{i,1}$ and $t_{i,2}$ (if the functions of the signatures are defined for these supports);
for any $i\in\{0,\ldots,n-1\}$, if $f_{i,0}\edge{e}f_{i,1}$ in $B_G$, from the support of $f_{i,0}$, the signature of $e$ determines the support of $f_{i,1}$ (if defined);
however, if we also have $f_{i,0}\edge{e'}f_{i,1}$ with $e'\neq e$ in $B_G$, it is necessary that the signature of $e'$ is  "compatible" with the pair $sup(f_{i,0})$ and $sup(f_{i,1})$ (to go from $0$ to $0$, $sig(e')$ may be  or ; to go from $0$ to $1$, $sig(e')$ may be  or ; to go from $1$ to $0$, sig(e') may be  or ; to go from $1$ to $1$, $sig(e')$ may be  or ).

In fact, the same is true if we choose as we want $sup(\iota)$ as well as $sup(s)$ when one chooses as we want some $s$ in each $T_i$ ($i\in\{0,\ldots,m-1\}$) and each $F_j$  ($j\in\{0,\ldots,n-1\}$), and (coherently) signatures $sig(e)$ when $e\in E$.
This is due to the fact that, for each partial function in $\tau$, its inverse is also a partial function (this would not be true if we allowed  or ). Hence we may proceed backward as well as forward in the exploration of $B_G$.

The TS $B_G$ has the $\tau$-SSP.

-Let $sup_0(\iota)=0$, $sup_0(s)=1$ when $s\in S(A_G)\setminus\{\iota\}$, $sig_0(e)=\swap$ for all $e\in Y$ and $sig_0(e)=\nop$ when $e\in E(A_G)\setminus Y$, then $R_0=(sup_0, sig_0)$ is a region that solves $\iota$.

Let $i\in \{0,\dots, m-1\}$ be arbitrary but fixed.

- For all $s\in I$, let $sup_1(s)=1$ if $s=t_{i,0}$, $0$ otherwise, and let $sig_1(e)=\nop$ for all $e\in E$.
This leads to a region $R_1=(sup_1, sig_1)$ that solves $(s,s')$ for all $s\in S(T_i)$, and all $s'\in S(A_G)\setminus S(T_i)$.

-If $sup_2(s)=0$ for all $s\in I$ and $sig_2(e)=\swap$ for all $e\in E$,
then $R_2=(sup_2, sig_2)$ solves $(t_{i,0}, t_{i,1})$ and $(t_{i,1}, t_{i,2})$.

-If $sup_3(s)=0$ for all $s\in I$ and, for all $e\in E$, if $e=v_{i_0}$ then $sig_3(e)=\swap$, $\nop$ otherwise,
then $R_3=(sup_3, sig_3)$ solves $(t_{i,0}, t_{i,2})$.

By the arbitrariness of $i$, this shows, for all $s\in \bigcup_{i=0}^{m-1}S(T_i)$, that $s$ is solvable.

Similarly, one shows the solvability of each $s\in \bigcup_{i=0}^{n-1}S(F_i)$.
The fact follows.

In the following of the subsection, we shall assume that $\omega\subseteq \{\inp,\out, \free,\used\}$ with $\omega\cap\{\inp,\out\}\not=\emptyset$, and $\tau=\{\nop,\swap\}\cup\omega$.

The TS $B_G$ has the $\tau$-ESSP.

We shall assume that $\inp\in\tau$ (the case where $\omega=\{\out\}$ is symmetrical).

-If $sup_0(\iota)=1$, $sig_0(e)=\inp$ for all $e\in Y$ and $sig_0(e)=\nop$ for all $E(A_G)\setminus Y$, then $R_0=(sup_0, sig_0)$ solves $e$ for all $e\in Y$.

We proceed with the $a_j$'s:
Let $j\in \{0,\dots, \kappa\}$ be arbitrary but fixed.

-If $sup_1(\iota)=0$, $sup_1(s)=1$ for all $s\in I$, $sig_1(a_j)=\inp$ and $sig_1(e)=\swap$ if $e\in E(A_G)\setminus\{a_j\}$,
then $R_1=(sup_1,sig_1)$ solves $(a_j,s)$ for all $s\in \bigcup_{i=0}^{n-1}\{f_{i,1}\}\cup \bigcup_{i=0}^{m-1}\{t_{i,1}\}\cup\{\iota\}$.

-If $sup_2(s)=1$ for all $s\in \{f_{0,0},\dots, f_{n-1,0}\}$, $sup_2(s)=0$ for all $s\in \{t_{0,0},\dots, t_{m-1,0}\}$,  $sig_1(a_j)=\inp$ and $sig_1(e)=\swap$ if $e\in E\setminus\{a_j\}$, then $R_2=(sup_2,sig_2)$ solves $(a_j,s)$ for all $s\in \bigcup_{i=0}^{m-1}\{t_{i,0}, t_{i,2}\}$.

Since $j$ was arbitrary, the solvability of the $a_j$'s follows.

We proceed with the $v_i$'s:
Let $i\in \{0,\dots, m-1\}$ be arbitrary but fixed, and let $L$ select the edges (at most three) that contain $v_i$, that is, $v_i\in \mathfrak{e_\ell}$ when $\ell\in L$.

We start with the case where $v_i\in \Ss$, implying that $f_{i,0}\edge{v_i}f_{i,1}\not\in B_G$:

-For all $s\in I$, let $sup_3(s)=1$ if $s\in \bigcup_{\ell\in L}\{t_{\ell,0}\}$ and $0$ otherwise; for all $e\in E$, then $sig_3(e)=\inp$ if $e=v_i$ and $\nop$ otherwise.
Then  $R_3=(sup_3,sig_3)$ solves $(v_i,s)$ for all $s\in S\setminus \bigcup_{\ell\in L}S(T_{\ell})$.

Let $\ell\in L$.
The region $R_3$ also solves $(v_i,t_{\ell,2})$ and, if $t_{\ell,0}\edge{v_i}$, then it solves also $(v_i,t_{\ell,1})$.
With respect to $T_{\ell}$, it remains to address the case $t_{\ell,1}\edge{v_i}$, which requires to solve $(v_i,t_{\ell,0})$.
The following region $R_4=(sup_4, sig_4)$ does it:
For all $s\in I$, if $s\edge{v_i}$ (implying that $v_i$ is the “first” event in the corresponding edge of the graph), then $sup_4(s)=1$, otherwise $sup_4(s)=0$;
for all $e\in E$, if $e=v_i$, then $sig_4(e)=\inp$, otherwise $sig_4(e)=\swap$ (note that, here, it is important that $f_{i,0}\edge{v_i}f_{i,1}\not\in B_G$, otherwise we would lose the coherency in $F_{v_i}$).
Since $i$ and $\ell$ were arbitrary, this shows that solvability of vertex events that do belong to the vertex cover.

It remains to consider the case where $v_i\not\in \Ss$, implying that $f_{i,0}\edge{v_i}f_{i,1}\in B_G$:

-Let $sup_5(s)=1$ when $s\in I$ and, for all $e\in E$, $sig_5(e)=\inp$ when $e\not\in \Ss$,  otherwise.
Then $R_5=(sup_5,sig_5)$ solves $(v_i,s)$ for all $s\in \bigcup_{i=0}^{n-1}\{f_{i,1}\}$.
(Notice that never two events with an -signature occur one after the other, since $\Ss$ is a vertex cover.)

-If $sup_6(s)=1$ for all $s\in \{f_{i,0}\}\cup\bigcup_{i=0}^{m-1}\{t_{i,0}\}$, $sup_6(s)=0$ for all $s\in\bigcup_{j=0}^{n-1}\{f_{j,0}\}\setminus \{f_{i,0}\}$, and, for all $e\in E$, $sig_6(e)=\inp$ if $e=v_i$, $sig_6(e)=\swap$ if $e\in  \{a_0,\dots, a_{\kappa}\}\cup\U\setminus \Ss$, $sig_6(e)=\nop$ otherwise, then $R_6=(sup_6,sig_6)$ solves $(v_i,s)$ for all $s\in \bigcup_{j=0}^{n-1}\{f_{j,0}\}\setminus \{f_{i,0}\}$.

In order to solve $v_i$ within $T_j$ when $j\not\in L$, it suffices to define a region that is complementary to $R_6$ within the $T_j$'s.
The following region $R_7=(sup_7, sig_7)$ accomplishes this:
for all $s\in I$, if $s\in \{ f_{i,0}\}\cup\bigcup_{l\in L}\{t_{l,0}\}$, then $sup_7(s)=1$, otherwise $sup_7(s)=0$;
for all $e\in E$, $sig(e)=\inp$ if $e=v_i$, $sig_7(e)=\swap$ if $e\in \{a_0,\dots, a_{\kappa}\}\cup \U\setminus \Ss$, otherwise $sig_7(e)=\nop$.

It remains to solve $v_i$ within $T_j$ when $j\in L$.
Let $j\in L$ be arbitrary but fixed.
The ESSA $(v_i, t_{j,2})$ is solved by $R_5$, and if $t_{j,0}\edge{v_i}$, then $R_5$ solves $(v_i, t_{j,1})$ as well.
Hence, it remains to consider the case $t_{j,1}\edge{v_i}$, which implies $v_{{j}_0}\in \Ss$, and requires to solve $(v_i, t_{j,0})$.
The following region $R_8=(sup_8, sig_8)$ accomplishes this:
for all $s\in I$, if $s\in \{f_{i,0}\}\cup\bigcup_{l\in L}\{t_{l,0}\}\setminus\{t_{j,0}\}$, then $sup_8(s)=1$, otherwise $sup_8(s)=0$;
for all $e\in E$, $sig_8(e)=\inp$ if $e=v_i$, $sig_8(e)=\swap$ if $e\in\{v_{{j}_0}\}\cup\{a_0,\dots, a_{\kappa}\}\cup\U\setminus \Ss$, $sig_8(e)=\nop$ otherwise.

Since $i$ and $j$ were arbitrary, this completes the solvability of the vertex events.
The fact follows.

Altogether, we get the following lemma:

If there is a vertex cover of size at most $\lambda$ for $G$, then there is an edge removal $B_G$ of $A_G$ that satisfies $\vert \K\vert \leq \kappa$, and has the $\tau$-SSP, and the $\tau$-ESSP.

§.§ The Proof of Theorem <ref>(<ref>) for the Types without $\inp$, and $\out$

In this section, we assume that $\emptyset\neq\omega\subseteq \{\free,\used\}$,
and more exactly $\used\in\omega$ (the case $\omega=\{\free\}$ may be handled symmetrically).

Note that, like in section <ref>, if $A$ is a TS such that $s'\edge{e}s\edge{\neg e}$, then the ESSA $(e,s)$ cannot be solved by a $\tau$-region.
The current reduction then extends the former one by simply adding the missing reverse edges.
More exactly, we first define $\kappa=2\lambda$.
Then, for every $i\in \{0,\dots, m-1\}$, and for every $j\in \{0,\dots, n-1\}$, the new TS $A_G$ has the following gadgets $T_i$, and $F_j$: (where $s\edge{e}s'$ implies $s'\edge{e}s$):

[new set = import nodes]

[nodes=set=import nodes]
(T) at (-0.75,0) $T_i=$;
ıin 0,...,2  (ı) at (ı*2cm, 0) ;
ıin 0,...,2  (ı) at (ı) $t_{i,\i}$;
(import nodes);
0 <->["$v_{i_0}$"]1<->["$v_{i_1}$"]2;

[xshift=7.5cm, nodes=set=import nodes]
(F) at (-0.75, 0) $F_j=$;
(0) at (0,0);
(1) at (3,0);
(0) at (0) $f_{j,0}$;
(1) at (1) $f_{j,1}$;
(dots) at (1.5,0.4) $\vdots$;

(import nodes);

0<->[ swap, bend right=90,  "$v_j$"]1;
0<->[swap, bend right =35, "$a_0$"]1;
0<->[ bend right  =5, swap,"$a_1$"]1;
0<->[swap, bend left =35,swap , "$a_{\lambda-1}$"]1;
0<->[swap, bend left =90, swap, "$a_\lambda$"]1;

Again, the TS $A_G$ has the initial state $\iota$;
for all $i\in \{0,\dots, m-1\}$ and all $j\in \{0,1,2\}$,

it has the edges $\iota\FBedge{y_i^j}t_{i,j}$;
finally, for all $\ell\in \{0,\dots, n-1\}$, it has the edges $\iota\FBedge{z_\ell}f_{\ell,0}$.
The result is a TS $A_G$, where the $y_i^j$-, and $z_\ell$-labelled edges serve to ensure reachability even if we delete some $v_j$'s.
For the sake of simplicity, we summarize these events by $Y=\bigcup_{i=0}^{m-1}\{y_i^0,y_i^1,y_i^2\}\cup\{z_0,\dots, z_{n-1}\}$.

If there is an edge removal $B_G$ of $A_G$ that satisfies $\vert \K\vert \leq \kappa$, and has the $\tau$-ESSP, then there is a vertex cover of size at most $\lambda$ for $G=(\U,M)$.

Let $B_G$ be an edge removal of $A_G$ that satisfies $\vert \K\vert \leq \kappa$, and has the $\tau$-ESSP, and let $\Ss=\{v\in \U\mid s\edge{v}s'\in \K\}$ select the vertex events that label an edge of $A_G$ that is removed in $B_G$.
Note that $s\edge{e}s'\in \K$ implies $s'\edge{e}s\in \K$, since otherwise we would have an unsolvable ESSA $(e,s')$ in $B_G$, which is a contradiction.
This particularly implies $\vert \Ss\vert \leq \frac{\kappa}{2}=\lambda$.

We argue that $\Ss$ defines a vertex cover for $G$:

Let $i\in \{0,\dots, m-1\}$ be arbitrary, but fixed.
Similarly to the proof of Lemma <ref> one argues that $\Ss\cap\{v_{i_0}, v_{i_1}\}=\emptyset$ implies a contradiction to the solvability of $(v_{i_0}, t_{i,2})$.
Hence, by the arbitrariness of $i$, we have $\Ss\cap \mathfrak{e}_i\not=\emptyset$ for all $i\in \{0,\dots, m-1\}$.
This proves the claim.

If there a vertex cover of size at most $\lambda$ for $G$, then there is an edge removal $B_G$ of $A_G$ that satisfies $\vert \K\vert \leq \kappa$ and has both the $\tau$-SSP and the $\tau$-ESSP.

Let $\Ss=\{v_{\ell_0},\dots, v_{\ell_{\lambda-1}}\}$ be a suitable vertex cover, and let $B_G$ be the TS that originates from (the new) $A_G$ by the removal of the edges $f_{\ell_j,0}\edge{v_{\ell_j}}f_{\ell_j,1}$ and $f_{\ell_j,1}\edge{v_{\ell_j}}f_{\ell_j,0}$ for all $j\in \{0,\dots, \lambda-1\}$, and nothing else.
Clearly, $B_G$ is an edge removal of $A_G$ that satisfies $\vert \K\vert =\kappa=2\lambda$.

Note that every region presented for the proof of Lemma <ref> can be directly transferred to the current edge removal $B_G$, since their signatures get along with $\nop$, and $\swap$.
Hence, $B_G$ has the $\tau$-SSP.

We argue for the $\tau$-ESSP:

We start with the $y_i^j$: Let $i\in \{0,\dots, m-1\}$, and $j\in \{0,1,2\}$.

-If $sup_0(\iota)=1$, and
for all $e\in E(B_G)$,
if $e=y_i^j$ then $sig_0(e)=\used$, if  $e\in \{v_{i_0}, v_{i_1}\}$ such that $t_{i,j}\edge{e}$ then $sig_0(e)=\swap$,
otherwise $sig(e)=\nop$,
this leads to a region $R_0=(sup_0, sig_0)$ that solves $(y_i^j, s)$ for all $s\in S(T_i)\setminus \{t_{i,j}\}$.

Let $I=\{t_{0,0}, t_{1,0},\dots, t_{m-1,0}, f_{0,0}, f_{1,0}, f_{n-1,0}\}$ be the set of the initial states of the gadgets of $A_G$ (when considered as TS).

Let $i\in \{0,\dots, m-1\}$ be arbitrary but fixed.
In the following, we argue hat $y_i^0$, and $y_i^1$, and $y_i^2$ are solvable at the necessary states of $T_i$.
We start with $y_i^0$, and have to distinguish the case where $v_{i_0}$ belongs to the vertex cover, and the case where it does not belong to the vertex cover, which implies that $F_{i_0}$ is completely present in $B_G$.

The following region $R_0=(sup_0, sig_0)$ solves $(y_i^0,t_{i,1})$, and $(y_i^0,t_{i,2})$:

The case $v_{i_0}\in \Ss$ (implying that $f_{i_0,0}\fbedge{v_{i_0}}f_{i_0,1}\not\in B_G$):

We let $sup(\iota)=sup(s)=1$ for all $s\in I$, and, for all $e\in E(B_G)\setminus (\bigcup_{i=0}^{m-1}\{y_i^1,y_i^2\})$,
if $e=y_i^0$, then $sig(e)=\used$,
if $e=v_{i_0}$, then $sig(e)=\swap$, and $sig(e)=\nop$ otherwise.

After that we compute the support completely:
for every $j\in \{0,\dots, m-1\}$, and every $\ell\in \{0,1\}$, we let $sup(t_{j,\ell+1})=1-sup(t_{j\ell})$ if $v_{j_\ell}=v_{i_0}$ (implying $sig(v_{j_\ell})=\swap$), and otherwise $sup(t_{j,\ell+1})=sup(t_{j\ell})$;

for every $j\in \{0,\dots, n-1\}$, we let $sup(f_{j,1})=1$ (which is consistent, since $v_{i_0}\in \Ss$).
Finally, we complete the signature: for all $e\in \bigcup_{i=0}^{m-1}\{y_i^1,y_i^2\}$, if $\edge{e}s\in B_G$, and $sup(s)=0$, then $sig(e)=\swap$, and $sig(e)=\nop$ otherwise.

The case $v_{i_0}\not\in \Ss$ (implying that $f_{i_0,0}\fbedge{v_{i_0}}f_{i_0,1}\in B_G$, and $v_{i_1}\in \Ss$, which implies $f_{i_1,0}\fbedge{v_{i_1}}f_{i_1,1}\not\in B_G$):

We let $sup(\iota)=sup(s)=1$ for all $s\in I$, and, for all $e\in E(B_G)\setminus (\bigcup_{i=0}^{m-1}\{y_i^1,y_i^2\})$,
if $e\in \{y_0^0, y_1^0,\dots, y_{m-1}^0\}\cup\{z_0,\dots, z_{n-1}\}$, then $sig(e)=\used$,
if $e=v_{i_1}$, then $sig(e)=\nop$, and
$sig(e)=\swap$ otherwise.

After that we compute the support completely:
for every $j\in \{0,\dots, m-1\}$, and every $\ell\in \{0,1\}$, we let $sup(t_{j,\ell+1})=1-sup(t_{j\ell})$ if $v_{j_\ell}=v_{i_0}$ (implying $sig(v_{j_\ell})=\swap$), and otherwise $sup(t_{j,\ell+1})=sup(t_{j,\ell})$;

for every $j\in \{0,\dots, n-1\}$, we let $sup(f_{j,1})=0$.
Finally, for all $e\in \bigcup_{i=0}^{m-1}\{y_i^1,y_i^2\}$, if $\edge{e}s\in B_G$, and $sup(s)=0$, then $sig(e)=\swap$, and $sig(e)=\nop$ otherwise.

It is easy to see, that we can define a region $R$ that solves $(y_i^1,t_{i,0})$, and $(y_i^1,t_{i,2})$, respectively $(y_i^2,t_{i,0})$, and $(y_i^2,t_{i,1})$, in a similar way.
We thus refrain from representing the tedious details, and consider $y_i^0, y_i^1, y_i^2$ solved with respect to the necessary states of $T_i$.

-If $sup_1(\iota)=1$, and,
for all $e\in E(B_G)$,
if $e\in \{y_i^0,y_i^1,y_i^2\}$, then $sig_0(e)=\used$,
if $e\in Y\setminus \{y_i^0,y_i^1,y_i^2\}$ then $sig_1(e)=\swap$, and
$sig_1(e)=\nop$ otherwise,
then the resulting region $R_1=(sup_1, sig_1)$ solves $(y_i^j, s)$ for all $s\in S(B_G) \setminus (\{\iota\}\cup S(T_i))$, and all $j\in \{0,1,2\}$.

By the arbitrariness of $i$, this proves the solvability of $y$ for all $y\in \bigcup_{i=0}^{m-1}\{y_i^0,y_i^1,y_i^2\}$.
Similarly, one argues that $z$ is solvable for all $z\in \bigcup_{i=0}^{n-1}\{z_i\}$.

If $e\in \{a_0,\dots, a_\kappa\}\cup\U$ and $s\in S(B_G)$ belongs to a gadget that does not contain $e$, then it is easy to see that $(e, s)$ is $\tau$-solvable:
One simply defines a region that maps exactly to $1$ the states that belong to gadgets of $B_G$ that contain $e$ (and $0$ to the others),
maps $e$ to $\used$, choses a suitable signature of the reachability events from $Y$ (either $\nop$ or $\swap$), and maps all the other events $e'$ with $e'\in E(B_G)\setminus (\{e\}\cup Y)$ to $\nop$.
This particularly implies the solvability of $a$ for all $a\in \{a_0,\dots, a_\lambda\}$.
Hence, it remains to address the vertex events.

Let $i\in \{0,\dots, m-1\}$ be arbitrary but fixed.
By the former discussion, if $f_{i_0,0}\fbedge{v_{i_0}}f_{i_0,1}\in \K$ then $v_{i_0}$ is solvable in $F_{i_0}$, otherwise there is no need to solve it in $F_{i_0}$.
Similarly, the solvability of $v_{i_1}$ in $F_{i_1}$ needs no further discussion.
Hence, it remains to argue for the solvability of $v_{i_0}$ in  $T_i$ (the case of $v_{i_1}$ will be similar).

Let us first assume that $v_{i_0}\in\mS$ (so that it does not occur in $F_{i_0}$):
for all $e\in E(B_G)\setminus Y$, if $e=v_{i_0}$ then $sig_2(e)=\used$, otherwise $sig_2(e)=\swap$; and
$sup(\iota)=0$; and
for any $j\in\{0,\ldots,n-1\}$, $sup_2(f_{j,0})=0$; and

for any $j\in\{0,\ldots,m-1\}$, if $v_{j_0}\not=v_{i_0}$, then $sup_2(t_{j,0})=0$,
otherwise $sup(t_{j,0})=1$;

the other supports and signatures may then be derived coherently, delivering a region  $R_2=(sup_2, sig_2)$ which, as expected, solves $(v_{i_0}, t_{i,2})$.

Let us now assume that  $v_{i_0}\not\in\mS$, so that $v_{i_1}\in\mS$ , since we have a vertex covering (then $v_{i_0}$ occurs in $F_{i_0}$, but the vertex cover events do not occur in the F-gadgets).
For all $e\in E(B_G)\setminus Y$, if $e=v_{i_0}$ then $sig_3(e)=\used$, if $e\in \Ss$, then $sig_3(e)=\swap$, otherwise $sig_3(e)=\nop$;
for any $j\in\{0,\ldots,n-1\}$, $sup_3(f_{j,0})=1$;
for any $j\in\{0,\ldots,m-1\}$, if $v_{j_0}=v_{i_0}$, then $sup_3(t_{j,0})=1$, otherwise $sup_3(t_{j,0})=0$;

the other supports and signatures may then be derived coherently, delivering a region  $R_3=(sup_3, sig_3)$ which, as expected, solves $(v_{i_0}, t_{i,2})$.

Since $i$ was arbitrary, this completes the proof.

§ THE COMPLEXITY OF EVENT REMOVAL

In this section, we deal with the following modification:

Let $A=(S,E,\delta,\iota)$ be a TS.
A TS  $B=(S,E',\delta',\iota)$ with

$E'\subseteq E$ is an event-removal of $A$ if for all $e\in E'$ the following is true:
$s\edge{e}s'\in B$ if and only if $s\edge{e}s'\in A$ for all $s,s'\in S$.
By $\E=E\setminus E'$ we refer to the (set of) removed events.

In the following, we shall assume that $B$ is a valid system, i.e., each state remains reachable from the initial one (note that each remaining event occurs at least once in $\delta'$ since this was already the case in $A$).

$\tau$-Event-Removal for Embedding
A TS  $A=(S,E,\delta,\iota)$, a natural number $\kappa$.
Does there exist an event-removal $B$ for $A$ by ${\E}$ that has the $\tau$-SSP and satisfies $\vert{\E}\vert\leq \kappa$?

$\tau$-Event-Removal for Language-Simulation
A TS  $A=(S,E,\delta,\iota)$, a natural number $\kappa$.
Does there exist an event-removal $B$ for $A$ by ${\E}$ that has the $\tau$-ESSP and satisfies $\vert{\E}\vert\leq \kappa$?

$\tau$-Event-Removal for Realization
A TS  $A=(S,E,\delta,\iota)$, a natural number $\kappa$.
Does there exist an event-removal $B$ for $A$ by ${\E}$ that has the $\tau$-ESSP and the $\tau$-SSP and satisfies $\vert{\E}\vert\leq \kappa$?

The following theorem is the main result of this section:

If $\omega\subseteq\{\inp,\out, \free,\used\}$, and $\tau=\{\nop,\swap\}\cup\omega$, then

$\tau$-Event Removal for Embedding is NP-complete.

$\tau$-Event Removal for Language Simulation, and

$\tau$-Event Removal for Realization are NP-complete if $\omega\not=\emptyset$.

First of all, we argue for the polynomial part:
If $\tau=\{\nop,\swap\}$, then a TS $A=(S,E,\delta,\iota)$ has the $\tau$-ESSP if and only if every event occurs at every state,
since the functions , are defined on both $0$ and $1$. Thus, any ESSP atom $(e,s)$ of $A$ would be unsolvable.
This does not imply that an event-removal may neither render nor keep the $\tau$-ESSP valid, since the event removal usually reduces the set $E$, however we may easily determine which events should be removed.
First, we may determine the events $e\in E$ such that, for some state $s$, we have $\neg s\edge{e}$: they must be removed.
For the language simulation problem, this is enough and we simply have to check if the resulting system is valid and if the number $k$ of removed events does not exceed $\kappa$.
For the realization problem we still have to consider the $\tau$-SSP problem.

Let $\tau=\{\nop,\swap\}$, and $A=(S,E,\delta,\iota)$ be a TS that has the $\tau$-ESSP.
If $A$ has the $\tau$-SSP, then

* if $s\edge{e}s'\in A$ such that $s\not=s'$, then $q\edge{e}q\not\in A$ for all $q\in S$;

* if $s\edge{e}s'\in A$ such that $s\not=s'$, then $s'\edge{e}s\in A$;

* if $e\not=e'\in E$, and $s,s'\in S$ such that $s\edge{e}s'\in A$, and $s\edge{e'}s'\in A$, then $sig(e)=sig(e')$ for every $\tau$-region $R=(sup, sig)$ of $A$;

* if $e\not=e'\in E$, and $s\not=s'\in S$ such that $s\edge{e}s'\in A$, and $s\edge{e'}s'\in A$, then $q\edge{e}q'\in A$ if and only if $q\edge{e'}q'\in A$ for all $q,q'\in S$;

* if $e\not=e'\in E$, and $s\not=s'\in S$ such that $s\edge{e}s'\in A$, and $s\edge{e'}s'\in A$, and $(q,q')$ then the following condition is true:
if $B=(S,E\setminus \{e'\}, \delta',\iota)$ is the event-removal of $A$ that removes $e'$ (and the $e'$-labeled edges), and nothing else, then, for any SSA $\alpha (s,s')$ of $A$, there is a $\tau$-region $R$ of $A$ that solves $\alpha$ if and only if there is a $\tau$-region $R'$ of $B$ that solves $\alpha$.

(1): If $q\edge{e}q\in A$ for some state $q\in S$, then $sig(e)=\nop$, and thus $sup(s)=sup(s')$ for every region of $A$, which contradicts the $\tau$-SSP of $A$.

(2): Assume that $s\edge{e}s'\in A$, but $s'\edge{e}s\not\in A$.
Since $A$ has the $\tau$-ESSP, there is a state $q$ such that $s'\edge{e}q\in A$.
If $s'=q$, then the SSA $(s,s')$ is not $\tau$-solvable, since $sup(s)\not=sup(s')$ implies $sig(e)=\swap$ for every $\tau$-region $R=(sup, sig)$, and thus $sup(s')\not=sup(s')$ by $s'\edge{e}s'$, which is a contradiction.
If $q\not\in\{s,s'\}$, then the SSA $(s,q)$ is not solvable, since $sig(e)\in \{\nop,\swap\}$ then implies $sup(s)=sup(q)$ for every region $R=(sup, sig)$.
Hence $q=s$, which proves the claim.

(3): Assume that $R=(sup, sig)$ is a $\tau$-region of $A$ such that, without loss of generality, $sig(e)=\nop$, and $sig(e')=\swap$.
Then $sup(s)=sup(s')$ by $sig(e)$, and $sup(s)\not=sup(s')$ by $sig(e')$, which is a contradiction.
The claim follows.

(4): $\Rightarrow$:

Notice that $s\not=s'$, and $s\edge{e}s'\in A$, and  $s\edge{e'}s'\in A$ implies $q\not=q'$ by Item (1), and $sig(e)=sig(e')$ for every $\tau$-region of $A$ by Item (3).
Assume that there is $q\edge{e}q'\in A$, but $q\edge{e'}q'\not\in A$.
Since $A$ has the $\tau$-ESSP, there is a state $t\in S$ such that $q'\edge{e'}t\in A$.
By $s\not=s'$, and $s\edge{e'}s'$, and Item (1), we get $t\not=q'$.
By Item (2), we get $t\not=q$, since $q'\edge{e'}q\in A$, implies $q\edge{e'}q'\in A$, which is a contradiction.
Hence, $A$ contains a path $q\edge{e}q'\edge{e'}t$ with pairwise distinct events $q,q',t$.
Since $A$ has the $\tau$-SSP, there is a $\tau$-region $R=(sup, sig)$, that solves $(q,t)$, implying $sup(t)=1-sup(q)$.
However, if $sig(e)=sig(e')\in \{\nop,\swap\}$, then $sup(q)=sup(t)$.
This implies $sig(e)\not=sig(e')$, which is a contradiction.

Similarly, one argues for the other direction, and the claim follows.

(5): $\Rightarrow$:
If $R=(sup, sig)$ is a $\tau$-region of $A$, that solves $\alpha$, then the restriction $R'=(sup, sig')$ of $R$ to $B$ such that $sig'(e)=sig(e)$ for all $e\in E\setminus \{e'\}$ is a $\tau$-region of $B$ that also solves $\alpha$.

If $R=(sup, sig)$ is a $\tau$-region of $B$, that solves $\alpha$, then the extension of $R'=(sup, sig')$ of $R$ to $A$ such that $sig'(e)=sig(e)$ for all $e\in E\setminus \{e'\}$, and $sig'(e')=sig(e)$ is a $\tau$-region of $A$ that also solves $\alpha$.
Indeed, by Item (4), we have that $q\edge{e}q'\in A$ if and only if $q\edge{e'}q'\in A$.
Since $q\edge{e'}q'\in B$ implies $sup(q)\ledge{sig(e')}sup(q')\in \tau$, and thus $sup(q)\ledge{sig'(e')}sup(q')\in\tau$, the region $R'$ is valid for $A$.

This completes the proof.

If $\tau=\{\nop,\swap\}$, and $A=(S,E,\delta, \iota)$ is a TS that has the $\tau$-ESSP, and $\kappa\in \mathbb{N}$, then one can decide in polynomial time whether there is an event-removal $B=(S,E',\delta',\iota)$ of $A$ by $\E$ that has the $\tau$-SSP, and satisfies $\vert \E\vert \leq \kappa$.

First of all, by Lemma <ref>(1), we have to remove all events $e$ such that $s\edge{e}s'\in A$, and $q\edge{e}q\in A$ for some $s\not=s'\in S$.

If, for some $s\in S$ and $e\in E'$, we have $s\edge{e}s$, then we must choose $sig(e)=\nop$;
but if, for some $s',s''\in S$, we also  have $s'\neq s''$ and $s'\edge{e}s''$, that means that $e$ must be removed.
Again, at the end, we simply have to check if  the resulting system is valid and if the number $k$ of removed events does not exceed $\kappa$.
In either case, the problem is polynomial.
Thus, for the proof of Theorem <ref>, it remains to consider the NP-completeness results.

§.§ The Proof of Theorem <ref>(<ref>), and the Proof of Theorem <ref>(<ref>) for the Types with $\inp$ or $\out$

In the following, as long as not stated explicitly otherwise, let $\tau=\{\nop,\swap\}\cup\omega$ with $\omega\subseteq \{\inp,\out, \free,\used\}$, and for the input $(G,\lambda)$ of 3BVC, where $G=(\U,M)$, let $(A_G,\kappa)$ be defined as in Section <ref>.
In this section, we show that $G$ has a $\lambda$-vertex cover if and only if $A_G$ allows an event-removal $B_G$ that respects $\kappa$, and has the $\tau$-SSP;
moreover, we also show that if $\tau\cap\{\inp,\out\}\not=\emptyset$, then $G$ has a $\lambda$-vertex cover if and only if $A_G$ allows an event-removal $B_G$ that respects $\kappa$, and has the $\tau$-ESSP.
Altogether, this proves Theorem <ref>(<ref>), and the statements of Theorem <ref>(<ref>) for the types $\tau\cap\{\inp,\out\}\not=\emptyset$.

For the sake of simplicity, in the remainder of this section, if we discuss aspects of the $\tau$-ESSP (where the addressed TS is clear from the context), we always assume that $\tau\cap\{\inp,\out\}\not=\emptyset$.

If there is an event removal $B_G$ of $A_G$ that satisfies $\vert \E\vert \leq \kappa$, and has the $\tau$-SSP, respectively the $\tau$-ESSP, then there is a vertex cover of size at most $\lambda=\kappa$ for $G=(\U,M)$.

Let $B_G$ be an event removal of $A_G$ that satisfies $\vert \E\vert \leq \kappa$, and has the $\tau$-SSP, respectively the $\tau$-ESSP, and let $\Ss=\E \cap\U$ be the set vertex-events that are removed from $A_G$.

Let $i\in \{0,\dots, m-1\}$ be arbitrary but fixed.

Since $\vert \E\vert \leq \kappa$, there is a $j\in \{0,\dots, \kappa\}$ such that the event $a_j$, and thus all $a_j$-labeled edges are present in $B_G$.
Hence, similar to the arguments for the proof of Lemma <ref>, one argues that if $\{v_{i_0}, v_{i_1}\}\cap \E=\emptyset$, implying that all $v_{i_0}$-labeled, and $v_{i_1}$-labeled edges are present in $B$, then $(t_{i,0}, t_{i,2})$ is an unsolvable SSA of $B$, respectively $(v_{i_0}, t_{i,2})$ is an unsolvable ESSA of $B$, which is a contradiction.
By the arbitrariness of $i$, and since $\vert \Ss\vert \leq \vert\E\vert\leq \kappa=\lambda$, the claim follows.

Reversely, if $G$ has a $\lambda$-vertex cover, then $A_G$ allows a suitable event-removal $B_G$ that has the $\tau$-SSP, respectively the $\tau$-ESSP:

If there is a vertex cover of size at most $\lambda$ for $G=(\U,M)$, then there is an event removal $B_G$ of $A_G$ that satisfies $\vert \E\vert \leq \kappa$, and has the $\tau$-SSP, and that has $\tau$-ESSP if $\tau\cap\{\inp,\out\}\not=\emptyset$.

Let $\Ss=\{v_{\ell_0},\dots, v_{\ell_{\lambda-1}}\}$ be a vertex cover for $G$, and let $B_G$ be the TS that originates from $A_G$ by the removal the events of $\Ss$ (and thus the edges labeled by these events), and nothing else.
By the events of $Y$, $B_G$ is a reachable TS, which has the same states as $A_G$, and obviously satisfies $\vert \E\vert\leq \kappa=\lambda$.

In the following, we argue that the solvability of $B_G$ follows from the regions presented for the proofs of Fact <ref>, and Fact <ref> of  Section <ref>:

Let $B_G'$ be the TS that originates from $A_G$ by removing, for all $i\in \{0,\dots, \lambda-1\}$, the edge $f_{\ell_i,0}\edge{v_{\ell_i}}f_{\ell_i,1}$, and nothing else (that is, $B_G'$ corresponds to the edge-removal defined in Section <ref>).
By definition, both $B_G$, and $B_G'$ have the same states as $A_G$, and thus have the same SSA to solve.
Moreover, if $s\edge{e}s'$ is an edge of $B_G$, then it is an edge of $B_G'$, since, for all $i\in \{0,\dots, \lambda-1\}$, $B_G$ does not only miss the edge $f_{\ell_i,0}\edge{v_{\ell_i}}f_{\ell_i,1}$, but all $v_{\ell_i}$-labeled edges (and nothing else).
In particular, for every event $e\in E(B_G)$, which implies $e\not\in \Ss$, all the (original) $e$-labeled edges (of $A_G$) are present in both $B_G$, and $B_G'$.
Hence, if $(e,s)$ is an ESSA of $B_G$, then it is an ESSA of $B_G'$.
Finally, if $R=(sup, sig)$ is a region of $B_G'$, then its restriction to (the events of) $B_G$ is also a region of $B_G$, since $sup(s)\ledge{sig(e)}sup(s')\in \tau$ is implied for all $s\edge{e}s'\in B_G$, by $s\edge{e}s'\in B_G'$.
Moreover, if $R$ solves a (state or event) separation atom $\alpha$ of $B_G'$ that is also present in $B_G$, then it also solves this atom in $B_G$.
Consequently, since $B_G'$ has the $\tau$-SSP, and the $\tau$-ESSP by the arguments of Fact <ref>, and Fact <ref>, respectively, we conclude that $B_G$ has also these properties.

First of all, we observe that every edge (and thus every state) of the current event removal is also present in the edge removal defined in Section <ref>.
Moreover, if $\alpha$ is an SSA, respectively an ESSA, of the current event removal, then it is also a separation atom of the corresponding edge removal.
Furthermore, if $R=(sup, sig)$ is a region defined for the proofs of Fact <ref>, and Fact <ref>, then the restriction of $R$ to the events of the current event removal defines a region of it.
Hence, the region of Fact <ref> or Fact <ref>, that solves $\alpha$ (respectively) in the edge removal of Section <ref>, also solves $\alpha$ in the current event removal $B$.
Since the regions Fact <ref>, and Fact <ref> cumulate to a suitable admissible set $\mathcal{R}$, the proof of the current lemma follows by $\mathcal{R}$.

§.§ The Proof of Theorem <ref>(<ref>) for the Types Without $\inp$ and $\out$

In this section, as long as not explicitly stated otherwise, let $\emptyset\neq\omega\subseteq \{\free,\used\}$, and $\tau=\{\nop,\swap\}\cup\omega$.
In order to complete the proof of Theorem <ref>(<ref>) (for $\tau$), we reduce the input $G=(\U,M)$ to the instance $(A_G,\kappa)$, where $A_G$ is the TS (with bi-directional edges) as defined in Section <ref>, and $\kappa=\lambda$, and show that $G$ has a $\lambda$-vertex cover if and only if $A_G$ allows an event-removal $B_G$ that respects $\kappa$, and has the $\tau$-ESSP, respectively the $\tau$-ESSP, and the $\tau$-SSP.
We would like to emphasize that we define $\kappa=\lambda$ here, in contrast to the definition of $\kappa=2\lambda$ in section <ref>.
This (current) definition is justified by the fact that the removal of an event already implies the removal of all its edges.
For details see the following arguments.

The following reduction that transforms an input $(\U,M,\lambda)$ to an instance $(A,\kappa)$:
$\kappa=\lambda$, and $A$ is the TS that is defined just like the one in Section <ref>.

If there is an event-removal $B_G$ of $A_G$ that satisfies $\vert \E\vert \leq \kappa$, and has the $\tau$-ESSP, then there is a vertex cover of size at most $\lambda$ for $G=(\U,M)$.

Let $B_G$ be an event-removal $B_G$ of $A_G$ that satisfies $\vert \E\vert \leq \kappa$, and has the $\tau$-ESSP;
let $\Ss=\U\cap\E$.
Note that  $\vert \Ss\vert \leq \vert \E\vert \leq\kappa=\lambda$.

We argue that $\Ss$ is a vertex cover:

Let $i\in \{0,\dots, m-1\}$ be arbitrary but fixed.
If $\{v_{i_0},v_{i_1}\}\cap\Ss=\emptyset$, then $T_i$, $F_{i_0}$ and $F_{i_1}$ are completely present in $B$.
Similar to the proof of Lemma <ref> one argues that this contradicts the $\tau$-ESSP of $B$.
Hence $\{v_{i_0},v_{i_1}\}\cap\Ss\not=\emptyset$, and the arbitrariness of $i$ implies the claim.

If there is a vertex cover of size at most $\lambda$ for $G=(\U,M)$, then there is an event-removal $B_G$ of $A_G$ that satisfies $\vert \E\vert \leq \kappa$, and has the $\tau$-ESSP, and the $\tau$-SSP.

Let $\Ss=\{v_{\ell_0},\dots, v_{\ell_{\lambda-1}}\}$ be a suitable vertex cover of $G$, and let $B_G$ be the event-removal that originates from $A_G$ by removing the events of $\Ss$ (and the corresponding edges), and nothing else.
One easily checks that $B_G$ is a (well-defined) reachable TS, and satisfies $\vert \E\vert\leq \vert \Ss\vert$.

In the following, we argue that the $\tau$-SSP, and the $\tau$-ESSP of $B_G$ is implied by the regions presented for the proof of Lemma <ref>:
Let $B_G'$ be the TS that originates from $A_G$ by the removal of the edges $f_{\ell_j,0}\edge{v_{\ell_j}}f_{\ell_j,1}$, and $f_{\ell_j,1}\edge{v_{\ell_j}}f_{\ell_j,0}$, and nothing else (that is, $B_G'$ corresponds to the edge-removal of Section <ref>).
One verifies that $B_G$, and $B_G'$ have the same states, and thus the same SSAs to solve.
Moreover, if $s\edge{e}s'$ is an edge of $B_G$, implying that $e\not\in \Ss$, then $s\edge{e}s'\in B_G'$.
Hence, every ESSA of $B_G$ is an ESSA of $B_G'$.
Moreover, for every region $R=(sup, sig)$ of $B_G'$, the restriction of $R$ to (the events of) $B_G$ is a region of $B_G$, since $sup(s)\edge{e}sup(s')$ is implied for every $s\edge{e}s'$ of $B_G$ (by $s\edge{e}s'\in B_G'$, and the region property of $R$).
Hence, since the regions of Lemma <ref> justify the $\tau$-SSP, and the $\tau$-ESSP, they particularly justify these properties for $B_G$.

§ THE COMPLEXITY OF STATE REMOVAL

In this section, we address the following modification:

Let $A=(S,E,\delta,\iota)$ be a TS.
A TS $B=(S',E,\delta',\iota)$ with states $S'\subseteq S$ is a state-removal of $A$ if the following two conditions are satisfied:

(1) for all $e\in E$
and all $s,s'\in S'$, $s\edge{e}s'\in B$ if and only if $s\edge{e}s'\in A$;

(2) if $s\edge{e}s'\in A$ and $s\edge{e}s'\not\in B$, then $s\not\in S'$ or $s'\not\in S'$ (or both).

By ${\mS}=S\setminus S'$ we refer to the (set of) removed states.

In the following, we shall assume that $B$ is a valid system, i.e., each state remains reachable from the initial one and each event occurs at least once in $\delta'$.

In particular, we investigate the complexity of the following three decision problems:

$\tau$-State-Removal for Embedding
A TS  $A=(S,E,\delta,\iota)$, a natural number $\kappa$.
Does there exist a state-removal $B$ for $A$ by ${\mS}$ that has the $\tau$-SSP and satisfies $\vert{\mS}\vert\leq \kappa$?

$\tau$-State-Removal for Language-Simulation
A TS  $A=(S,E,\delta,\iota)$, a natural number $\kappa$.
Does there exist a state-removal $B$ for $A$ by ${\mS}$ that has the $\tau$-ESSP and satisfies $\vert{\mS}\vert\leq \kappa$?

$\tau$-State-Removal for Realization
A TS  $A=(S,E,\delta,\iota)$, a natural number $\kappa$.
Does there exist a state-removal $B$ for $A$ by ${\mS}$ that has the $\tau$-ESSP and the $\tau$-SSP and satisfies $\vert{\mS}\vert\leq \kappa$?

The following theorem is the main result of this section:

If $\omega\subseteq\{\inp,\out, \free,\used\}$, and $\tau=\{\nop,\swap\}\cup\omega$, then

$\tau$-State Removal for Embedding is NP-complete.

$\tau$-State Removal for Language Simulation, and

$\tau$-State Removal for Realization are NP-complete if $\omega\not=\emptyset$, otherwise they are solvable in polynomial time.

First of all, we argue for the polynomial part:
If $\tau=\{\nop,\swap\}$, then a TS $A=(S,E,\delta,\iota)$ has the $\tau$-ESSP if and only if every event occurs at every state,
since the functions  , are defined on both $0$ and $1$.
Thus, any ESSP atom $(e,s)$ of $A$ would be unsolvable.
Again, we may determine the states $s\in S$ such that, for some event $e$, we have $\neg s\edge{e}$: they must be removed.
Let $B=(S',E,\delta, \iota)$ be the (unique) result of this phase.
For the language simulation problem, this is enough and we simply have to check if $B$ is valid and if the number $k$ of removed states does not exceed $\kappa$.
Let $(s,s')$ be an unsolvable SSA of $B$.
Since $B$ is an initialized TS, there is a path $\iota\edge{e_1}s_1\dots s_{n-1}\edge{e_n}s_n$ such that $s_n=s$ in $B$.
If we remove $s_n$ (and get, say, $B'$), then $\neg s_{n-1}\edge{e_n}$, since $B$ is deterministic, and thus we have an unsolvable ESSA $(s_{n_1}, e_n)$.
Consequently, we have also to remove $s_{n-1}$, and get, say, $B''$.
By the same arguments, we inductively obtain that $s_{n-1},\dots,s_1$, and finally $\iota$, have to be removed, which is a contradiction, since every state-removal of $A$ has the initial state $\iota$ by Definition <ref>.
Similarly, the removal of $s'$ yields also a contradiction.

If, for some $s\in S'$ and $e\in E$, we have $s\edge{e}s$, then we must choose $sig(e)=\nop$;
but if, for some $s',s''\in S'$, we also  have $s'\neq s''$ and $s'\edge{e}s''$, that means that $s$ or $s'$ must be removed.

Again, at the end, we simply have to check if  the resulting system is valid and if the number $k$ of removed events does not exceed $\kappa$.
In either case, the problem is polynomial.

Thus, for the proof of Theorem <ref>, it remains to consider the NP-completeness results.

§.§ The Proof of Theorem <ref>(<ref>), and the Proof of Theorem <ref>(<ref>) for the Types with $\inp$ or $\out$

In the following, as long as not explicitly stated otherwise, let $\omega\subseteq \{\inp,\out, \free,\used\}$ and $\tau=\{\nop,\swap\}\cup\omega$ such that $\tau\cap\{\inp,\out\}\not=\emptyset$.

In order to prove Theorem <ref>(<ref>), and the statement of Theorem <ref>(<ref>) for $\tau\cap\{\inp,\out\}\not=\emptyset$, we use the following reduction that transforms an input $(G,\lambda)$, where $G=(\U,M)$, to an instance $(A_G,\kappa)$:
$\kappa=\lambda$, and $A_G$ is the TS that is defined just like the one in Section <ref>, but, for all $i\in \{0,\dots, m-1\}$, and for all $j\in \{1,2\}$, it does not implement the edges $\iota\edge{y_i^j}t_{i,j}$.
(The edge $\iota\edge{y_i^0}t_{i,0}$ is still present to ensure reachability.)
By doing so, we ensure that if $B_G$ is well-defined state removal of $A_G$, then, for all $i\in \{0,\dots, m-1\}$, if $t_{i,1}$ is removed, then $t_{i,2}$ is also removed, and, moreover, if $t_{i,0}$ is removed, then also both $t_{i,1}$ and $t_{i,2}$ are removed.
This can be seen as follows:
By Definition <ref>, $B_G$ is a TS, and by Remark <ref>, every TS is initialized, and thus, that is, the initial state $\iota$ is present, and its states are reachable from $\iota$ by a directed path.
Hence, if, for example, the state $t_{0,1}$ is missing in $B_G$ (compared with $A_G$), implying that the (only) edge $t_{0,1}\edge{v_{0_1}}t_{0,2}$ is removed to, then the state $t_{0,2}$ is also not present in $B_G$, since it would not be reachable by a directed path from $\iota$ otherwise, which is a contradiction.

If there is a state removal $B_G$ of $A_G$ that satisfies $\vert \mS\vert \leq \kappa$, and has the $\tau$-SSP, respectively, given $\tau\cap\{\inp,\out\}\not=\emptyset$, has the $\tau$-ESSP, then there is a vertex cover of size at most $\lambda$ for $G=(\U,M)$.

Let $B_G$ be a state removal of $A_G$ that satisfies $\vert \mS\vert \leq \kappa$, and has the $\tau$-SSP, respectively the $\tau$-ESSP.
Let $\Ss=\{v\in \U\mid \exists s\in \mS : \edge{v}s\}$.
Note that $\vert \Ss\vert \leq \vert \mS\vert$, since every state of $A$ is the target of at most one vertex event.
We show that $\Ss$ defines a vertex cover:
Let $i\in \{0,\dots, m-1\}$ be arbitrary but fixed.
Recall that, as argued above, $\iota$ is present in $B_G$, and, for every path $s_0\edge{e_1}s_1\dots\edge{e_n}s_n$ of $A_G$, if $s_i$ is missing in $B_G$, then $s_j$ is also missing for all $i < j\in \{0,\dots, n\}$, since $B_G$ would have unreachable states otherwise.
Hence, if $\Ss\cap\{v_{i_0}, v_{i_1}\}=\emptyset$, implying $\{t_{i,1}, t_{i,2}, f_{i_0,1}, f_{i_1,1}\}\subseteq S(B_G)$, then $T_i$, and $F_{i_0}$, and $F_{i_1}$ are completely present in $B_G$.

Consequently, similar to the proof of Lemma <ref>, one argues that this implies that $B_G$ has the unsolvable SSA $(t_{i,0}, t_{i,2})$, respectively the unsolvable ESSA $(v_{i_0}, t_{i,2})$, which is a contradiction.
By the arbitrariness of $i$, $\Ss$ is a suitable vertex cover, which proves the lemma.

For the converse direction, we state the following lemma:

If there is a vertex cover of size at most $\lambda$ for $G=(\U,M)$, then there is a state-removal $B_G$ of $A_G$ that satisfies $\vert \mS\vert \leq \kappa$, and has the $\tau$-SSP, and, given $\tau\cap\{\inp,\out\}\not=\emptyset$, it has the $\tau$-ESSP.

Let $\Ss=\{v_{\ell_0}, \dots, v_{\ell_{\lambda-1}}\}$ be a vertex cover for $G$, and let $B_G$ the TS that originates from $A_G$ by removing the states $f_{\ell_0,1}, f_{\ell_1,1},\dots, f_{\ell_{\lambda-1},1}$ (and thus the edges incident to these states), and nothing else.
Notice that, for all $j\in \{0,\dots, \lambda-1\}$, this reduces $F_{\ell_j}$ to $f_{\ell_j,0}$, since, for all $a\in \{a_0,\dots, a_{\lambda-1}\}$, the edge $f_{\ell_j,0}\edge{a}f_{\ell_j,1}$ is removed by the removal of $f_{\ell_j,1}$.

Obviously, $\vert \mS\vert\leq \kappa=\lambda$.

Let $B_G'$ be the TS that result by the removal of the edge $f_{\ell_j,0}\Edge{v_{\ell_j}}f_{\ell_j,1}$ for all $j\in \{0,\dots, \lambda-1\}$, that is, $B_G'$ corresponds to the edge removal defined in Section <ref>.
Obviously, every edge of $B_G$ is present in $B_G'$.
Hence, every region $R=(sup, sig)$ of $B_G'$ is a region of $B_G$, when restricted to its present states, and events.
Furthermore, if $(s,s')$ is an SSA of $B_G$, then it is also an SSA of $B_G'$, and solved by a corresponding region of Fact <ref>.

If $(e,s)$ is an ESSA of $B_G$ such that $e\not\in \{a_0,\dots, a_\lambda\}$, or $s\not\in \{f_{\ell_0},\dots, f_{\ell_{\lambda-1}}\}$, then $(e,s)$ is also an ESSA of $B_G'$, and solved by a corresponding region of Fact <ref>.

Hence, it only remains to argue that an ESSA $(e,s)$ is also solvable, if $e\in \{a_0,\dots, a_\lambda\}$ and $s\in \{f_{\ell_0},\dots, f_{\ell_{\lambda-1}}\}$.
The following region $R=(sup, sig)$ accomplishes this:
$sup(\iota)=0$, and, for all $e\in E(B_G)$,

if $e\in \{a_0,\dots, a_\lambda\}$, then $sig(e)=\inp$, and if $e\in \{z_{\ell_0},\dots, z_{\ell{\lambda-1}}\}$, then $sig(e)=\nop$, otherwise $sig(e)=\swap$.

Notice that this definition implies $sup(f_{\ell_j,0})=0$ for all $j\in \{0,\dots,\lambda-1\}$ (by $sig(z_{\ell_j})=\nop$), and $sup(f_{i,1})=sup(f_{i,0}) - 1= 0$ for all $i\in \{0,\dots, n-1\}\setminus \{\ell_0,\dots, \ell_{\lambda-1}\}$ (by $sig(z_i)=sig(v_i)=\swap$, respectively $sig(a_0)=\dots=sig(a_{\lambda})=\inp$) such that $R$ is actually a well-defined region that solves the remaining ESSA.
This proves the lemma.

§.§ Proof of Theorem <ref>(<ref>) for the Types without $\inp$ and $\out$

In the following, as long as not explicitly stated otherwise, let $\emptyset\neq\omega\subseteq \{\free,\used\}$, and $\tau=\{\nop,\swap\}\cup\omega$.

The following reduction transforms an input $(G,\lambda)$, where $G=(\U,M)$, to an instance $(A_G,\kappa)$:
$\kappa=\lambda$, and $A_G$ is the TS that is defined just like the one in Section <ref>, but, for all $i\in \{0,\dots, m-1\}$, and for all $j\in \{1,2\}$, does neither implement the edge $\iota\edge{y_i^j}t_{i,j}$ nor the edge $\iota\edge{y_i^j}t_{i,j}$.
Hence, for every state-removal $B_G$ of $A_G$, if there is $i\in \{0,\dots, m-1\}$, such that $t_{i,1}$ is missing in $B_G$ (implying that the edge $t_{i,1}\edge{v_{i_1}}t_{i,2}$ is also removed), then $t_{i,2}$ is also removed, since this state would not be reachable from the initial state $\iota$ otherwise, which is a contradiction.
Similarly, if $t_{i,0}$ is removed, then so are $t_{i,1}$, and $t_{i,2}$.

In the following, we argue that $(A_G,\kappa)$ is a yes-instance (i.e., it allows a fitting state-removal that has the ESSP, and, when realization is considered, the SSP) if and only if $(G,\lambda)$ is a yes-instance.

If there is a state-removal $B_G$ of $A_G$ that satisfies $\vert \mS\vert \leq \kappa$ and has the $\tau$-ESSP, then there is a vertex cover of size at most $\lambda$ for $G=(\U,M)$.

Let $B_G$ be a state removal of $A_G$ that satisfies $\vert \mS\vert \leq \kappa$ and has the $\tau$-ESSP, and
let $\Ss=\{v\in \U \mid \exists s\in \mS: \edge{v}s\}$.
Note that  $\vert \Ss\vert \leq \vert \mS\vert \leq\kappa=\lambda$, which can be seen as follows:
On the one hand, if $t_{i,1}\in \mS$ for some $i\in \{0,\dots, m-1\}$, which implies $v_{i_0}, v_{i_1}\in \Ss$, then $t_{i,2}\in \mS$.
(Otherwise, $t_{i,2}$ would no reachable, which is excluded by the definition of TS.)

On the other hand, there is no other kind of state that is adjacent to two different vertex events.

We argue that $\Ss$ is a vertex cover:

Let $i\in \{0,\dots, m-1\}$ be arbitrary but fixed.
If $\{v_{i_0},v_{i_1}\}\cap\Ss=\emptyset$, then $T_i$, and $F_{i_0}$, and $F_{i_1}$ are completely present in $B_G$.
Similar to the proof of Lemma <ref> one argues that this contradicts the $\tau$-ESSP of $B_G$.
Hence $\{v_{i_0},v_{i_1}\}\cap\Ss\not=\emptyset$, and the arbitrariness of $i$ implies the claim.

For the converse direction, we present the following lemma:

If there is a vertex cover of size at most $\lambda$ for $G=(\U,M)$, then there is a state-removal $B_G$ of $A_G$ that satisfies $\vert \mS\vert \leq \kappa$ and has the $\tau$-ESSP, and the $\tau$-SSP.

Let $\Ss=\{v_{\ell_0},\dots, v_{\ell_{\lambda-1}}\}$ be a vertex cover of $G$, and let $B_G$ be the TS that originates from $A_G$ by the removal of the states $f_{\ell_0,1}, f_{\ell_1,1}, \dots, f_{\ell_{\lambda-1},1}$ (and the corresponding adjacent edges), and nothing else.
One finds our that $B_G$ is a well-defined (i.e. reachable) TS, which satisfies $\vert \mS\vert \leq \kappa=\lambda$.
Similar to the proof of Lemma <ref>, one argues that $B_G$ has both the $\tau$-SSP, and the $\tau$-ESSP.
The claim follows.

§ CONCLUDING REMARKS

In this paper, we characterized the computational complexity of finding a label-splitting of a TS $A$ that allows implementing $\tau$-net for all types $\tau=\{\nop,\swap\}\cup \omega$ with $\omega\subseteq \{\inp,\out,\used,\free\}$ and all implementations previously considered in the literature.
By the results of [20, 21, 22], the synthesis problem aiming at language-simulation and realization is NP-complete for all types $\tau=\{\nop,\swap\}\cup\omega$ with $\omega\subseteq \{\inp,\out,\res,\set,\used,\free\}$ and $\omega\cap\{\inp,\out,\used,\free\}\neq\emptyset$ and $\omega\cap\{\set,\res\}\neq\emptyset$.
Hence, their corresponding label splitting problem is also NP-complete.
Moreover, similar to the proof of Theorem <ref>, one argues

that label splitting aiming at language-simulation or realization is trivial for $\tau=\{\nop,\swap\}\cup\omega$ when $\omega\subseteq \{\res,\set\}$:
the relabeling of an input TS $A$ would result in some ESSAs, and since $\tau$ does not allow for solving ESSAs, either $A$ already has the separation properties or it has to be rejected.
Moreover, we already know that synthesis aiming at embedding is NP-complete for all Boolean types $\tau$ with $\{\nop,\swap\}\subseteq\tau$ and $\tau\cap\{\res,\set\}=\emptyset$ [26].
Hence, again their corresponding label-splitting problem is also NP-complete.
Altogether, with the present work, the complexity of $\tau$-label-splitting is characterized for all 64 Boolean types with $\{\nop,\swap\}\subseteq\tau$ and all implementations.
It remains future work to determine the complexity of the label-splitting problem for the -free and -equipped Boolean types whose underlying synthesis problem is in P.

In order to avoid to deal with the intractability of label-splitting, we also analyzed the complexity of various element removal techniques to render a $\tau$-implementable TS, for similar types $\tau\cup\omega$ with $\emptyset\not=\omega\subseteq\{\inp,\out, \used,\free\}$.
Unfortunately, it turns out that these techniques are also NP-complete for $\tau$, and all implementations.
Hence, it remains future work to investigate whether other techniques that make TS implementable may have a better complexity, as, for example, the insertion of states, edges or events.

Moreover, one might consider $\kappa$ as a parameter and investigate the discussed modification techniques

from the point of view of parameterized complexity.

§.§.§ Acknowledgements.

We would like to thank the unknown reviewers of the previous versions of this paper
for their valuable comments.

[1]
Badouel E, Caillaud B, Darondeau P.
Distributing Finite Automata Through Petri Net Synthesis.
Formal Asp. Comput., 2002.

[2]
van der Aalst WMP.
Process Mining - Discovery, Conformance and Enhancement of Business
Springer, 2011.

[3]
Holloway LE, Krogh BH, Giua A.
A Survey of Petri Net Methods for Controlled Discrete Event
Discrete Event Dynamic Systems, 1997.

[4]
Cortadella J, Kishinevsky M, Kondratyev A, Lavagno L, Yakovlev A.
A region-based theory for state assignment in speed-independent
IEEE Trans. on CAD of Integrated Circuits and Systems,

[5]
Badouel E, Bernardinello L, Darondeau P.
Petri Net Synthesis.
Texts in Theoretical Computer Science. An EATCS Series. Springer,

[6]
Carmona J.
The Label Splitting Problem.
Trans. Petri Nets Other Model. Concurr., 2012.

[7]
Cortadella J, Kishinevsky M, Lavagno L, Yakovlev A.
Deriving Petri nets from finite transition systems.
IEEE Transactions on Computers, 1998.

[8]
Schlachter U, Wimmel H.
Relabelling LTS for Petri Net Synthesis via Solving Separation
Trans. Petri Nets Other Model. Concurr., 2019.

[9]
Schlachter U, Wimmel H.
Optimal Label Splitting for Embedding an LTS into an arbitrary
Petri Net Reachability Graph is NP-complete.
CoRR, 2020.

[10]
Tredup R.
Finding an Optimal Label-Splitting to Make a Transition System Petri
Net Implementable: a Complete Complexity Characterization.
In: Proceedings of the 21st Italian Conference on Theoretical
Computer Science, Ischia, Italy, September 14-16, 2020. 2020 pp. 131–144.

[11]
Devillers RR, Tredup R.
Some Basic Techniques allowing Petri Net Synthesis: Complexity and
Algorithmic Issues.
CoRR, 2021.

[12]
Tredup R.
Edge, Event and State Removal: The Complexity of Some Basic
Techniques that Make Transition Systems Petri Net Implementable.
In: Application and Theory of Petri Nets and Concurrency - 42nd
International Conference, PETRI NETS 2021, Virtual Event, June 23-25,
2021, Proceedings. 2021 pp. 253–273.

[13]
Badouel E, Darondeau P.
Trace Nets and Process Automata.
Acta Inf., 1995.

[14]
Kleijn J, Koutny M, Pietkiewicz-Koutny M, Rozenberg G.
Step semantics of boolean nets.
Acta Inf., 2013.

[15]
Montanari U, Rossi F.
Contextual Nets.
Acta Inf., 1995.

[16]
Pietkiewicz-Koutny M.
Transition Systems of Elementary Net Systems with Inhibitor Arcs.
In: ICATPN, volume 1248 of Lecture Notes in Computer
Science. Springer, 1997 pp. 310–327.

[17]
Rozenberg G, Engelfriet J.
Elementary Net Systems.
In: Petri Nets, volume 1491 of Lecture Notes in Computer
Science. Springer, 1996 pp. 12–121.

[18]
Schmitt V.
Flip-Flop Nets.
In: STACS, volume 1046 of Lecture Notes in Computer Science.
Springer, 1996 pp. 517–528.

[19]
Badouel E, Bernardinello L, Darondeau P.
The Synthesis Problem for Elementary Net Systems is NP-Complete.
Theor. Comput. Sci., 1997.

[20]
Tredup R.
The Complexity of Synthesizing nop-Equipped Boolean Petri
Nets from $g$-Bounded Inputs.
Trans. Petri Nets Other Model. Concurr., 2021.

[21]
Tredup R, Rosenke C.
The Complexity of Synthesis for 43 Boolean Petri Net Types.
In: TAMC, volume 11436 of Lecture Notes in Computer Science.
Springer, 2019 pp. 615–634.

[22]
Tredup R, Rosenke C.
On the Hardness of Synthesizing Boolean Nets.
In: ATAED@Petri Nets/ACSD, volume 2371 of CEUR Workshop
Proceedings. CEUR-WS.org, 2019 pp. 71–86.

[23]
Badouel E, Bernardinello L, Darondeau P.
Polynomial Algorithms for the Synthesis of Bounded Nets.
In: TAPSOFT, volume 915 of Lecture Notes in Computer
Science. Springer, 1995 pp. 364–378.

[24]
Tredup R.
The Complexity of the Label-Splitting-Problem for Flip-Flop-Nets.
In: Reachability Problems - 14th International Conference, RP 2020,
Paris, France, October 19-21, 2020, Proceedings. 2020 pp. 148–163.

[25]
Garey MR, Johnson DS.
Computers and Intractability: A Guide to the Theory of
W. H. Freeman, 1979.
ISBN 0-7167-1044-7.

[26]
Tredup R, Erofeev E.
The Complexity of Boolean State Separation.
In: Theoretical Aspects of Computing - ICTAC 2020 - 17th
International Colloquium, Macau, China, November 30 - December 4, 2020,
Proceedings. 2020 pp. 123–142.

§ ADDITIONAL ILLUSTRATIONS FOR THE PROOF OF LEMMA <REF>

In this section, we let $(G,\lambda)$ and $M=\{v_0,v_2\}$ as in  Example <ref>, and let $A_G$ and $B_G$ be defined in accordance to Section <ref>.
The following figures shall serve a supporting illustrations of the regions as defined for the proof of Lemma <ref>.
All figures depict the TS $B_G$.
Moreover, for every figure, the red colored area marks exactly the states of $B_G$ that have a positive support in accordance to the region that is illustrated.

[new set = import nodes]
[nodes=set=import nodes]
(bot1) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 0,1,3 [red!20] (ı) circle (0.3cm);
(bot1) at (bot1) $\bot_0$;
ıin 0,...,4 (ı) at (ı) $t_{0,\i}$;

(import nodes);

[yshift=-1cm, nodes=set=import nodes]
(bot2) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 1 [red!20] (ı) circle (0.3cm);
(bot2) at (bot2) $\bot_1$;
ıin 0,...,4 (ı) at (ı) $t_{1,\i}$;

(import nodes);

[yshift=-2cm, nodes=set=import nodes]
(bot3) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 3,4 [red!20] (ı) circle (0.3cm);
(bot3) at (bot3) $\bot_2$;
ıin 0,...,4 (ı) at (ı) $t_{2,\i}$;

(import nodes);

[yshift=-3cm, nodes=set=import nodes]
(bot4) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 0,2 [red!20] (ı) circle (0.3cm);
(bot4) at (bot4) $\bot_3$;
ıin 0,...,4 (ı) at (ı) $t_{3,\i}$;

(import nodes);

[yshift=-4cm,nodes=set=import nodes]
(bot5) at (0,0);
(bot5) at (0,0) $\bot_4$;
ıin 0,...,4  (ı) at (1.8cm+ ı*1.8cm,0) ;
ıin 3,4 [red!20] (ı) circle (0.3cm);
ıin 0,...,4  (ı) at (ı) $t_{4,\i}$;

(import nodes);

(bot1) edge [->] node[left] $\ominus_1$  (bot2);
(bot2) edge [->] node[left] $\ominus_2$  (bot3);
(bot3) edge [->] node[left] $\ominus_3$  (bot4);
(bot4) edge [->] node[left] $\ominus_4$  (bot5);

A sketch of region $R_1=(sup,sig)$ of Lemma <ref>, where $i=3$ and $j=0$ and $\ell$ does not exists (since $v_1$ is adjacent to two edges in $G$).
In particular, $v_{3_0}=v_{j_0}=v_1$ and $v_{3_1}=v_2$ and $v_{3_0}=v_0$.
Moreover, $sig(v_1)=\inp$ and $sig(e)=\swap$ if $e\in \{w_0,w_3,v_0,v_2\}$ and $sig(e)=\nop$ otherwise.

[new set = import nodes]
[nodes=set=import nodes]
(bot1) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 2,3 [red!20] (ı) circle (0.3cm);
(bot1) at (bot1) $\bot_0$;
ıin 0,...,4 (ı) at (ı) $t_{0,\i}$;

(import nodes);

[yshift=-1cm, nodes=set=import nodes]
(bot2) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 0,1 [red!20] (ı) circle (0.3cm);
(bot2) at (bot2) $\bot_1$;
ıin 0,...,4 (ı) at (ı) $t_{1,\i}$;

(import nodes);

[yshift=-2cm, nodes=set=import nodes]
(bot3) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);

(bot3) at (bot3) $\bot_2$;
ıin 0,...,4 (ı) at (ı) $t_{2,\i}$;

(import nodes);

[yshift=-3cm, nodes=set=import nodes]
(bot4) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 1,3,4 [red!20] (ı) circle (0.3cm);
(bot4) at (bot4) $\bot_3$;
ıin 0,...,4 (ı) at (ı) $t_{3,\i}$;

(import nodes);

[yshift=-4cm,nodes=set=import nodes]
(bot5) at (0,0);
(bot5) at (0,0) $\bot_4$;
ıin 0,...,4  (ı) at (1.8cm+ ı*1.8cm,0) ;
ıin 0,1,2 [red!20] (ı) circle (0.3cm);
ıin 0,...,4  (ı) at (ı) $t_{4,\i}$;

(import nodes);

(bot1) edge [->] node[left] $\ominus_1$  (bot2);
(bot2) edge [->] node[left] $\ominus_2$  (bot3);
(bot3) edge [->] node[left] $\ominus_3$  (bot4);
(bot4) edge [->] node[left] $\ominus_4$  (bot5);

A sketch of region $R_2=(sup,sig)$ of Lemma <ref>, where $i=3$ and $j=1$ and $\ell=4$.
In particular, $v_{3_1}=v_{1_1}=v_{4_0}=v_2$ and $v_{3_0}=v_{0_1}=v_1$.
Moreover, $sig(v_2)=\inp$ and $sig(e)=\swap$ if $e\in \{w_1,w_4,v_1\}$ and otherwise $sig(e)=\nop$.

[new set = import nodes]
[nodes=set=import nodes]
(bot1) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);

(bot1) at (bot1) $\bot_0$;
ıin 0,...,4 (ı) at (ı) $t_{0,\i}$;

(import nodes);

[yshift=-1cm, nodes=set=import nodes]
(bot2) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 0,1 [red!20] (ı) circle (0.3cm);
(bot2) at (bot2) $\bot_1$;
ıin 0,...,4 (ı) at (ı) $t_{1,\i}$;

(import nodes);

[yshift=-2cm, nodes=set=import nodes]
(bot3) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);

(bot3) at (bot3) $\bot_2$;
ıin 0,...,4 (ı) at (ı) $t_{2,\i}$;

(import nodes);

[yshift=-3cm, nodes=set=import nodes]
(bot4) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 0,1 [red!20] (ı) circle (0.3cm);
(bot4) at (bot4) $\bot_3$;
ıin 0,...,4 (ı) at (ı) $t_{3,\i}$;

(import nodes);

[yshift=-4cm,nodes=set=import nodes]
(bot5) at (0,0);
(bot5) at (0,0) $\bot_4$;
ıin 0,...,4  (ı) at (1.8cm+ ı*1.8cm,0) ;
ıin 0,1,2 [red!20] (ı) circle (0.3cm);
ıin 0,...,4  (ı) at (ı) $t_{4,\i}$;

(import nodes);

(bot1) edge [->] node[left] $\ominus_1$  (bot2);
(bot2) edge [->] node[left] $\ominus_2$  (bot3);
(bot3) edge [->] node[left] $\ominus_3$  (bot4);
(bot4) edge [->] node[left] $\ominus_4$  (bot5);

A sketch of region $R_3=(sup,sig)$ of Lemma <ref>, where $i=3$ and $j=1$ and $\ell=4$.
In particular, $v_{3_1}=v_{1_1}=v_{4_0}=v_2$.
Moreover, $sig(v_2)=\inp$ and $sig(e)=\swap$ if $e\in \{w_1,w_3, w_4\}$ and $sig(e)=\nop$ otherwise.

[new set = import nodes]
[nodes=set=import nodes]
(bot1) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 2,3 [red!20] (ı) circle (0.3cm);
(bot1) at (bot1) $\bot_0$;
ıin 0,...,4 (ı) at (ı) $t_{0,\i}$;

(import nodes);

[yshift=-1cm, nodes=set=import nodes]
(bot2) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 0,...,3 [red!20] (ı) circle (0.3cm);
(bot2) at (bot2) $\bot_1$;
ıin 0,...,4 (ı) at (ı) $t_{1,\i}$;

(import nodes);

[yshift=-2cm, nodes=set=import nodes]
(bot3) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);

(bot3) at (bot3) $\bot_2$;
ıin 0,...,4 (ı) at (ı) $t_{2,\i}$;

(import nodes);

[yshift=-3cm, nodes=set=import nodes]
(bot4) at (0,0);
ıin 0,...,4 (ı) at (ı*1.8cm+1.8cm,0);
ıin 0,3 [red!20] (ı) circle (0.3cm);
(bot4) at (bot4) $\bot_3$;
ıin 0,...,4 (ı) at (ı) $t_{3,\i}$;

(import nodes);

[yshift=-4cm,nodes=set=import nodes]
(bot5) at (0,0);
(bot5) at (0,0) $\bot_4$;
ıin 0,...,4  (ı) at (1.8cm+ ı*1.8cm,0) ;
ıin 0 [red!20] (ı) circle (0.3cm);
ıin 0,...,4  (ı) at (ı) $t_{4,\i}$;

(import nodes);

(bot1) edge [->] node[left] $\ominus_1$  (bot2);
(bot2) edge [->] node[left] $\ominus_2$  (bot3);
(bot3) edge [->] node[left] $\ominus_3$  (bot4);