Introduction

Boolean Petri nets have been widely regarded as a fundamental model for concurrent systems. These Petri nets allow at most one token per place in every reachable marking. Accordingly, a place p can be regarded as a boolean condition which is true if p contains a token and is false if p is empty, respectively. A place p and a transition t of a boolean Petri net are connected by one of the following (boolean) interactions: no operation (nop), input (inp), output (out), set, reset (res), inverting (swap), test if true (used), and test if false (free). An interaction defines which pre-condition p has to satisfy to activate t and it determines p's post-condition after t has fired: inp (out) mean that p has to be true (false) to allow t's firing and if t fires then p become false (true). The interaction free (used) says that if t is activated then p is false (true) and t's firing as no impact on p. The other interactions nop, set, res, swap are pre-condition free, that is, neither true nor false prevent t's firing. Moreover, nop means that the firing of t has no impact and leaves p's boolean value unchanged. By res (set), t's firing determine p to be false (true). Finally, swap says that if t fires then it inverts p's boolean value.

Boolean Petri nets are differentiated by types of nets τ accordingly to the boolean interactions they allow. Since we have eight interactions to choose from, this results in a total of 256 different types. Yet, research has explicitly defined seven of them: Elementary net systems {nop, inp, out} [10], Contextual nets {nop, inp, out, used, free} [7], event/condition nets {nop, inp, out, used} [2], inhibitor nets {nop, inp, out, free} [9], set nets {nop, inp, set, used} [6], trace nets {nop, inp, out, set, res, used, free} [3], and flip flop nets {nop, inp, out, swap} [11]. Results of [14] reestablishing the result for flip flop nets [11]. Green colored area: Results of this paper. The last two rows intersect in eight supersets of {nop, inp, out, set, res} and the eighth row includes the already investigated elementary net systems [1]. Altogether, this paper discovers 67 new types with an NP-hard synthesis problem.

This paper is devoted to a computational complexity analysis of the boolean net synthesis problem subject to a target type of nets. Synthesis relative to a specific type of nets τ is the challenge to find for a given transition system (TSs, for short) A, a boolean τ -net N whose state graph is isomorphic to A if it exists. The complexity of boolean net synthesis has originally been investigated for elementary net systems [1], where it is NP-complete to decide if general TSs can be synthesized. In [15,12] this has been confirmed even for strongly restricted input TSs. On the contrary, [11] shows for flip flop nets, simply extending elementary net systems by swap, synthesis is doable in polynomial time. Inspired by these results, it is the (global) goal of our research to obtain a dichotomy result that fully characterizes which synergies of interactions make synthesis intractable or tractable, respectively. After resolving the complexity of synthesis for elementary nets [1,15,12] and flip flop nets [11], the next big step towards a complete characterization of boolean net synthesis is taken in [14]. Here, besides the already investigated flip flop nets, 42 further boolean types of nets are covered at one blow, cf. Figure 1. Besides the 128 practically less relevant types without nop, there are 84 nop-afflicted boolean types of nets left where the synthesis' complexity has not been settled, yet.

In this paper, we tackle 67 of them with a common NP-hardness proof scheme and, additionally, reestablish the result for elementary net systems [1]. Except flip flop nets, our result covers all types of nets previously considered in the literature. In particular, we show that synthesis is hard for all types that are a superset of {nop, inp, out} that excludes swap and for all supersets of {nop, inp, set} and {nop, out, res}, cf. Figure 1.

Aside from the actual identification of 67 new types with hard net synthesis, this paper's contribution is also a very generic reduction scheme for NP-hardness proofs of boolean net synthesis. This methodology significantly generalizes preliminary methods that we developed in [15,12] to derive the hardness of synthesizing elementary net systems from strongly restricted TSs. Unlike those premature approaches, the present solution abstracts from individual types of nets and bases on the throughout analysis of properties gained by available interactions. Moreover, the approach from [14], although again slightly similar, is incompatible with the generic scheme in this paper.

To develop the generic reduction scheme, we deal with the synthesis problem's decision version, called feasibility. The reason is that complexity analysis rather works with decision problems than search problems. Instead of really finding a net N with state graph isomorphic to a given TS, it is sufficient for feasibility to just decide if the target type contains N . If feasibility is NP-complete, then synthesis is an NP-hard computational problem with no obvious efficient solutions.

To simplify our argumentation is it meaningful to detach our notions from Petri nets and focus on TSs. For this purpose, we use the well known equality between feasibility and the conjunction of the state separation property (SSP) and the event state separation property (ESSP) [2], which are solely defined on the input TSs. The presented polynomial time reduction scheme translates the NP-complete cubic monotone one-in-three 3-SAT problem [8] into the ESSP of the considered 68 boolean net types. As we also make sure that given boolean expressions ϕ are transformed to TSs A(ϕ) where the ESSP relative to the considered type implies the SSP, we always show the NP-completeness of the ESSP and feasibility at the same time. Instead of 68 individual proofs, our scheme covers all cases by just three reductions following a common pattern.

Due to space limitation, we are not able to present all proofs. However, all omitted proofs are given in the technical report [13].

Preliminary Notions

This section provides short formal definitions of all preliminary notions used in the paper. A transition system (TS, for short), A = (S, E, δ) is a directed labeled graph with nodes S, events E and partial transition function δ : S × E −→ S, where δ(s, e) = s is interpreted as s e s . An event e occurs at a state s, denoted by s e , if δ(s, e) is defined. An initialized TS A = (S, E, δ, s 0 ) is a TS with a distinct state s 0 ∈ S. TSs in this paper are deterministic by design as their state transition behavior is given by a (partial) function. Initialized TSs are also required to make every state reachable from s 0 by a directed path.

