=Paper=
{{Paper
|id=Vol-2625/paper06
|storemode=property
|title=On the Complexity of Synthesis of nop-Free Boolean Petri Nets
|pdfUrl=https://ceur-ws.org/Vol-2625/paper-05.pdf
|volume=Vol-2625
|authors=Ronny Tredup,Evgeny Erofeev
|dblpUrl=https://dblp.org/rec/conf/apn/TredupE20
}}
==On the Complexity of Synthesis of nop-Free Boolean Petri Nets==
https://ceur-ws.org/Vol-2625/paper-05.pdf
On the Complexity of Synthesis of nop-Free
Boolean Petri Nets
Ronny Tredup( )1 and Evgeny Erofeev?2
1
Universität Rostock, Institut für Informatik, Theoretische Informatik,
Albert-Einstein-Straße 22, 18059, Rostock (ronny.tredup@uni-rostock.de)
2
Department of Computing Science, Carl von Ossietzky Universität Oldenburg,
D-26111 Oldenburg, Germany (evgeny.erofeev@informatik.uni-oldenburg.de)
Abstract. In a Boolean Petri net, the interaction nop allows places and
transitions to be independent, so that the firing of a transition does not
affect the marking of a place, and vice versa. Recently, the complexity
of synthesis of nets equipped with nop has been investigated thoroughly,
while the question for the rest 128 types of nets remains open. This work
tackles the case of nop-free nets synthesis, that is, the Boolean nets where
places and transitions are always related via interactions that are able to
modify the marking of a place. In this paper, we show that, for nop-free
nets, the absence of swap leads always to a polynomial time synthesis
procedure. Moreover, we give a first hint, that the presence of swap might
make the synthesis for these types NP-complete.
Keywords: Boolean Petri Net, Synthesis, transition systems, time complexity
1 Introduction
Boolean Petri nets is a well-known formalism for modeling and analysing of
concurrent and distributed systems. This class of Petri nets assumes each place to
be a Boolean condition which is true if the place is marked, i.e. contains a token,
and false otherwise. Hence, the places can be treated as indicators for properties
of the modeled system. The interconnections between places and transitions of
a Boolean net are given through the Boolean interactions. These interactions
are partial binary functions from {0, 1} to {0, 1}, and the precise set of the
interactions which are employed in a given net determines the Boolean type of
the net.
By means of the notion of type of nets, Boolean Petri nets provide a uniform
approach for defining of many classes of nets, e.g. event/condition nets [1],
elementary net systems [1], SET nets [3], which allows researchers to comprise
models of different kinds in a generic manner [1]. Eight binary functions are applied
as interactions between places and transitions in Boolean nets: no operation (nop),
input (inp), output (out), unconditionally set to true (set), unconditionally reset
?
Supported by DFG through grant Be 1267/16-1 ASYST.
66
Copyright © 2020 for this paper by its authors.
Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
to false (res), inverting (swap), test if true (used), and test if false (free). These
interactions define in which way a place p and a transition t influence each other:
The interaction inp (out) defines that p must be true (false) before and false
(true) after the firing of t; free (used) implies that the firing of t proves that p
is false (true); nop means that p and t do not affect each other at all; res (set)
implies that p may initially be both false or true but after the firing of t it is
false (true); swap means that t inverts the current Boolean value of p. With these
eight interactions, 256 different Boolean types of nets are possible in total.
In the previous works [9–11], the complexity of Boolean Petri net syn-
thesis has been investigated for the types which allow the interaction nop.
Among others, these types include some well-known classes, e.g. contextual
nets {nop, inp, out, used, free} [4], inhibitor nets {nop, inp, out, free} [6], trace nets
{nop, inp, out, set, res, used, free} [2], flip-flop nets {nop, inp, out, swap} [7]. Besides,
for the types with nop, the complexity of synthesis has been studied in a special
setting with restrictions on the synthesis input [8], which has some practical
applications in hardware design. At the same time, the complexity of synthesis for
128 Boolean types which do not allow a place and a transition to be independent,
i.e. the nop-free types of nets, remains an uncharted research area. This paper
aims at compensating of this skewness and at filling the gap in theory. Hence,
the paper focusses on the synthesis of nop-free types, and makes an effort to
reach the complete characterization for the complexity of Boolean net synthesis.
The limitations of the target net class imply a structural property of admissible
behaviors, which we call the single sink property. The property requires all the
edges that carry the same label, to have a unique common target state. Along the
consideration, we especially distinguish between nop-free types which allow the
interaction swap, and the ones which do not. In comparison to the other Boolean
interactions, nop and swap are the only two of eight which on the one hand do
not have a symmetrical dual interaction, and on the other hand, have 1 and 0
both as their input and their output. As we shall prove, this peculiarity indeed
makes a big difference: while the synthesis of nop-free types without swap will be
proved polynomial, we present a first hint that synthesis might be NP-complete
at least for some nop-free types which admit swap.
The paper is organized as follows. After introducing of the necessary definitions
in Section 2, the main results will be presented in Section 3. We begin with
the polynomial cases in Section 3 and then continue with the hardness result in
Section 4. Section 5 summarises the work and suggests an outlook of possible
directions of the further research.
2 Preliminaries
Transition Systems. A (deterministic) transition system (TS, for short) A =
(S, E, δ) is a directed labeled graph with the set of nodes S (called states), the
set of labels E (called events) and partial transition function δ : S × E −→ S,
where δ(s, e) = s0 is interpreted as s e s0 . For s e s0 , we say that s is a source
and s0 is a sink of e, respectively. If δ(s, e) is defined, we say that event e occurs
67
at state s, denoted by s e . An initialized TS A = (S, E, δ, s0 ) is a TS with a
distinct initial state s0 ∈ S where every state s ∈ S is reachable from s0 by a
directed labeled path.
Boolean Types of Nets [1]. The following notion of Boolean types of nets
allows to capture all Boolean Petri nets in a uniform way. A Boolean type of net
τ = ({0, 1}, Eτ , δτ ) is a TS such that Eτ is a subset of the Boolean interactions:
Eτ ⊆ I = {nop, inp, out, set, res, swap, used, free}. Each interaction i ∈ I is a
binary partial function i : {0, 1} → {0, 1} as defined in Figure 1. For all x ∈ {0, 1}
and all i ∈ Eτ , the transition function of τ is defined by δτ (x, i) = i(x). Since a
type τ is completely determined by Eτ , we often identify τ with Eτ , cf. Figure 2.
τ -Nets. Let τ ⊆ I. A Boolean Petri net N = (P, T, f, M0 ) of type τ (a
τ -net) is given by finite disjoint sets P of places and T of transitions, a (total)
flow function f : P × T → τ , and an initial marking M0 : P −→ {0, 1}. A
transition t ∈ T can fire in a marking M : P −→ {0, 1} if δτ (M (p), f (p, t)) is
defined for all p ∈ P . By firing, t produces the marking M 0 : P −→ {0, 1} where
M 0 (p) = δτ (M (p), f (p, t)) for all p ∈ P , denoted by M t M 0 . The behavior of
τ -net N is captured by a transition system AN , called the reachability graph of
N . The states set RS(N ) of AN consists of all markings that can be reached
from initial state M0 by sequences of transition firings.
τ -Regions. Let τ ⊆ I. If an input A of τ -synthesis allows a positive decision,
we want to construct a corresponding τ -net N . TS represents the behavior of a
modeled system by means of global states (states of TS) and transitions between
them (events). Dealing with a Petri net, we operate with local states (places) and
their changing (transitions), while the global states of a net are markings, i.e.,
combinations of local states. Since A and AN must be isomorphic, 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 τ -region
of A = (S, E, δ, s0 ) is a pair (sup, sig) of support sup : S → {0, 1} and signature
sig : E → Eτ where every edge s e s0 of A leads to an edge sup(s) sig(e) sup(s0 )
of type τ . 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 ∈ RS(N ) that corresponds to s ∈ S(A). Every τ -region R = (sup, sig)
partitions the set of states S into two disjoint subsets: S = S0R ∪ S1R , where
SiR = {s ∈ S | sup(s) = i}, i ∈ {0, 1}. Since each of S0R and S1R uniquely defines
sup, we will often identify S1R with sup, for R.
Every set R of τ -regions of A defines the synthesized τ -net NAR = (R, E, f, M0 )
with f ((sup, sig), e) = sig(e) and M0 ((sup, sig)) = sup(s0 ) for all (sup, sig) ∈
R, e ∈ E. To ensure that the input behavior is captured by the synthesized net,
we have to discern 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 problems. A pair (s, s0 ) of distinct states of A defines a state separation
atom (SSP atom). A τ -region R = (sup, sig) solves (s, s0 ) if sup(s) 6= sup(s0 ). If
every SSP atom of A is τ -solvable then A has the τ -state separation property
(τ -SSP, for short). A pair (e, s) of event e ∈ E and state s ∈ S where e does not
68
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
Fig. 1: All Interactions i of I. If a cell is empty, then i is undefined on the respective x.
s1 r1
set, swap
used
free 0 1 a a c b 0 1
inp set
swap
s0 r0
τ A1 A2 τ̃
Fig. 2: Left: τ = {inp, free}. Right: τ̃ = {swap, used, set}. The TS A1 has no ESSP
atoms. Hence, it has the τ -ESSP and τ̃ -ESSP. The only SSP atom of A1 is (s0 , s1 ).
It is τ̃ -solvable by R1 = (sup1 , sig1 ) with sup1 (s0 ) = 0, sup1 (s1 ) = 1, sig1 (a) = swap.
Thus, A1 has the τ̃ -admissible set R = {R1 }, and the τ̃ -net NA R
= ({R1 }, {a}, M0 , f )
with M0 (R1 ) = sup1 (s0 ) and f (R1 , a) = sig1 (a) solves A1 . The SSP atom (s0 , s1 ) is
not τ -solvable, thus, neither is A1 . TS A2 has ESSP atoms (b, r1 ) and (c, r0 ), which
are both τ̃ -unsolvable. The only SSP atom (r0 , r1 ) in A2 can be solved by τ̃ -region
R2 = (sup2 , sig2 ) with sup2 (r0 ) = 0, sup2 (r1 ) = 1, sig2 (b) = set, sig2 (c) = swap. Thus,
A2 has the τ̃ -SSP, but not the τ̃ -ESSP. None of the (E)SSP atoms of A2 can be solved
by any τ -region.
occur, that is ¬s e , defines an event state separation atom (ESSP atom). A
τ -region R = (sup, sig) solves (e, s) if sig(e) is not defined on sup(s) in τ , that
is, ¬δτ (sup(s), sig(e)). If every ESSP atom of A is τ -solvable then A has the
τ -event state separation property (τ -ESSP, for short).
A set R of τ -regions of A is called τ -admissible if for each (E)SSP atom there
is a τ -region R in R that solves it. The next lemma establishes the connection
between the existence of τ -admissible sets of A and (the solvability of) τ -synthesis:
Lemma 1 ([1]). A TS A is isomorphic to the reachability graph of a τ -net N
if and only if there is a τ -admissible set R of A such that N = NAR .
The synthesis problem for Boolean nets of type τ is formulated as follows.
τ -Synthesis:
Input: an initialized TS A.
Decide: whether there exists a τ -admissible set R of A.
If so: construct such a set R. Otherwise: reject input.
The present paper studies the complexity of τ -synthesis, for the types τ which
do not include the interaction nop. The following lemma helps to treat several
(isomorphic) types simultaneously:
Lemma 2 (Without Proof). If τ0 ∼ = τ1 , then an ESSP atom or a SSP atom
of A is τ0 -solvable if and only if it is τ1 -solvable.
69
3 Polynomial-Time Synthesis for nop-Free Boolean Types
of Nets
In this section, we focus on the nop-free Boolean types τ such that swap ∈
/ τ and
show that τ -synthesis is polynomial for these types of nets:
Theorem 1. If τ ⊆ {inp, out, res, set, used, free}, then τ -solvability is polynomial.
Notice that Theorem 1 covers exactly 64 types. The roadmap for the proof
of Theorem 1 is as follows: Firstly, we show that τ -synthesis is polynomial for
all 16 types τ that satisfy τ = {set, res} ∪ ω and ω ⊆ {inp, out, used, free}. After
that, we do the same for the 16 types τ that satisfy τ = {set} ∪ ω and ω ⊆
{inp, out, used, free}. By isomorphisms (Lemma 2), this implies also the tractability
of τ -synthesis for the 16 types τ with τ = {res} ∪ ω and ω ⊆ {inp, out, used, free}.
Finally, we show that τ -synthesis is polynomial for the remaining 16 types
that satisfy τ ⊆ {inp, out, free, used}, too. This approach covers all the types of
Theorem 1 and thus proves it.
In the context of τ -synthesis, the input TS represents the behavior of the
sought-for τ -net. Hence, restrictions of the possible behavioral patterns of the
net imply restrictions for structural properties of the admissible synthesis inputs.
In particular, if the firing of an arbitrary but fixed transition e of a τ -net N
leads always to the same global marking M , then any e-labeled arc in N ’s state
graph AN has the the same sink s that corresponds to M . We formulate this as
a structural property of TS:
Single-Sink Property. We say that TS A has the single-sink property if it
satisfies |{s ∈ S(A) | e s}| = 1 for all e ∈ E(A).
The following lemma establishes that if τ is nop-free and swap-free, then
state graphs of τ -nets have the single-sink property. In particular, this makes the
single-sink property a necessary condition for the τ -solvability of TS.
Lemma 3. Let τ ⊆ {inp, out, res, set, used, free}. If a TS A is τ -solvable, then it
has the single-sink property.
Proof. Let e ∈ E(A) be arbitrary but fixed. We have to show that all e-labeled
arcs have the same sink. By contraposition, assume there are arcs e s and
e s0 such that s 6= s0 . Since A is τ -solvable, there is a τ -region (sup, sig)
that solves the SSP atom (s, s0 ), that is, sup(s) 6= sup(s0 ). This contradicts
sig(e) ∈ {inp, out, res, set, used, free}, cf. Figure 1; hence the claim.
Clearly, whether a TS A has an event e ∈ E(A) that has two distinct sinks
s, s0 ∈ S(A) is decidable in polynomial time (in the size of A). In case of a positive
decision, we simply reject A by Lemma 3. Thus, justified by Lemma 3, in the
remainder of this section, unless stated explicitly otherwise, we assume that A is
an arbitrary but fixed TS that has the single-sink property.
70
3.1 Types τ such that τ = {set, res} ∪ ω and ω ⊆ {inp, out, used, free}
In the following, unless stated explicitly otherwise, let τ be a type such that
τ = {set, res} ∪ ω and ω ⊆ {inp, out, used, free}. Moreover, let τ0 , τ1 , τ2 and τ3 be
defined in accordance to Figure 3.
res set set res set, out set res set set free set set
0 1 0 1 0 1 0 1
res, inp res res used res res
τ0 τ1 τ2 τ3
Fig. 3: The isomorphic types τ0 = {inp, res, set} and τ1 = {out, res, set} as well as the
isomorphic types τ2 = {res, set, used} and τ3 = {res, set, free}.
The main insights about the structural nature of τ can be summarized as
follows: Firstly, every SSP atom (s, s0 ) of A is τ -solvable. Secondly, an ESSP
atom of A is τ -solvable if and only if it is τ0 -solvable or τ2 -solvable. Thirdly,
if α = (a, q) is an ESSP atom of α, then there are exactly two certain regions
for which have to ascertain if they solve α or not. No other regions have to be
considered at all.
The following lemma corresponds to the first statement. Its proof is construc-
tive and Figure 4.2 illustrates the region presented in lemma:
Lemma 4. The TS A has the τ -SSP.
Proof. If (s, s0 ) is a SSP atom of A, then the following τ -region R = (sup, sig)
solves (s, s0 ): sup(s0 ) = 0 and sup(q) = 1 for all q ∈ S(A) \ {s0 }; for all e ∈ E(A),
if e s0 then sig(e) = res, otherwise sig(e) = set. By definition of R and
A’s single-sink property, we have, for all e ∈ E(A) and all q, q 0 ∈ S(A), that
sig(e) = res if and only if q e q 0 implies q 0 = s0 . Thus, R is well defined and
satisfies sup(s) 6= sup(s0 ). Since (s, s0 ) was arbitrary, this proves the claim.
The following lemma paves us the way to the comprehension, that it is
sufficient for a given ESSP atom α = (a, q) to test if it is τ0 - or τ2 -solvable:
Lemma 5. If α = (a, q) is an ESSP atom of A, then α is τ -solvable if and only
there is τ 0 ∈ {τ0 , τ2 } and τ 00 ⊆ τ such that α is τ 0 -solvable and τ 0 ∼
= τ 00 .
Proof. Only-if : Let R = (sup, sig) be a τ -region of A. For a start, we claim that
there is a {res, set, sig(a)}-region R0 = (sup, sig 0 ) of A (with the same support
as R) as follows: for all e ∈ E(A), if e = a, then sig 0 (e) = sig(e); otherwise,
if sig(e) ∈ {inp, res, free} then sig 0 (e) = res, and if sig(e) ∈ {out, set, used},
then sig 0 (e) = set. That R0 is well-defined can be seen as follows: R is a τ -
sig(e)
region, thus s e s0 ∈ A implies sup(s) sup(s0 ) ∈ τ . Moreover, since, for
71
s0 e a e0
e
e e0
a e0
s s s0 p q
e e00
e a
e0 e00 s
(1) (2) (3)
a e0 a e0 a e0
0 0 0
a e a e a e
p q p q p q
00 00
e e e00
a a a
e00 s e00 s e00 s
(4) (5) (6)
Fig. 4: Sketches of regions, where the red colored area corresponds to the states with
a positive support. (1) Sketch of the separation of two states s 6= s0 which are both
sinks of the same event e, i.e., A does not have the single-sink property. If nop 6∈ τ
and swap 6∈ τ , then such a separating τ -region is ruled out in advance. (2) Sketch of
a region that separates the single-sink s of e from all other states of A according to
Lemma 4. (3) Sketch of the {inp, res, set}-region R that solves (a, q) in accordance to
Lemma 6.1 and, sketched by (4), its complementary {out, res, set}-region. (5) Sketch of
the {used, res, set}-region R that solves (a, q) in accordance to Lemma 6.2 and, depicted
by (6), its complementary {free, res, set}-region.
all i ∈ {inp, res, free} (i ∈ {out, set, used}), b i b0 implies b res b0 (b set b0 ) for all
sig 0 (e)
b, b0 ∈ {0, 1}, the definition also implies that sup(s) sup(s0 ) ∈ τ . Thus, R0
is a well-defined region.
Consequently, if R = (sup, sig) solves α, i.e., ¬sup(q) sig(a) , which implies
sig(a) ∈ {inp, out, used, free}, then the just introduced {res, set, sig(a)}-region R0
solves α. If sig(a) ∈ {inp, used}, then R0 is already a τ0 - or a τ2 -region, which
implies that α is τ0 - or τ2 -solvable. Otherwise, if sig(e) ∈ {out, free}, then either
{res, set, sig(a)} ∼
= τ0 or {res, set, sig(a)} =
∼ τ2 , and the claim follows by Lemma 2.
If : If τ ⊆ τ , then the claim is trivial. Otherwise, τ 0 ∼
0
= τ 00 ⊆ τ and, by
Lemma 2, α is τ -solvable. Hence, α is τ -solvable.
00
The following lemma tells us exactly for which τ0 - or τ2 -region we have to
look for:
Lemma 6. Let τ ∈ {τ0 , τ2 }, α = (a, q) an ESSP atom of A, and p the unique
sink of the a-labeled arcs. There is a τ -region R0 = (sup0 , sig 0 ) of A that solves α
if and only if there is a τ -region R = (sup, sig) as follows:
1. If sig 0 (a) = inp, then sup = S(A) \ {p, q} and, for all e ∈ E(A), if e = a,
then sig(e) = inp; if e = 6 a and e q ∈ A or e p ∈ A, then sig(e) = res;
otherwise sig(e) = set.
72
2. If sig 0 (a) = used, then sup = S(A) \ {q} and, for all e ∈ E(A), if e = a, then
sig(e) = used; if e q ∈ A, then sig(e) = res; otherwise sig(e) = set.
Proof. The if -direction is trivial.
Only-if : Let R0 = (sup0 , sig 0 ) be a τ -region, that solves α. By definition of τ
and ¬sup(q) sig(a) , we have either sig 0 (a) = inp and sup0 (q) = 0 or sig 0 (a) = used
and sup0 (q) = 0. The former case corresponds to τ = τ0 and the latter to τ = τ2 .
Assume, for a start, sig 0 (a) = inp and sup0 (q) = 0, which implies sup0 (p) = 0
and sup0 (s) = 1 for all s ∈ S(A) that satisfy s a . We argue that R as in (1.) is
well-defined. Notice that since A has the single-sink property, the definition of
R’s signature is consistent. Assume, for a contradiction, that there is an edge
s e s0 ∈ A such that sup(s) e sup(s0 ) 6∈ τ . If sup(s0 ) = 1, then s0 6∈ {p, q} and
thus sig(e) = set, which implies sup(s) e sup(s0 ) ∈ τ for all sup(s) ∈ {0, 1}.
If sup(s0 ) = 0, then s0 ∈ {p, q} and sig(e) ∈ {inp, res}. If sig(e) = res, then
sup(s) e sup(s0 ) ∈ τ for all sup(s) ∈ {0, 1}. Thus, sig(e) = inp, which implies
e = a and s0 = p. Since sup(s) e sup(s0 ) 6∈ τ , by sig(a) = inp, we get sup(s) = 0,
which implies s ∈ {p, q}. If s = q, then (a, q) is not an ESSP atom, a contradiction.
Otherwise, if s = p, then p e p ∈ A, which contradicts that R0 is a region such
that sig 0 (a) = inp. Thus sup(s) e sup(s0 ) ∈ τ .
Similarly, one argues that if sig 0 (a) = used and sup0 (q) = 0, the region of (2.)
is well defined. This proves the lemma.
Corollary 1. Let τ = {res, set} ∪ ω such that ω ⊆ {inp, out, used, free}, A be a
TS and |A| = |S(A)|2 ·|E(A)|. There is an algorithm that constructs a τ -admissible
set R of A if it exists and rejects A otherwise, which terminates in time O(|A|2 ).
Proof. If β (α) is an arbitrary but fixed (E)SSP atom, then to define a region in
accordance to Lemma 4 (Lemma 5), respectively its “isomorphic” counterpart,
and to check its validity is doable in time O(|A|). We have to check at most three
regions per atom and we have at most |S(A)|2 ≤ |A| SSP atoms (|S(A)|·|E(A)| ≤
|A| ESSP atoms) to solve. Thus, within the time O(|A|2 ) we have either a τ -
admissible set R that already defines a solving net implicitly be Lemma 1, or A
is not τ -solvable and has to be rejected.
3.2 Types τ such that τ = {set} ∪ ω and ω ⊆ {inp, out, used, free}
In the following, we investigate the types τ0 = {set}∪ω where ω ⊆ {inp, out, used}
and τ1 = {set, free} ∪ ω where ω ⊆ {inp, out, used} separately. The reason for this
distinction is that, for the former types, a solving region for an atom exists if and
only if a solving region exists whose support excludes exactly the necessary states.
More exactly, let α = (a, q) be an ESSP atom of A and p be the unique sink of
a-labeled edges in A. By definition, if R = (sup, sig) is a τ -region, that solves α,
then sig(a) = inp implies sup(p) = sup(q) = 0 (Figure 5.1), and sig(a) = used
implies sup(q) = 0 (Figure 5.2), and sig(a) = out implies sup(s) = 0 for all
s ∈ {s ∈ S(A) | s a } (cf. Figure 5.3). In other words, R’s support necessarily
73
a e0 a e0 a
0
e0
a a e e0
p q p q p q
e00 e00 a
a a
e00 s e00 s
e00
(1) (2) (3)
Fig. 5: Sketches of ESSP atom (a, p) solving τ -regions R = (sup, sig) according to
Lemma 7, i.e., τ = {set} ∪ ω and ω ⊆ {inp, out, used}: (1) sup = S(A) \ {p, q} and
sig(a) = inp; (2) sup = S(A) \ {q} and sig(a) = used; (3) sup = S(A) \ {s ∈ S(A) |
∃s0 ∈ S(A) : δ(s, a) = s0 } and sig(a) = out.
excludes {p, q}, {s ∈ S(A) | s a } and {q} if sig(a) = inp, sig(a) = out and
sig(a) = used, respectively. In the following subsection, we show that α is τ0 -
solvable if and only if there is a solving τ0 -region R = (sup, sig) whose support
excludes only the necessary states.
Unfortunately, the types covered by τ1 do not always have this property. For
τ1 , we rather work the other way around. In particular, we present an algorithm
that starts from a set of necessarily included states and extends it iteratively (by
further states) until it either reaches a separating region or a solution does not
exists.
Types τ such that τ = {set} ∪ ω and ω ⊆ {inp, out, used}. In the
remainder of this subsection, unless stated explicitly otherwise, let τ = {set} ∪ ω
and ω ⊆ {inp, out, used}.
It turns out, that τ allows to search for separating regions in a very specific
way. In particular, the following lemma shows that for a given ESSP atom α of A
there are at most three distinct τ -regions that solves α and how they are defined:
Lemma 7. Let α = (a, q) be an ESSP atom of A, and p the single sink of the
a-labeled arcs. There is a τ -region R = (sup0 , sig 0 ) that solves α if and only if
there is a τ -region R = (sup, sig) as follows:
1. If sig 0 (a) = inp, then sup = S(A) \ {p, q} and, for all e ∈ E(A), if e p or
e q, then sig(e) = inp, otherwise sig(e) = set.
2. If sig 0 (a) = used, then sup = S(A) \ {q} and, for all e ∈ E(A), if e = a, then
sig(e) = used; if e q, then sig(e) = inp, otherwise sig(e) = set.
3. If sig 0 (a) = out, then sup0 = S(A) \ {s ∈ S(A) | s a } and, for all e ∈ E(A),
if e = a, then sig(a) = out; if e s for some s ∈ {s ∈ S(A) | s a }, then
sig(e) = inp, otherwise sig(e) = set.
Proof. The if direction is trivial.
Only-If : Since R0 solves α, it holds sig 0 (a) ∈ {inp, out, used} and ¬sup0 (q) sig (a) .
0
Let’s consider the possible cases:
74
(1): Assume sig 0 (a) = inp, which implies sup0 (p) = sup0 (q) = 0. This implies,
for all e ∈ E(A), if there is s ∈ {p, q} such that e s, then sig(e) = inp and thus
sup0 (s0 ) = 1 and sup0 (s00 ) = 0 for all e-labeled edges s0 e s00 of A. In particular,
there is no e-labeled edge s e s0 such that s, s0 ∈ {p, q}. We argue that the region
R is well defined. Assume, for a contradiction, that there is s e s0 ∈ A such that
sup(s) sig(e) sup(s0 ) 6∈ τ . If sup(s0 ) = 1, implying s0 6∈ {p, q}, then sig(e) = set by
definition of sig. This would imply sup(s) sig(e) sup(s0 ) ∈ τ for all sup(s) ∈ {0, 1}.
Hence, sig(s0 ) = 0, which implies s0 ∈ {p, q} and thus sig 0 (e) = inp. Moreover,
by sup(s) sig(e) sup(s0 ) 6∈ τ and sup(s0 ) = 0, we get sup(s) = 0, which implies
s ∈ {p, q}, a contradiction. Hence, R is well-defined and solves α.
(2): If sig 0 (a) = used, then sup0 (p) = 1 and sup0 (q) = 0. This implies, for all
e ∈ E(A), if s e q, then sig(e) = inp and thus sup0 (s) = 1. This particularly
implies q e q 6∈ τ for all e ∈ E(A). Similar to (1), if there is s e s0 ∈ A such
that sup(s) sig(e) sup(s0 ) 6∈ τ , then sig(s0 ) = 0, which implies s0 = q and thus
sig 0 (e) = inp. Since sup(s) sig(e) sup(s0 ) 6∈ τ and sup(s0 ) = 0, we get sup(s) = 0
and thus s = q, a contradiction. Hence, R is well-defined and solves α.
(3): Assume sig 0 (a) = out, which implies sup0 (p) = sup0 (q) = 1 and sup(s) = 0
for all s ∈ {s ∈ S(A) | s a }. Moreover, for all e ∈ E(A), the latter implies
that if s e s0 ∈ E(A) such that s0 ∈ {s ∈ S(A) | s a }, then sig(e) = inp and
sup(s) = 1 and thus s 6∈ {s ∈ S(A) | s a }. Similar to the arguments of (1) and
(2), one get’s that this implies that R is well-defined and solves α.
The following lemma shows that we can also specifically search for regions
that solve a given SSP atom:
Lemma 8. Let β = (p, q) be an SSP atom of A. There is a τ -region R =
(sup0 , sig 0 ) that solves β if and only if there is a τ -region R = (sup, sig) as
follows:
1. sup = S(A) \ {p} and, for all e ∈ E(A), if e p, then sig(e) = inp, otherwise
sig(e) = set.
2. sup = S(A) \ {q} and, for all e ∈ E(A), if e p, then sig(e) = inp, otherwise
sig(e) = set.
Proof. The if-direction is trivial.
(Only-if ): Since R0 solves β, either sup0 (p) = 0 and sup0 (q) = 1 or sup0 (p) = 1
and sup0 (q) = 0 is true. We consider both cases, where the former corresponds
to the first condition of the lemma and the latter to the second.
For a start, let sup0 (p) = 0 and sup0 (q) = 1. Since sup0 (p) = 0, if s e q ∈
A, then sig 0 (e) = inp and sup0 (s) = 1 and thus s 6= q. We argue that the
definition of R according to (1.) is sound. Assume, for a contradiction, there is an
s e s0 ∈ A such that sup(s) sig(e) sup(s0 ) 6∈ τ . If sup(s0 ) = 1, then sig(e) = set
and sup(s) sig(e) sup(s0 ) ∈ τ . Thus, it is sup(s0 ) = 0, which implies s0 = q and
75
sig(e) = inp. By sig 0 (e) = inp, this also implies s 6= q and thus sup0 (s) = 1.
Hence, sup(s) sig(e) sup(s0 ) ∈ τ , a contradiction.
Similarly, if sup0 (p) = 1 and sup0 (q) = 0, then the region of (2.) exists.
Corollary 2. Let τ = {set} ∪ ω such that ω ⊆ {inp, out, used}, A be a TS and
|A| = |S(A)|2 · |E(A)|. There is an algorithm that constructs a τ -admissible set
R of A if it exists and rejects A otherwise, which terminates in time O(|A|2 ).
Proof. The proof is similar to the one for Corollary 1.
The Types τ such that τ = {set, free} ∪ ω and ω ⊆ {inp, out, used}. In
this subsection, unless stated explicitly otherwise, let τ be a type such that
τ = {set, free} ∪ ω and ω ⊆ {inp, out, used}. In what follows, we present an
algorithm that starts from a set of necessarily included states and extends
it iteratively (by further states) until it either reaches a separating region or
separation is not possible at all.
Lemma 9. Let S ⊆ S(A). The set S is a τ -support if and only if the following
conditions are true:
1. If s e s0 ∈ A such that S(s) = 1 and S(s0 ) = 0, then inp ∈ τ
2. For all e ∈ E(A), if s e s0 , q e q 0 ∈ A, then {(S(s), S(s0 )), (S(q), S(q 0 ))}
belongs to {{(0, 1)}, {(1, 1)}, {(1, 0)}, {(0, 0)}, {(0, 1), (1, 1)}}.
Proof. Only-if : Assume that S is a τ -support that allows the τ -signature sig, that
is, if s e s0 ∈ A, then sup(s) sig(e) sup(s0 ) ∈ τ . Clearly, by the definition of τ , if
s e s0 ∈ A such that S(s) = 1 and S(s0 ) = 0, then sig(e) = inp. Moreover, since
A has the single-sink property, for all e ∈ E(A), if s e s0 ∈ A and q e q 0 ∈ A,
then sup(s0 ) = sup(q 0 ). Furthermore, since res 6∈ τ , if sup(s0 ) = sup(q 0 ) = 0, then
{S(s), S(s0 ), S(q), S(q 0 )} cannot be {(1, 0), (0, 0)}. All the other possibilities are
allowed. This proves the Only-if-direction.
If : For all events e ∈ E(A), we define the following set Se = {(S(s), S(s0 )) |
s, s0 ∈ S(A) and s e s0 }. Notice that if |Se | ≥ 3, then there are edges s e s0
and q e q 0 such that {(S(s), S(s0 )), (S(q), S(q 0 ))} 6∈ {{(0, 1)}, {(1, 0)}, {(0, 0)},
{(0, 0)}, {(0, 1), (1, 1)}}. Moreover, if |Se | = 2, then one easily finds out that
Se = {{(0, 1), (1, 1)}}. Thus, the following definition of sig yields a well-defined
τ -region (S, sig) of A: for all e ∈ E(A), if Se = {(1, 0)}, then sig(e) = inp; if
Se = {(0, 1)}, then sig(e) = out if out ∈ τ , otherwise sig(e) = set; if Se = {(1, 1)},
then sig(e) = used if used ∈ τ , otherwise sig(e) = set; if Se = {(0, 1), (1, 1)}, then
sig(e) = set; otherwise, Se = {(0, 0)} and we then define sig(e) = free.
Example 1 (Algorithm application). Consider TS A with the set of states S(A) =
{ι, p, q, s} and E(A) = {a, b, c, d, e} depicted on the left in Figure 6. Let us apply
Algorithm 1 to A, with input τ = {set, free} and S = {ι, p, s} (the states from S
are colored in red in Figure 6). The first while-check in line 1 of the algorithm
76
finds the transition ι a q with S(ι) = 1 and S(q) = 0. Since inp ∈
/ τ , we remove
ι from S (line 2). The new set S is depicted in the middle of Figure 6. For
S = {p, s}, we repeat the while-check and find s b ι, q b ι with S(s) = 1 and
S(q) = S(ι) = 0. Accoridng to the line 2 of the algorithm, we remove s from S,
obtaining S = {p}. The new while-check does not report any inconsistency in S,
hence {p} is a valid τ -suport. The τ -region defined by this support is given on
the right of Figure 6.
p e p e p set
q q q
a a free
d d set
b c b c free free
ι ι ι
s s s
A b b free
Fig. 6: A {set, free}-region of TS A has been obtained from {ι, p, s} by Algorithm 1.
Lemma 10 (Algorithm 1). Let |A| = |S(A)|2 · |E(A)| and S ⊆ S(A). For the
input (A, S, τ )
1. sup terminates and its running time is at most O(|A|3 ).
2. sup returns a τ -support.
3. If R = (sup, sig) is an S-maximal τ -region such that sup ⊆ S, then sup
returns sup.
Proof. (1): If sup initiates the while loop, then it decreases the cardinality of S.
This implies that sup terminates after at most |S(A)| ≤ |A| while-loop iterations.
Moreover, the conditions of the while-loop can be tested in time O(|A|2 ). Hence
the claim.
(2): If sup returns S 0 , then the set S 0 does not satisfy the conditions of the
while-loop. Thus, by Lemma 9, S 0 allows a τ -signature sig that is defined in
correspondence to Lemma 9.
Algorithm 1: Sup
Input: Type {set, free} ⊆ τ ⊆ {inp, out, set, used, free}. TS A with states S(A)
and events E(A). S ⊆ S(A).
Result: A τ -support sup of A such that sup ⊆ S.
1 while (s
e
s0 ∈ A such that S(s) = 1, S(s0 ) = 0 and inp 6∈ τ ) or
(s s0 , q e q 0 ∈ A such that S(s) = 1, S(s0 ) = S(q) = S(q 0 ) = 0) do
e
2 S = S \ {s};
3 end
4 return S;
77
(3): By (1), sup terminates after at most t ≤ |S(A)| iterations of the while-
loop. Let S0 = S and, for i ∈ {1, . . . , t}, let Si be the set that originates from
Si−1 due to the execution of the i-th while-loop iteration. More exactly, after the
i − 1-th execution of the while-loop, we have Si−1 ; sup tests (for the i-th time)
the while-loop condition; if the condition is not satisfied, then Si = Si−1 and sup
terminates and returns Si , otherwise, the condition is satisfied and sup redefines
Si−1 , that is, Si = Si−1 \ {s}, where s corresponds to the while-loop condition.
In the following, we show by induction on the while-loop iterations that
if sup ⊆ Si−1 , then sup ⊆ Si . By the construction, we have sup ⊆ S = S0 .
Assume that i ∈ {1, . . . , t} and sup ⊆ Si−1 . If Si = Si−1 , then we have sup ⊆ Si
by the assumption. Otherwise, Si = Si−1 \ {s}, where s e s0 ∈ A such that
S(s) = 1, S(s0 ) = 0 and inp 6∈ τ or s e s0 , q e q 0 ∈ A such that S(s) =
1, S(s0 ) = S(q) = S(q 0 ) = 0. If sup 6⊆ Si = Si−1 \ {s}, then, by sup ⊆ Si−1 , we
have sup(s) = 1, sup(s0 ) = 0 and inp 6∈ τ , which is a contradiction, or we have
sup(s) = 1, sup(s0 ) = sup(q) = sup(q 0 ) = 0, which contradicts res 6∈ τ . This
implies sup ⊆ Si and, in particular, sup ⊆ St . If sup = 6 St , then there is a state
s ∈ St such that sup(s) = 0. This implies |St | > |sup|. Since sup is a S-maximal
support, this is a contradiction. Consequently, we have sup = St .
Lemma 11. Let {set, free} ⊆ τ ⊆ {inp, out, set, used, free}, let A be a TS and
let α = (a, q) be an ESSP atom and β = (q, q 0 ) be an SSP atom of A. If
R = (sup, sig) is a (maximal) τ -region that solves α, then Algorithm 1 provides
sup. In particular, sup is returned by sup(A, S(A) \ {s ∈ S(A) | a s}, τ ) or
sup is returned by sup(A, S(A) \ {q}, τ ).
Proof. Let R = (sup, sig) be a τ -region that solves α. Let p be the single-
sink of a in A. If sig(a) = inp and sup(q) = 0, then we invoke sup on input
S = S(A) \ {p, q}; if sig(a) = used and sup(q) = 0, then we invoke sup on input
S = S(A) \ {q}; if sig(a) = out and sup(q) = 1, then we invoke sup on input
S = S(A) \ {s ∈ S(A) | s a }; if sig(a) = free and sup(q) = 1, then we invoke
sup on input S = S(A) \ {s, s0 ∈ S(A) | s a s0 }. By Lemma 10, sup outputs
sup.
Corollary 3. Let τ be a type of nets such that τ = {set, free} ∪ ω and ω ⊆
{inp, out, used} and |A| = |S(A)|2 · |E(A)|. There is an algorithm that constructs
a τ -admissible set R of A if it exists and rejects A otherwise, which terminates
in time O(|A|4 ).
Proof. Since we have at most |S(A)| ≤ |A| SSP atoms and at most |S(A)| ·
|E(A)| ≤ |A| ESSP atoms to solve, the claim follows by and Lemma 10 and
Lemma 11.
The Types τ such that τ ⊆ {inp, out, used, free}. The following lemma
implies that τ -synthesis is solvable in polynomial time if τ ⊆ {inp, out, used, free}:
78
Lemma 12. Let τ ⊆ {inp, out, used, free}, let A be a TS and let α = (a, q) and
β = (q, q 0 ) be an ESSP and an SSP atom of A, respectively. Deciding if α or β
are τ -solvable requires polynomial time.
(Sketch). First of all, we observe that Se ∈ {{(0, 0)}, {(0, 1)}, {(1, 0)}, {(1, 1)}} for
all e ∈ E(A). If free ∈ τ , then we can test the τ -solvability of α (β) by a procedure
that originates as a modification of Algorithm 1: Firstly, we have to check if
s e s0 ∈ A such that S(s) = 0, S(s0 ) = 1 and out 6∈ τ or S(s) = 1, S(s0 ) = 1
and used 6∈ τ . In case of a positive decision, we have (at least) to remove s0 , that
is, S = S \ {s0 }. Similarly, if S(s) = 1, S(s0 ) = 0 and inp 6∈ τ , then we have to
update S = S \ {s}.
Secondly, we have to check for all e ∈ E(A) and all pairs s e s0 , q e q 0
if there is eτ ∈ τ such that Se ∈ {{(0, 0)}, {(0, 1)}, {(1, 0)}, {(1, 1)}} ∩ {(x, y) |
x eτ y ∈ τ }. In case of a negative decision, we have to update S, and one finds
out that this is deterministically possible for all Se under consideration.
Otherwise, if free 6∈ τ , then we obtain a similar procedure by starting from
a minimal necessary subset S ⊆ S(A) (for example, {s ∈ S(A) | s a } for
sig(a) = inp). Then increase S deterministically, until either we obtain a valid
support or we can correctly conclude that such a support does not exist.
4 NP-Completeness of the Single-Instance ESSP Problem
for a nop-Free Type
Let τ be a Boolean type of nets and A be a TS and α be an ESSP atom of
A. The single-instance ESSP problem consists in deciding whether there is a
τ -region R of A that solves α. Notice that the polynomial-time procedures for
τ -synthesis which have been presented in Section 3 base on the fact that the
single-instance problem is solvable in polynomial-time for the corresponding types,
i.e, if τ ∩ {nop, swap} =
6 ∅. In this section, we show that the absence of nop does
not guarantee that the single-instance ESSP problem for Boolean τ -synthesis is
polynomial. In particular, the following theorem exhibits a nop-free Boolean type
for which the single-instance ESSP problem is intractable:
Theorem 2. Let τ = {inp, res, set, swap}, A be a TS and α be an ESSP atom of
A. Deciding if there is a τ -region R of A that solves α is NP-complete.
It is noteworthy that Theorem 2 does not imply that {inp, res, set, swap}-
synthesis is NP-complete. Nevertheless, the NP-completeness of the correspond-
ing single-instance ESSP problem gives a good reason to believe that the
{inp, res, set, swap}-synthesis problem might actually be harder than the one
for the types which lack both nop and swap.
The proof of Theorem 2 bases on a polynomial-time reduction of the following
decision problem, which has been shown to be NP-complete in [5]:
Cubic monotone one-in-three 3Sat. (CM 1-in-3 Sat)
79
Input: a Boolean formula ϕ = {ζ0 , . . . , ζm−1 } of negation-free three-clauses
ζi = {Xi0 , Xi1 , Xi2 }, where i ∈ {0, . . . , m − 1}, with set of variables V (ϕ) =
Sm−1
i=0 ζi ; every variable X ∈ V (ϕ) occurs in exactly three clauses.
Decide: whether there exists a one-in-three model M of ϕ, that is, a set M ⊆
V (ϕ) such that |M ∩ ζi | = 1 for all i ∈ {0, . . . , m − 1}.
Notice that the fact that every variable occurs in exactly three clauses and ϕ has
exactly m three-clauses (and thus 3m unnegated literals) imply that |V (ϕ)| = m.
Example 2 (CM 1-in-3 3Sat). The instance ϕ = {ζ0 , . . . , ζ5 } of CM 1-in-3 3Sat
with set of variables X = {X0 , . . . , X5 } and clauses ζ0 = {X0 , X1 , X2 }, ζ1 =
{X0 , X2 , X3 }, ζ2 = {X0 , X1 , X3 }, ζ3 = {X2 , X4 , X5 }, ζ4 = {X1 , X4 , X5 } and
ζ5 = {X3 , X4 , X5 } has the one-in-three model M = {X0 , X4 }.
In the remainder of this section, unless stated explicitly otherwise, we let
ϕ = {ζ0 , . . . , ζm−1 } be an arbitrary but fixed input of CM 1-in-3 3Sat, where
ζi = {Xi0 , Xi1 , Xi2 } for all i ∈ {0, . . . , m − 1} such that, moreover, m is
even. This is possible without loss of generality, which can be seen as fol-
lows: If m is odd and V (ϕ) = {X0 , . . . , Xm−1 }, then we get an equivalent
instance ϕ0 = {ζ0 , . . . , ζm−1 } ∪ {ζ00 , . . . , ζm−1
0
} with set of variables V (ϕ0 ) =
{X0 , . . . , Xm−1 } ∪ {X0 , . . . , Xm−1 }, where any Xi0 is new and corresponds one-
0 0
to-one to Xi . Moreover, ζi0 contains Xj0 if and only if ζi contains Xj . Clearly, ϕ
is a yes-instance if and only if ϕ0 is a yes-instance and, moreover, |V (ϕ0 )| = 2m.
Our Reduction. We reduce a given ϕ to a pair (A, α) of TS A and ESSP
atom α such that ϕ has a one-in-three model if and only if there is a τ -region of
A that solves α.
Notice that our current approach extends earlier methods that we applied
to prove NP-completeness of τ -synthesis for many nop-equipped types [8–11].
However, our previous reductions crucially rely on the presence of nop and are
thus useless for the current types.
Essentially, the resulting TS A can be seen as a composition of several
(independent) TS, which we also call gadgets, since any of them is applied for a
certain functionality. For a start, the TS A has the following gadgets H (top)
and G (bottom) that provide the ESSP-atom α = (k, g24m+6 ) (ignore the gray
colored area for now):
u0 v0 w0 u8m+1 v8m+1 w8m+1 k
h0 h1 h2 h3 . . . h24m+3 h24m+4 h24m+5 h24m+6 h
k u0 v0 w0 u8m+1 v8m+1 w8m+1
g g0 g1 g2 g3 . . . g24m+3 g24m+4 g24m+5 g24m+6
Notice that the sequence u0 v0 w0 u1 v1 w1 . . . u8m v8m w8m u8m+1 v8m+1 w8m+1 has
24m + 6 events and precedes and succeeds the single occurrence of k in H and
G, respectively.
Secondly, the TS A has, for every i ∈ {0, . . . , m − 1}, the following four
gadgets Ti,0 (top) and Ti,1 , Ti,2 , Ti,3 (bottom, from left to right) that apply the
variables Xi0 , Xi1 , Xi2 of the clause ζi = {Xi0 , Xi1 , Xi2 } as events:
80
k v8i Xi0 v8i+1 Xi1 v8i+2 Xi2
ti,0,0 ti,0,1 ti,0,2 ti,0,3 ti,0,4 ti,0,5 ti,0,6 ti,0,7
v8i+3
ti,0,10 ti,0,9 ti,0,8
k v8i+4
Xi0 Xi0 Xi1
y6i ti,1,1 ti,1,2 y6i+2 ti,2,1 ti,2,2 y6i+4 ti,3,1 ti,3,2
ti,1,0 v8i+5 ti,2,0 v8i+6 ti,3,0 v8i+7
y6i+1 ti,1,3 ti,1,4 y6i+3 ti,2,3 ti,2,4 y6i+5 ti,3,3 ti,3,4
Xi1 Xi2 Xi2
Finally, to connect the introduced gadgets T0,0 , . . . , Tm−1,3 , H and G, the TS
A has for all j ∈ {0, . . . , 4m}, the edge ⊥j ⊕j ⊥j+1 ; for all i ∈ {0, . . . , m − 1}
and all j ∈ {0, . . . , 3}, the edge ⊥4i+j 4i+j
ti,j,0 ; and the edges ⊥4m 4m
h0 and
⊥4m+1 4m+1
g. Eventually, A can be sketched as follows:
⊕0 ⊕1 ⊕2 ⊕4m−4 ⊕4m−3 ⊕4m−2 ⊕4m−1 ⊕4m
⊥0 ⊥1 ⊥2 ⊥3 ... ⊥4m−4 ⊥4m−3 ⊥4m−2 ⊥4m−1 ⊥4m ⊥4m+1
0 1 2 3 4m−4 4m−3 4m−2 4m−1 4m 4m+1
T0,0 T0,1 T0,2 T0,3 ... Tm−1,0 Tm−1,1 Tm−1,2 Tm−1,3 H G
Having just introduced the gadgets of A, we proceed by providing their
functionality. To do so, we need the statement of the following lemma:
Lemma 13. Let τ be a Boolean type of nets such that nop 6∈ τ , and let A be a
TS and P0 = s0 e1 . . . em sm and P1 = q0 e1 . . . em qm be two distinct acyclic
directed paths of A that both apply the same sequence e1 . . . em of events. If R =
(sup, sig) is a τ -region of A such that sup(sm ) 6= sup(qm ), then sig(ei ) = swap
for all i ∈ {1, . . . , m}.
Proof. By definition of τ , if sup(sm ) 6= sup(qm ), then, by em sm and em qm , we
get sig(em ) = swap. Clearly, by sup(sm ) 6= sup(qm ), this implies sup(sm−1 ) 6=
sup(qm−1 ). Thus, the claim follows easily by induction on m.
Let τ be a type of nets in correspondence to Theorem 2. The gadget G
provides the ESSP atom α = (k, g24m+6 ) and the events v0 , . . . , v8m+1 . While
the events k and v0 , . . . , v8m−1 occur also outside of H and G, the other events
of these gadgets do not. The aim of H and G is to ensure that any τ -region
R = (sup, sig) that solves α, which immediately implies sig(k) = inp, satisfies
sig(vj ) = swap for all j ∈ {0, . . . , 8m − 1}. We prove that H and G fulfill this
functionality: Since R solves α, we have sig(k) = inp and sup(h24m+6 ) = 1 and
sup(g24m+6 ) = 0. By Lemma 13, this implies sig(uj ) = sig(vj ) = sig(wj ) = swap
for all j ∈ {0, . . . , 8m + 1}.
In what follows, we introduce the functionality of the remaining gadgets
T0,0 , . . . , Tm−1,3 and particularly argue that R reveals a one-in-three model of ϕ.
81
Let i ∈ {0, . . . , m − 1} be arbitrary but fixed. The intuition behind Ti,0 , . . . , Ti,3 is
to ensure that there is exactly one variable event X ∈ {Xi,0 , Xi,1 , Xi,2 } such that
sig(X) = set. Since i was arbitrary, the set M = {X ∈ V (ϕ) | sig(X) = set} then
selects exactly one variable per clause ζi for all i ∈ {0, . . . , m − 1}. Consequently,
M defines a one-in-three model of ϕ.
In what follows, we formally prove the announced functionality of Ti,0 , . . . , Ti,3 .
Let Pi = ti,0,1 v8i . . . v8i+4 ti,0,9 and, let PiR be the image of Pi under R in τ ,
sig(v ) sig(v )
that is, PiR = sup(ti,0,1 ) 8i
... 8i+4
sup(ti,0,9 ). Since sig(k) = inp, we
have sup(ti,0,1 ) = 0 and sup(ti,0,9 ) = 1. Thus, PiR is a directed path from 0 to 1
in τ and the number of state changes between 0 and 1 on PiR is odd. Recall that
sig(v8i+j ) = swap for all j ∈ {0, . . . , 4}. Thus, v8i , . . . , v8i+4 already perform an
odd number of state changes on PiR . This implies that there is either exactly one
X ∈ {Xi,0 , Xi,1 , Xi,2 } such that s X s0 ∈ Pi and sup(s) = sup(s0 ), or for all X ∈
{Xi,0 , Xi,1 , Xi,2 } holds that if s X s0 ∈ Pi , then sup(s) = sup(s0 ). (Otherwise we
would have an even number of state changes on PiR , which is a contradiction.) In
what follows, we argue that the former case is true. Assume, for a contradiction,
that sup(ti,0,2 ) = sup(ti,0,3 ) and sup(ti,0,6 ) = sup(ti,0,7 ). By sup(ti,0,1 ) = 0 and
sig(v8i ) = swap, we get sup(ti,0,2 ) = sup(ti,0,3 ) = 1. This implies sig(Xi0 ) = set.
By sup(ti,0,9 ) = 1 and sig(v8i+3 ) = sig(v8i+4 ) = swap, we get sup(ti,0,6 ) =
sup(ti,0,7 ) = 1, which implies sig(Xi2 ) = set. Moreover, by sig(Xi0 ) = set
and sig(v8i+6 ), we get sup(ti,2,2 ) = 1 and sup(ti,2,4 ) = 0, respectively. Since
i,2,4 , this contradicts sig(Xi2 ) = set. Altogether, by the former discussion,
Xi2 t
this implies that there is exactly one event X ∈ {Xi,0 , Xi,1 , Xi,2 } such that
its occurrence s X s0 ∈ Pi preserves the support, that is, sup(s) = sup(s0 ). In
the following, we argue that this implies sig(X) = set and sig(Y ) 6= set for all
Y ∈ {Xi,0 , Xi,1 , Xi,2 }\{X}. If sup(ti,0,1 ) = sup(ti,0,2 ), then, as already discussed,
we obtain sig(Xi0 ) = set. By sig(Xi0 ) = set and sig(v8i+5 ) = sig(v8i+6 ) =
swap, we get sup(ti,1,2 ) = sup(ti,2,2 ) = 1 and sup(ti,1,4 ) = sup(ti,2,4 ) = 0,
respectively. Clearly, by Xi ti,1,4 and Xi ti,2,4 , this yields sig(Xi1 ) 6= set and
1 2
sig(Xi2 ) 6= set, respectively. Similarly, the assumption sup(ti,0,4 ) = sup(ti,0,5 )
yields sig(Xi1 ) = set and sig(Xi0 ), sig(Xi2 ) 6= set, and sup(ti,0,6 ) = sup(ti,0,7 )
leads to sig(Xi2 ) = set and sig(Xi0 ), sig(Xi1 ) 6= set.
Thus if R = (sup, sig) is a τ -region that solves α and satisfies sig(k) = inp,
then M = {X ∈ V (ϕ) | sig(X) = set} is a one-in-three model of ϕ.
To complete the proof of Theorem 2, it remains to argue that if M has a
one-in-three model, then α is τ -solvable. This is the content of the following
paragraph.
A One-in-three Model M of ϕ Implies the τ -Solvability of A.
Let τ = {inp, res, set, swap}. We argue that α is τ -solvable by presenting a
solving region R = (sup, sig). Due to space restrictions, we define R implicitly,
that is, we explicitly define sup(⊥0 ) and sig(e) for all e ∈ E(A). By construction,
any state sn ∈ S(A) is reachable via an unique path ⊥0 e1 . . . en sn of A.
82
Thus, sup(sn ) can be computed inductively by sup(si ) = δτ (sup(si−1 ), ei ) for all
i ∈ {1, . . . , n}.
For abbreviation, we define Y = {y0 , . . . , y6m−1 }, ⊕ = {⊕0 , . . . , ⊕4m−1 },
= { 0 , . . . , 4m+1 } , U = {u0 , . . . , v8m+1 }, V = {v0 , . . . , v8m+1 } and W =
{w0 , . . . , w8m+1 } and U V W = U ∪ V ∪ W .
Let M be a one-in-three model of ϕ. The following τ -region R = (sup, sig)
solves (k, g24m+6 ): sup(⊥0 ) = 0; for all e ∈ ⊕, we define sig(e) = res, which yields
sup(⊥0 ) = · · · = sup(⊥4m+1 ) = 0. Moreover, for all e ∈ { 4i | i ∈ {0, . . . , m}} ∪
{ 4m+1 }, we let sig(e) = swap, which ensures sup(ti,0,0 ) = sup(h0 ) = sup(g) = 1
for all i ∈ {0, . . . , m − 1}. Furthermore, for all e ∈ \ { 4i | i ∈ {0, . . . , m}},
we define sig(e) = res, which yields sup(ti,1,0 ) = · · · = sup(ti,3,0 ) = 0 for
all i ∈ {0, . . . , m − 1}. Additionally, for all e ∈ U V W ∪ (V (ϕ) \ M ), we let
sig(e) = swap, and, for all e ∈ M , we define sig(e) = set. Finally, for all
i ∈ {0, . . . , m − 1} and all e ∈ {y6i , . . . , y6i+5 }, if e = y6i+5 and Xi0 ∈ M , then
sig(e) = res; if e = y6i+3 and Xi1 ∈ M , then sig(e) = res; if e = y6i+1 and
Xi2 ∈ M , then sig(e) = res; otherwise, sig(e) = swap. The colored areas of
the gadgets H, G and Ti,0 , . . . , Ti,3 as introduced in the latter section sketches
R where Xi0 ∈ M ; grey colored states are mapped to 1 and the others to 0.
Moreover, the following figures sketch the cases Xi1 ∈ M and Xi2 ∈ M (in the
given order):
k v8i Xi0 v8i+1 Xi1 v8i+2 Xi2
ti,0,0 ti,0,1 ti,0,2 ti,0,3 ti,0,4 ti,0,5 ti,0,6 ti,0,7
v8i+3
ti,0,10 ti,0,9 ti,0,8
k v8i+4
Xi0 Xi0 Xi1
y6i ti,1,1 ti,1,2 y6i+2 ti,2,1 ti,2,2 y6i+4 ti,3,1 ti,3,2
ti,1,0 v8i+5 ti,2,0 v8i+6 ti,3,0 v8i+7
y6i+1 ti,1,3 ti,1,4 y6i+3 ti,2,3 ti,2,4 y6i+5 ti,3,3 ti,3,4
Xi1 Xi2 Xi2
k v8i Xi0 v8i+1 Xi1 v8i+2 Xi2
ti,0,0 ti,0,1 ti,0,2 ti,0,3 ti,0,4 ti,0,5 ti,0,6 ti,0,7
v8i+3
ti,0,10 ti,0,9 ti,0,8
k v8i+4
Xi0 Xi0 Xi1
y6i ti,1,1 ti,1,2 y6i+2 ti,2,1 ti,2,2 y6i+4 ti,3,1 ti,3,2
ti,1,0 v8i+5 ti,2,0 v8i+6 ti,3,0 v8i+7
y6i+1 ti,1,3 ti,1,4 y6i+3 ti,2,3 ti,2,4 y6i+5 ti,3,3 ti,3,4
Xi1 Xi2 Xi2
83
5 Conclusion
In this paper, we completely characterize the computational complexity of Boolean
τ -synthesis for types τ that contain neither nop nor swap and show that all these
types allow for a polynomial time synthesis procedure. Moreover, we give a
first hint that the absence of nop might not guarantee that Boolean synthesis
is polynomial. To do so, we show that the single instance ESSP problem is
NP-complete if τ = {inp, res, set, swap}. It remains future work to characterize
the computational complexity of τ -synthesis for the remaining nop-free Boolean
types τ .
References
1. Badouel, E., Bernardinello, L., Darondeau, P.: Petri Net Synthesis. Texts
in Theoretical Computer Science. An EATCS Series, Springer (2015).
https://doi.org/10.1007/978-3-662-47967-4
2. Badouel, E., Darondeau, P.: Trace nets and process automata. Acta
Inf. 32(7), 647–679 (1995). https://doi.org/10.1007/BF01186645,
https://doi.org/10.1007/BF01186645
3. Kleijn, J., Koutny, M., Pietkiewicz-Koutny, M., Rozenberg, G.: Step semantics of
boolean nets. Acta Inf. 50(1), 15–39 (2013). https://doi.org/10.1007/s00236-012-
0170-2, https://doi.org/10.1007/s00236-012-0170-2
4. Montanari, U., Rossi, F.: Contextual nets. Acta Inf. 32(6), 545–596 (1995).
https://doi.org/10.1007/BF01178907, https://doi.org/10.1007/BF01178907
5. Moore, C., Robson, J.M.: Hard tiling problems with simple tiles. Discrete &
Computational Geometry 26(4), 573–590 (2001). https://doi.org/10.1007/s00454-
001-0047-6
6. Pietkiewicz-Koutny, M.: Transition systems of elementary net systems with inhibitor
arcs. In: Azéma, P., Balbo, G. (eds.) Application and Theory of Petri Nets 1997,
18th International Conference, ICATPN ’97, Toulouse, France, June 23-27, 1997,
Proceedings. Lecture Notes in Computer Science, vol. 1248, pp. 310–327. Springer
(1997). https://doi.org/10.1007/3-540-63139-9 43, https://doi.org/10.1007/3-540-
63139-9 43
7. Schmitt, V.: Flip-flop nets. In: STACS. Lecture Notes in Computer Science, vol. 1046,
pp. 517–528. Springer (1996). https://doi.org/10.1007/3-540-60922-9 42
8. Tredup, R.: The complexity of synthesizing nop-equipped boolean nets from g-
bounded inputs (technical report) (2019), invited to ToPNoC 2020
9. Tredup, R.: Tracking down the bad guys: Reset and set make feasibility for flip-
flop net derivatives np-complete. In: ICE. EPTCS, vol. 304, pp. 20–37 (2019).
https://doi.org/10.4204/EPTCS.304.2
10. Tredup, R., Rosenke, C.: The complexity of synthesis for 43 boolean petri net types.
In: Theory and Applications of Models of Computation. Theoretical Computer
Science and General Issues, vol. 11436. Springer International Publishing (2019).
https://doi.org/10.1007/978-3-030-14812-6
11. Tredup, R., Rosenke, C.: On the hardness of synthesizing boolean nets. In:
ATAED@Petri Nets/ACSD. CEUR Workshop Proceedings, vol. 2371, pp. 71–86.
CEUR-WS.org (2019)
84