x nop(x) inp(x) out(x) set(x) res(x) swap(x) used(x) free(x) 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}. The interactions i ∈ I are binary partial functions i : {0, 1} → {0, 1} as defined in the listing of Figure 2. For all x ∈ {0, 1} and all i ∈ E τ the transition function of τ is defined by δ τ (x, i) = i(x). Notice that I contains all possible binary partial functions {0, 1} → {0, 1} except for the entirely undefined function ⊥. Even if a type τ includes ⊥, this event can never occur, so it would be useless. Thus, I is complete for deterministic boolean types of nets, and that means there are a total of 256 of them. By definition, a (boolean) type τ is completely determined by its event set E τ . Hence, in the following we will identify τ with E τ , cf. Figure 3. Moreover, for readability, we group interactions by enter = {out, set, swap}, exit = {inp, res, swap}, keep + = {nop, set, used}, and keep − = {nop, res, free}.

0 0 1 1 0 1 0 1 1 0 1 0 0 1φ(i) = i for i ∈ {nop, swap}, φ(out) = inp, φ(res) = set and φ(free) = used.

A boolean Petri net N = (P, T, M 0 , f ) of type τ , (τ -net, for short) is given by finite and disjoint sets P of places and T of transitions, an initial marking M 0 : P −→ {0, 1}, and a (total) flow function f : P × T → τ . The meaning of a boolean net is to realize a certain behavior by firing sequences of transitions. In particular, 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 next marking M : P −→ {0, 1} where M (p) = δ τ (M (p), f (p, t)) for all p ∈ P . This is denoted by M t M . Given a τ -net N = (P, T, M 0 , f ), its behavior is captured by a transition system A(N ), called the state graph of N . The state set of A(N ) consists of all markings that, starting from initial state M 0 , can be reached by firing a sequence of transitions. For every reachable marking M and transition t ∈ T with M t M the state transition function δ of A is defined as δ(M, t) = M .

Boolean net synthesis for a type τ is going backwards from input TS A = (S, E, δ, s 0 ) to the computation of a τ -net N with A(N ) isomorphic to A, if such a net exists. In contrast to A(N ), the abstract states S of A miss any information about markings they stand for. Accordingly, the events E are an abstraction of N 's transitions T as they relate to state changes only globally without giving the information about the local changes to places. After all, the transition function δ : S × E → S still tells us how states are affected by events.

To prove net synthesis of τ -nets NP-hard, we show the NP-completeness of the corresponding decision version: τ -feasibility is the problem to decide the existence of a τ -net N with A(N ) isomorphic to the given TS A. To describe feasibility without referencing the searched τ -net N , in the sequel, we introduce the τ -state separation property (τ -SSP, for short) and the τ -event state separation property (τ -ESSP, for short) for TSs. In conjunction, they are equivalent to τ -feasibility. The following notion of τ -regions allows us to define the announced properties.

A τ -region of a given A = (S, E, δ, s 0 ) is a pair (sup, sig) of support sup : S → S τ = {0, 1} and signature sig : E → E τ = τ where every transition s e s of A leads to a transition sup(s) sig(e) sup(s ) of τ . While a region divides S into the two sets

sup −1 (b) = {s ∈ S | sup(s) = b} for b ∈ {0, 1}, the events are cumulated by sig −1 (i) = {e ∈ E | sig(e) = i} for all available interactions i ∈ τ . We also use sig −1 (τ ) = {e ∈ E | sig(e) ∈ τ } for τ ⊆ τ .

For a TS A = (S, E, δ, s 0 ) and a type of nets τ , a pair of states s = s ∈ S is τseparable if there is a τ -region (sup, sig) such that sup(s) = sup(s ). Accordingly, A has the τ -SSP if all pairs of distinct states from A are τ -separable. Secondly, an event e ∈ E is called τ -inhibitable at a state s ∈ S if there is a τ -region (sup, sig) where sup(s) sig(e) does not hold, that is, the interaction sig(e) ∈ τ is not defined on input sup(s) ∈ {0, 1}. A has the τ -ESSP if for all states s ∈ S it is true that all events e ∈ E that do not occur at s, meaning ¬s e , are τ -inhibitable at s. It is well known from [2] that a TS A is τ -feasible, that is, there exists a τ -net N with A(N ) isomorphic to A, if and only if A has τ -SSP and the τ -ESSP. Types of nets τ and τ have an isomorphism φ if s i s is a transition in τ if and only if φ(s) φ(i) φ(s ) is one in TS τ . By the following lemma, we benefit from the eight isomorphisms that map nop to nop, swap to swap, inp to out, set to res, used to free, and vice versa:

Lemma 1 (Without proof). If τ and τ are isomorphic types of nets then a TS A has the (E)SSP for τ if and only if A has the (E)SSP for τ .

Main Result

Theorem 1 (Main result). Let τ1 = {nop, inp, out}, τ 2 = {nop, inp, res, swap}, τ2 = {nop, out, set, swap}, τ 3 = {nop, inp, set} and τ3 = {nop, out, res}. If τ = τ ∪ ω for τ ∈ {τ 1 , τ 2 , τ2 } with ω ⊆ {used, free} or τ ⊇ τ 3 or τ ⊇ τ3 then τ -feasibility is NP-complete.

In total, Theorem 1 covers 68 types, cf. Figure 1, including the elementary net systems [1]. It is straight forward that τ -feasibility is a member of NP for all considered type of nets τ : By definition, there are at most |S| 2 pairs of states (s, s ) to separate and at most |E| • |S| pairs (e, s) of event and state where e has to be inhibited at s. In a non-deterministic computation, one can simply guess and check in polynomial time for all pairs the region that separates s and s , respectively inhibits e at s, or reject the input if such a region does not exist. Hence, for the proof of Theorem 1 it remains to prove τ -feasibility to be NP-hard for all types of nets. Although this demands for 68 NP-hardness proofs, we manage to reduce it to three. Every reduction bases on one scheme using the cubic monotone one-in-three-3-SAT problem, (P1, for short), which has been shown to be NP-hard in [8]:

cubic monotone one-in-three-3-sat (P1) Instance: negation-free boolean expression ϕ = {ζ 0 , . . . , ζ m−1 } of three-clauses ζ 0 , . . . , ζ m−1 with variable set V (ϕ), every variable occurs in exactly three clauses Question: Is there a subset M ⊆ V (ϕ) such that |M ∩ ζ i | = 1 for i ∈ {0, . . . , m − 1}? Starting from a common construction principle, we choose one of our three reductions by a turn-switch σ. In every switch position σ 1 , σ 2 , σ 3 , the chosen reduction works for multiple boolean types based on mutually shared interactions and isomorphisms. Before we set out the details, the following subsection introduces our way of easily combining gadget TSs for our NP-completeness proofs.

Unions of Transition SystemsIf A 0 = (S 0 , E 0 , δ 0 , s 0 0 ), . . . , A n = (S n , E n , δ n , s n 0 ) are (initialized)

TSs with pairwise disjoint states (but not necessarily disjoint events) we say that U (A 0 , . . . , A n ) is their union. By S(U ), we denote the entirety of all states in A 0 , . . . , A n and E(U ) summarizes all events. For a flexible formalism, we allow to build unions recursively: Firstly, we allow empty unions and identify every TS A with the union containing only A, that is,

A = U (A). Next, if U 1 = U (A 1 0 , . . . , A 1 n1 ), . . . , U m = (A m 0 , . . . , A n nm ) are unions (possibly with U i = U () or U i = A i ) then U (U 1 , . . . , U m ) is the union U (A 1 0 , . . . , A 1 n1 , .

. . , A m 0 , . . . , A n nm ). We lift the concepts of regions, SSP, and ESSP to unions U = U (A 0 , . . . , A n ) as follows: A τ -region (sup, sig) of U consists of sup : S(U ) → S τ and sig : E(U ) → E τ such that, for all i ∈ {0, . . . , n}, the projections sup i (s) = sup(s), s ∈ S i and sig i (e) = sig(e), e ∈ E i provide a region (sup i , sig i ) of A i . U has the τ -SSP if for all different states s, s ∈ S(U ) of the same TS A i there is a τ -region (sup, sig) of U with sup(s) = sup(s ). Moreover, U has the τ -ESSP if for all events e ∈ E(U ) and all states s ∈ S(U ) with ¬s e there is a τ -region (sup, sig) of U such that ¬sup(s) sig (e) . Naturally, U is called τ -feasible if it has the τ -SSP and τ -ESSP. To merge a union U = U (A 0 , . . . , A n ) into a single TS, we define the joining A(U ): If s 0 0 , . . . , s n 0 are the initial states of U 's TSs then

A(U ) = (S(U ) ∪ ⊥, E(U ) ∪ ∪ , δ, ⊥ 0

) is a TS with additional connector states ⊥ = {⊥ 0 , . . . , ⊥ n } and fresh events = { 0 , . . . , n }, = { 1 , . . . , n } joining the individual TSs of U by δ as defined in Figure 4. Hence, A(U ) puts the connector states into a chain of the events from and links the initial states of TSs from U to this chain using events from . The following lemma certifies the validity of the joining operation for the unions and the types of nets that occur in our reduction scheme. Lemma 2. Let τ be a type of nets such that nop, inp ∈ τ and τ ∩ enter = ∅. If U = U (A 0 , . . . , A n ) is a union of TSs A 0 , . . . , A n where, for every event e in E(U ), there is at least one state s in S(U ) with ¬s e then U has the τ -(E)SSP if and only if A(U ) has the τ -(E)SSP.

δ(s, e) =    s i 0 , if s = ⊥i and e = i,

Notice that Lemma 2 does not cover all types mentioned in Theorem 1. However, this is not necessary as every type τ from Theorem 1 missed by Lemma 2 is indirectly covered in the Lemma by an isomorphic type τ .

The General Reduction Scheme

Our general scheme can be set up to a specific reduction by the turn switch σ. In each of its three positions, σ covers a whole collection of net types. Therefore, we simply understand the positions σ 1 , σ 2 , σ 3 as the type sets managed by the respective reductions:

σ 1 = {τ 1 ∪ ω | ω ⊆ {used, free}} ∪ {τ 3 ∪ ω | ω ⊆ {out, res, used, free} σ 2 = {τ 3 ∪ {swap} ∪ ω | ω ⊆ {out, res, used, free}} σ 3 = {τ 2 ∪ ω | ω ⊆ {used, free}}

The input of our scheme is the switch position σ ∈ {σ 1 , σ 2 , σ 3 } and an instance ϕ of P1. The result is a union U σ ϕ of gadget TSs satisfying the conditions of Lemma 2, that is, U σ ϕ is τ -feasible if and only if A(U σ ϕ ) is τ -feasible for all τ ∈ σ. Moreover, the union U σ ϕ satisfies the following properties:

1. The variables V (ϕ) are a subset of E(U σ ϕ ), the union events. 2. Event k ∈ E(U σ ϕ ) is to inhibit at state h 0,6 ∈ S(U σ ϕ ) and there are events A polynomial time reduction scheme with these properties proves Theorem 1 as the following implications are justified:

V = {v 0 , . . . , v 3m−1 } ⊆ E(U σ ϕ ) and W = {w 0 , . . . , w 3m−1 } ⊆ E(U σ ϕ ). 3. If τ ∈ σϕ is one-in-three satisfiable 5. =⇒ k is τ -inhibitable at h 0,6 in U σ ϕ 6. =⇒ U σ ϕ has the τ -ESSP & τ -SSP def. =⇒ U σ ϕ is τ -feasible def. =⇒ U σ ϕ has the τ -ESSP def. =⇒ k is τ -inhibitable at h 0,6 in U σ ϕ 3./4.

=⇒ ϕ is one-in-three satisfiable.

Especially, ϕ is one-in-three satisfiable if and only if U σ ϕ is τ -feasible. By Lemma 2, this proves NP-hardness of τ -feasibility for all τ in the positions σ 1 , σ 2 , σ 3 . Secondly, every remaining type τ of Theorem 1 is isomorphic to one of the already covered cases τ . Hence, by Lemma 1, this also proves NP-hardness of τ -feasibility which, by feasibility being in NP, justifies Theorem 1.

In the sequel, we develop the reduction of U σ ϕ and show that it satisfies Condition 1-Condition 5. Notice that this proves ϕ is one-in-three satisfiable if and only if k is inhibitable at h 0,6 . Due to space limitation, the proof that U σ ϕ also has Condition 6 is moved to the technical report [13].

Details for Condition 2 and Condition 3

To satisfy Condition 2, every union U σ ϕ implements the following transition system H that provides the event k, the state h 0,6 , where ¬h 0,6 k , and the events of Z = {z 0 , . . . , z 3m−1 }, V = {v 0 , . . . , v 3m−1 } and W = {w 0 , . . . , w 3m−1 } (the colored areas are to be explained later):

h 0,0 h 0,1 h 0,2 h 0,3 h 0,4 h 0,5 h 0,6 h 3m−1,0 h 3m−1,1 h 3m−1,2 h 3m−1,3 h 3m−1,4 h 3m−1,5 h 3m−1,6 h 3m,0 h 3m,1 h 3m,2 h 3m,3 h 3m,4 h 3m,5 h 3m,6 h 6m−1,0 h 6m−1,1 h 6m−1,2 h 6m−1,3 h 6m−1,4 h 6m−1,5 h 6m−1,6 . . . . . . r 0 r 3m−2 r 3m−1 . . . . . . r 3m r 6m−2 k z 0 v 0 k q 0 z 0 k z 3m−1 v 3m−1 k q 3m−1 z 3m−1 k w 0 p 0 k y 0 w 0 k w 3m−1 p 3m−1 k y 3m−1 w 3m−1 c 0 c 3m−2 c 3m−1 c 3m c 6m−2

So far Condition 2 is already satisfied. For Condition 3 we observe that, by definition, there are basically four interactions possibly useful for sig(k): inp, out, used, free. The other interactions res, set, swap, nop are defined on both 0 and 1 and, hence, not suitable to inhibit events. H alone generally does not guarantee that a region (sup, sig) inhibiting k at h 0,6 satisfies Condition 3. Thus, to achieve this goal other gadgets are necessary. By theirs different types (having different interactions), it depends on σ which gadgets are necessary. We proceed step by step and develop the construction for σ 1 , σ 2 and σ 3 in the given order. In the sequel, if not explicitly stated otherwise, by (sup, sig) we refer to a τ -region of U σ ϕ , τ ∈ σ, that inhibits k at h 0,6 . The union U σ1 ϕ implements additionally the following two TSs F 0 , F 1 :

F 0 = f 0,0 f 0,1 f 0,2 f 0,3 f 0,4 k n 0 z 0 k F 1 = f 1,0 f 1,1 f 1,2 q 0 k

We argue that every region (sup, sig) of U σ1 ϕ satisfies Condition 3: If sig(k) = used then, by definition of used we get sup(s) = sup(s ) = 1 for every transition s k s . Hence, we have sup(f 0,3 ) = sup(f 1,1 ) = sup(h 0,4 ) = 1. By definition of inp, res we have that e s and sig(e) ∈ {inp, res} implies sup(s) = 0. Hence, by z 0 f 0,3 and q 0 f 1,1 we have that sig(z 0 ), sig(q 0 ) ∈ {inp, res}. Moreover, we observe that swap ∈ τ for all τ ∈ σ 1 . Thus, sig(z 0 ), sig(q 0 ) ∈ keep + such that sup(h 0,4 ) = sup(h 0,5 ) = sup(h 0,6 ) = 1 which contradicts ¬sup(h 0,6 ) sig(k) . Hence, sig(k) = used. Similarly, one argues that sig(k) = free implies that sup(h 0,6 ) = 0, again a contradiction. Hence, we have that sig(k) = inp and sup(h 0,6 ) = 0 or sig(k) = out and sup(h 0,6 ) = 1.

As a next step, we show that sig(k) = inp and sup(h 0,6 ) = 0 implies sig(v 0 ) ∈ enter and sig(z 0 ) ∈ keep − : By sig(k) = inp and k h 0,1 and h 0,3 k we have that sup(h 0,1 ) = 0 and sup(h 0,3 ) = 1. By z 0 h 0,6 , sup(h 0,6 ) = 0 and swap ∈ τ we have that sig(z 0 ) ∈ keep − . Moreover, by sup(h 0,1 ) = 0 and sig(z 0 ) ∈ keep − it is sup(h 0,2 ) = 0 which, by h 0,2 v 0 h 0,3 and sup(h 0,3 ) = 1, implies sig(v 0 ) ∈ enter. Notice, that this reasoning purely bases on sig(k) = inp and sup(h 0,6 ) = 0. Similarly, one argues that sig(k) = out and sup(h 0,6 ) = 1 implies sig(v 0 ) ∈ exit and sig(z 0 ) ∈ keep + . U σ1 ϕ uses for every i ∈ {0, . . . , 6m − 2} the following TS G c,c i to transfer the support-value sup(h 0,6 ) to the states h 1,6 , . . . , h 6m−1,6 :

G c,c i = g c,c i,0 g c,c i,1 g c,c i,2 g c,c i,3 c i k c i k

By doing so, it transfers the outcome of the latter observation to the events v 1 , . . . , v 3m−1 and w 0 , . . . ,

w 3m−1 : If sig(k) = inp, then we have sup(g c,c i,0 ) = sup(g c,c i,0 ) = 1 and sup(g c,c i,2 ) = sup(g c,c i,3 ) = 0, that is, sig(c i ) = nop. Symmetrically, if sig(k) = out then sig(c i ) = nop. Hence, if sig(k) = inp

and sup(h 0,6 ) = 0 then sup(h i,6 ) = 0 for all i ∈ {0, . . . , 6m − 1}. Perfectly similar to the discussion for z 0 and v 0 we obtain that V ⊆ sig −1 (enter) and W ⊆ sig −1 (keep − ), respectively. Symmetrically, sig(k) = out and sup(h 0,6 ) = 1 imply V ⊆ sig −1 (exit) and W ⊆ sig −1 (keep + ). Hence, U σ1 ϕ satisfies Condition 3. Unfortunately, if σ ∈ {σ 2 , σ 3 } then the introduced gadgets F 0 , F 1 (alone) are not powerful enough to ensure Condition 3. This is mainly due to the interaction swap. However, we tackle this problem by the application of other gadgets. While, due to theirs different interaction sets, σ 2 and σ 3 have different requirements, both of U σ2 ϕ and U σ3 ϕ implement for every i ∈ {0, . . . , 6m − 2} the gadget G c,c i and for i ∈ {0, . . . , 3m − 1} following gadget TSs G ,q i and G ,y i :

G ,q i = g ,q i,0 g ,q i,1 g ,q i,2 g ,q i,3 k q i k G ,y i = g ,y i,0 g ,y i,1 g ,y i,2 g ,y i,3 k y i k

Here and in the sequel, the purpose of underscore-labeled edges is essentially to ensure reachability of the TSs. Every underscore represents an arbitrary unique event occurring only at this edge. For the sake of readability we do not define these events explicitly. Again for readability, we define Q = {q 0 , . . . , q 3m−1 } and Y = {y 0 , . . . , y 3m−1 }. Moreover, U σ2 ϕ adds the TS F 0 (originally introduced for σ 1 ) and the next TS G n, 0 while U σ3 ϕ uses also F 0 and the following TS F 2 :

G n, 0 = g n, 0,0 g n, 0,1 g n, 0,2 g n, 0,3 n 0 k k F 2 = f 2,0 f 2,1 f 2,2 f 2,3 n 0 k k That U σ2 ϕ and U σ3 ϕ differ in G n, 0

and F 2 , respectively, is mainly due to the fact that the interactions of theirs types have different requirements to satisfy Condition 5 and Condition 6. To argue for U σ3 ϕ 's and U σ4 ϕ 's functionality, respectively, we firstly show that sig(k) ∈ {inp, out} for (sup, sig):

If sig(k) = used then s k s implies sup(s) = sup(s ) = 1. Applying this to F 2 , G n,

0 and G ,q 0 we obtain that sig(n 0 ), sig(q 0 ) ∈ keep + . By sig(n 0 ) ∈ keep + and sup(f 0,1 ) = 1 we obtain sup(f 0,2 ) = 1 which, by sup(f 0,3 ) = 1, implies sig(z 0 ) ∈ keep + . Finally, by sup(h 0,3 ) = 4 and sig(z 0 ), sig(q 0 ) ∈ keep + , we get sup(h 0,6 ) = 1 which contradicts ¬ sup(h 0,6 ) sig (k) . Similarly, the assumption sig(k) = free yields the same contradiction. Thus, sig(k) ∈ {inp, out}.

We argue that sig(k) = inp and sup(h 0,6 ) = 0 implies V ⊆ sig −1 (enter) and W ⊆ sig −1 (keep − ): By sig(k) = inp we get again sig(c i ) = nop and, thus, sup(h i,6 ) = 0 for all i in question. Moreover, by sig(k) = inp we get sup(s) = 0 for all k s. Applying this to G ,q i and G ,y i yields Q, Y ⊆ sig −1 (keep − ). By Q, Y ⊆ sig −1 (keep − ) and sup(h i,4 ) = 0 (for all i ∈ {0, . . . , 6m − 1}) we get sup(h i,5 ) = 0 which, by sup(h i,6 ) = 0, implies W, Z ⊆ sig −1 (keep − ). Finally, by Z ⊆ sig −1 (keep − ) and sup(h i,1 ) = 0 we conclude sup(h i,2 ) = 0 implying with sup(h i,3 ) = 1 that sig(v i ) ∈ enter for every i ∈ {0, . . . , 3m − 1}: V ⊆ sig −1 (enter). Symmetrically, sig(k) = out and sup(h 0,6 ) = 1 implies W ⊆ sig −1 (keep + ) and

V ⊆ sig −1 (exit). Hence, U σ2

ϕ and U σ3 ϕ satisfy Condition 3.

Details for Condition 1 and Condition 4

Essential for the realization of Condition 1 and Condition 4 is the observation that for every τ -region R = (sup, sig) and path P = s e 1 . . . e n s the image R(P ) = sup(s) sig(e 1 ) . . . sig(e n ) sup(s ) is a path in τ . Moreover, if sup(s) = sup(s ) = 0 then there has to be an event e i mapped to an interaction of τ that allows a state change in τ : sig(e i ) ∈ {nop, used, free}. Our target is to exploit this observation in the following way: Firstly, represent every clause

ζ i = {X i,0 , X i,1 , X i,2 } by a path P i,0 = t i,0,2 X i,0 t i,0,3 X i,1 t i,0,4 X i,2 t i,0,5 .

Secondly, ensure that region (sup, sig) (inhibiting k at h 0,6 ) requires sup(t i,0,2 ) = sup(t i,0,5 ) for every i ∈ {0, . . . , m−1}. Thirdly, ensure that there is exactly one variable event X ∈ {X i,0 , X i,1 , X i,2 } whose image sig(X) allows the necessary state change in τ and that both of the others are mapped to nop. Such a region implies that M = {X ∈ V (ϕ) | sig(X) = nop} is a one-in-three model of ϕ as two different clauses ζ i , ζ j are represented by different paths P i,0 , P j,0 . Let's discuss the case that region (sup, sig) satisfies sup(t i,0,2 ) = 1 and sup(t i,0,5 ) = 0. Unfortunately, generally there are many possibilities for the signature of the variable events X i,0 , X i,1 , X i,2 and not even one of them need to be mapped to nop. For example, sig(X) = res or sig(X) = swap for X ∈ {X i,0 , X i,1 , X i,2 } would be possible, too.

We attack this problem as follows: Firstly, instead of one path for ζ i we apply the following three forward-backward paths P i,0 , P i,1 , P i,2 which for every variable event X ∈ {X i,0 , X i,1 , X i,2 } use an additional mirror event x:

P i,0 = t i,0,2 t i,0,3 t i,0,4 t i,0,5 X i,0 X i,1 X i,2 x i,0 x i,1 x i,2 P i,1 = t i,1,2 t i,1,3 t i,1,4 t i,1,5 X i,1 X i,2 X i,0 x i,1 x i,2 x i,0 P i,2 = t i,2,2 t i,2,3 t i,2,4 t i,2,5 X i,2 X i,0 X i,1 x i,2 x i,0 x i,1

Notice that, by the arbitrariness of i, we have for every X ∈ {X 0 , . . . , X m−1 } = V (ϕ) its unique mirror event x ∈ {x 0 , . . . , x m−1 }. Moreover, by definition, if s X s is a an edge (of any forward-backward path) then s x s is too. The paths P i,0 , P i,1 , P i,2 are similar but the variable events are once and twice leftshifted, respectively. Secondly, we ensure that (sup, sig) also satisfies sup(t i,1,2 ) = sup(t i,2,2 ) = 1 and sup(t i,1,5 ) = sup(t i,2,5 ) = 0, that is, sup synchronizes the states t i,0,2 , t i,1,2 , t i,2,2 and the states t i,0,5 , t i,1,5 , t i,2,5 , respectively. As a result, we have for every variable event X ∈ {X i,0 , X i,1 , X i,2 } an edge X s such that sup(s) = 0. Consequently, we have that sig(X) ∈ {out, set, used}, as i x and i ∈ {out, set, used} requires x = 1. Moreover, we also have for every variable event an edge s X such that sup(s) = 1, such that sig(X) = free. This leaves nop, inp, res, swap as remaining candidates for sig(X).

As a matter of fact, the construction already ensures that a variable event

X ∈ {X i,0 , X i,1 , X i,2 } with sig(X) ∈ {inp, res} implies that sig(Y ) = nop for Y ∈ {X i,0 , X i,1 , X i,2 } \ {Y }.

We explicitly justify this claim only for X = X i,0 as, by symmetry, the cases X = X i,1 and X = X i,2 are quite similar: By sig(X i,0 ) ∈ {inp, res} we have sup(t i,0,3 ) = 0 which by sup(t i,0,2 ) = 1 and t i,0,2 x i,0 t i,0,3 implies sig(x i,0 ) ∈ {out, set, swap}. Again by sig(X i,0 ) ∈ {inp, res} we have sup(t i,2,4 ) = 0 implying with sig(x i,0 ) ∈ {out, set, swap} that sup(t i,2,3 ) = 1. By

t i,2,2 X i,2 t i,2,3 , sup(t i,2,2 ) = sup(t i,2,3 ) = 1 and sig(X i,2 ) ∈ {nop, inp, res, swap} we conclude sig(X i,2 ) = nop. Furthermore, by sup(t i,1,5 ) = 0 and sig(x i,0 ) ∈ {out, set, swap} we have sup(t i,1,4 ) = 1. By sig(X i,2 ) = nop, t i,1,3 X i,2 t i,1,4

and sup(t i,1,4 ) = 1 we obtain that sup(t i,1,3 ) = 1. Finally, by sup(t i,1,2 ) = 3 and sig(X i,1 ) ∈ {nop, inp, res, swap} we obtain sig(X i,1 ) = nop.

sup(t i,1,3 ) = 1, t i,1,2 X i,1 t i,1,

So far, we have already argued that for types τ with swap ∈ τ the following is true: A τ -region that synchronizes t i,0,2 , t i,1,2 , t i,2,2 and t i,0,5 , t i,1,5 , t i,2,5 as announced ensures that there is exactly one variable event of X i,0 , X i,1 , X i,2 with a signature different from nop. This concerns the types which are covered by σ 1 .

For the types τ with swap ∈ τ , covered by σ 2 and σ 3 , it remains to ensure the following:

If X ∈ {X i,0 , X i,1 , X i,2 } and sig(X) = swap then sig(Y ) = nop for Y ∈ {X i,0 , X i,1 , X i,2 } \ {X}.

Unfortunately, the previous construction (alone) can not afford this. However, we overcome this problem by another enhancement which we develop in the sequel.

Notice that, by the former discussion, sig(X) = swap already implies sig(Y ) ∈ {inp, res} for Y ∈ {X i,0 , X i,1 , X i,2 }\{X}. Hence, its simple maths that if sig(X) = swap then either all variable events are mapped to swap or exactly one of them: Either we have three changes in τ to get from 1 to 0 or exactly one. Moreover, it is easy to see that if sig(X) = swap for all X ∈ {X i,0 , X i,1 , X i,2 } then sig(x) = swap for all x ∈ {x i,0 , x i,1 , x i,2 }. Thus, it is sufficient to prevent that any x is mapped to swap. To do so, the union U σ2 ϕ installs for every mirror event x i ∈ {x 0 , . . . , x m−1 }, that is, especially for x i,0 , x i,1 , x i,2 , the gadget TS G x, i which is defined in Figure 5.4. As (sup, sig) satisfies sig(k) ∈ {inp, out} we have sup(g x, i,0 ) = sup(g x, i,1 ) which implies sig(x i ) = swap for i ∈ {0, . . . , m − 1}. Similarly, the union U σ3 ϕ installs for every i ∈ {0, . . . , m − 1} the gadget TS G ,x i which is defined in Figure 5.8. The reason for these differences between U σ2 ϕ and U σ3 ϕ is again due to theirs different types and the target to satisfy Condition 5 and Condition 6. We will give a detailed explanation later.

Altogether, we have argued that a reduction with these features ensures, that the existence of (sup, sig) implies that M = {X ∈ V (ϕ) | sig(X) = nop} is a onein-three model of ϕ. Moreover, an analogous argument shows that sup(t i,0,2 ) = sup(t i,1,2 ) = sup(t i,2,2 ) = 0 and sup(t i,0,5 ) = sup(t i,1,5 ) = sup(t i,2,5 ) = 1 also implies that exactly one variable event (per clause) has a signature different from nop. But how can we ensure that the states t i,0,2 , t i,1,2 , t i,2,2 and the states t i,0,5 , t i,1,5 , t i,2,5 become synchronized? To achieve this, we enhance P i,0 , P i,1 , P i,2 as follows: If σ ∈ {σ 1 , σ 2 } then we enhance P i,0 , P i,1 , P i,2 to T i,0 , T i,1 , T i,2 in accordance to Figure 5.1-Figure 5.3, respectively. T i,0 , T i,1 and T i,2 apply the event k and the events v 3i , v 3i+1 , v 3i+2 and w 3i , w 3i+1 , w 3i+2 . To make it clear: Besides the corresponding gadgets introduced in Section 3.3, U σ1 ϕ and U σ2 ϕ (additionally) implement the TSs T i,0 , T i,1 and T i,2 for every i ∈ {0, . . . , m − 1}. Moreover, U σ2 ϕ implements also G x, i for every i ∈ {0, . . . , m − 1}.

The region (sup, sig) uses the latest enhancement as follows: As already discussed in the former section, sig(k) = inp (and sup(h 0,6 ) = 0) imply V ⊆ sig −1 (enter) and W ⊆ sig −1 (keep − ). Moreover, by sig(K) = inp, we have sup(t i,0,1 ) = sup(t i,1,1 ) = sup(t i,2,1 ) = 0. Altogether, this implies sup(t i,0,2 ) = sup(t i,1,2 ) = sup(t i,2,2 ) = 1 and sup(t i,0,5 ) = sup(t i,1,5 ) = sup(t i,2,5 ) = 0. Moreover, if sig(k) = out then V ⊆ sig −1 (exit), implying sup(t i,0,2 ) = sup(t i,1,2 ) = sup(t i,2,2 ) = 0, and W ⊆ sig −1 (keep + ), implying sup(t i,0,5 ) = sup(t i,1,5 ) = sup(t i,2,5 ) = 1. As discussed, this implies a one-in-three model of ϕ.

For U σ3 ϕ we need a slightly different construction: The union U σ3 ϕ implements for every i ∈ {0, . . . , m − 1} instead of T i,0 , T i,1 , T i,2 the transition system T i,0 , T i,1 , T i,2 defined in Figure 5.4-Figure 5.6, respectively. T i,0 , T i,1 , T i,2 also implement P i,0 , P i,1 , P i,2 but switch the position of v 3i , v 3i+1 , v 3i+2 with w 3i , w 3i+1 , w 3i+2 , respectively. By symmetry, the arguments that U σ3 ϕ satisfies Condition 4 are similar to the ones for U σ1 ϕ and U σ2 ϕ . Altogether, we have argued that U σ ϕ satisfies Condition 1 and Condition 4 for σ ∈ {σ 1 , σ 2 , σ 3 }. In the next section we talk about the fifth condition. By doing so, we also justify for why U σ3 ϕ 's construction different to U σ2 ϕ . An essential reason for this is that we have to fulfill both: Condition 4 and Condition 5.

8) g ,x i,0 g ,x i,1 g ,x i,2 g ,x i,3 k xi k Fig. 5. (1-3) Ti,0, Ti,1, Ti,2, (4) G x, i , (5-7) T i,0 , T i,1 , T i,2 , (8) G ,x i . (1-3,5-7):

The colored areas mark the supports of the three possible regions for Condition 5 as described in Section 3.5: red: Xi,0 ∈ M , green: Xi,1 ∈ M and blue: Xi,2 ∈ M . The (initial) states ti,0,0, ti,1,0 and ti,2,0 are mapped to 1 for all cases. (4,8): The colored areas define the support of (sup, sig) for Condition 5 as given in Section 3.5.

Details for Condition 5

For Condition 5, we start from a given one-in-three model M of ϕ and show that U σ ϕ allows a region (sup, sig) such that sig(k) = inp and sup(h 0,6 ) = 0 and V ⊆ sig −1 (enter) and W ⊆ sig −1 (keep − ).

For a start, let's restrict to σ 1 , σ 2 and the TSs T i,0 , T i,1 T i,2 implemented by

U σ1 ϕ , U σ2 ϕ and G x, i used by U σ2 ϕ where i ∈ {0, . . . , m − 1}: We define sig(k) = inp, sig(v 3i ), sig(v 3i+1 ), sig(v 3i+2 ) ∈ enter and sig(w 3i ), sig(w 3i+1 ), sig(w 3i+2 ) ∈ keep − , i ∈ {0, . . . , m − 1}. This requires sup(t i,0,2 ) = sup(t i,1,2 ) = sup(t i,2,2 ) = 1 and sup(t i,0,5 ) = sup(t i,1,5 ) = sup(t i,2,5 ) = 0. That is, for every T i,0 , T i,1 , T i,2

we have a path from 1 to 0 labeled by X i,0 , X i,1 , X i,2 and a path from 0 to 1 labelled by x i,0 , x i,1 , x i,2 . For the former path, we define sig(X) = inp if X ∈ M and sig(X) = nop if Y ∈ V (ϕ) \ M . Accordingly, for the latter path we let sig(x) ∈ enter if sig(X) = inp and, otherwise sig(x) = nop, cf. Figure 5.1-Figure 5.3: The red area sketches the case sig(X i,0 ) = inp, the green area sig(X i,1 ) = inp and the blue area sig(X i,2 ) = inp. States within the corresponding colored area are mapped to 1 the others to 0, respectively. If σ = σ 1 then, by Figure 5.1-Figure 5.3 and by recalling that every variable occurs exactly three times in exactly three clauses, it is easy to see that this yields a well defined region. Considering T i,0 , T i,1 , T i,2 alone, this is also true for σ 2 . However, for σ 2 we also need to take the TSs G x, 0 , . . . , G x, m−1 into account. Here, by sig(k) = inp we have that sup(g x, i,0 ) = sup(g x, i,1 ) = 1 such that sig(x i ) ∈ keep + . Hence, we need that sig(x i ) ∈ enter ∩ keep + , that is, sig(x i ) = set. Fortunately, all types τ ∈ σ 2 has the property set ∈ τ . We argue that (sup, sig) is extendable to U σ1 ϕ and U σ2 ϕ and their other TSs: With the help of the colored areas of the introduced TSs we extend (sup, sig) as follows. For every implemented gadget TS, the red colored area refers to states s such that sup(s) = 1, otherwise, sup(s) = 0. If s e s where s is in a red colored area and s is not, define sig(e) = inp. Similarly, if s is in a red colored area and s is not, define sig(e) ∈ enter. Finally, if either both of s, s are red or both not then define sig(e) = nop. One easily verifies that this yields a well defined region such such that U σ1 ϕ , U σ2 ϕ satisfy Condition 5. Unfortunately, as set ∈ τ for τ ∈ σ 3 this region can not exist for σ 3 which is one reason why σ 3 needs another construction. For U σ3 ϕ we obtain a corresponding region as follows: We define sig(k) = inp and V ⊆ sig −1 (enter) and W ⊆ sig −1 (keep − ) which requires sup(t i,0,2 ) = sup(t i,1,2 ) = sup(t i,2,2 ) = 0 and sup(t i,0,5 ) = sup(t i,1,5 ) = sup(t i,2,5 ) = 1. That is, for every T i,0 , T i,1 , T i,2 we have a path from 0 to 1 which is labeled by X i,0 , X i,1 , X i,2 and a path from 1 to 0 labelled by x i,0 , x i,1 , x i,2 . For the former path, we define sig(X) = swap if X ∈ M and sig(X) = nop if Y ∈ V (ϕ) \ M , cf. Figure 5.4-Figure 5.7. Accordingly, for the latter path we let sig(x) = res if sig(X) = swap and, otherwise sig(x) = nop. We take the TSs G ,x 0 , . . . , G ,x m−1 into account and, by sig(k) = inp we have sup(g ,x i,2 ) = sup(g ,x i,3 ) = 0 which is compatible with sig(x i ) = res. The extension of (sup, sig) to the remaining gadgets of U σ3 ϕ works analogously to U σ2 ϕ , where border-crossing events from 0 to 1 are mapped to swap (instead of set). Altogether, we have proven that U σ ϕ satisfies Condition 5 for σ ∈ {σ 1 , σ 2 , σ 3 }.

Concluding Remarks

In this paper we present a proof scheme to show the NP-hardness of synthesis, for 68 boolean Petri net types. Together with our previous work from [14], this already makes 111 out of 256 boolean net types where the complexity of synthesis has been figured out. In fact, with respect to the practically more relevant nopafflicted types of nets, there are only 17 cases left open. However, in view of our main target (dichotomy result) it remains for future work to characterize the synthesis complexity for all the remaining 145 types.

The NP-hardness results of the investigated synthesis problems motivates the search for (fixed-parameter) tractable special cases. There are at least two ways to (possibly) obtain such cases: Firstly, one can put (structural) restrictions on the τ -net N to be synthesized (the output) and require, for example, that N has to be free-choice or a marked graph [4]. To investigate the impact of such output-restrictions on the complexity of boolean net synthesis is certainly an interesting direction for further research.

Secondly, one can put restrictions on the TS from which N to synthesize (the input). One of the most obvious parameters here is the TS's state degree g, that is, the maximum number of ingoing and outgoing edges at a state. Actually, TSs of benchmarks of the digital hardware design community often have a low state degree [5]. However, our result show that it is very unlikely that feasibility is (fixed-parameter) tractable for parameter g: All gadget TSs have at most two ingoing and at most two outgoing edges per state, that is g ≤ 2, and this property is preserved by the joining-operation for A(U σ ϕ ). Clearly, this leaves us with the question if synthesis becomes tractable if g ≤ 1. On the one hand, that this can not generally be true has been shown in [15]. On the other hand, one observes that our reduction's functionality heavily bases on the ability to prevent a res-, setand swap-signature of certain events. The core gadgets here are T i,0 , T i,1 , T i,2 (implementing the paths P i,0 , P i,1 , P i,2 ) and the TSs G x, i and G ,x i . These gadgets are reliant on the possibility to have two ingoing and outgoing edges per state. Hence, the case g ≤ 1 is an object worth to study in future work, at least for the discussed types satisfying τ ∩ {set, res, swap} = ∅.