Boolean Petri nets are differentiated by types of nets based on which of the interactions nop, inp, out, set, res, swap, used, and free they apply or spare. From the 256 thinkable types only a few have yet been explicitly defined, as for instance contextual nets { nop, inp, out, used, free} and trace nets { nop, inp, out, set, res, used, free} . The synthesis problem relative to a specicfi type of nets τ is to find, for a given transition system A, a boolean τ -net with state graph isomorphic to A. It is known to be NP-hard for elementary nets systems { nop, inp, out} and tractable for flip-flop nets { nop, inp, out, swap} . This paper presents a general reduction scheme for the NP-hardness of boolean net synthesis and identifies 67 new types with a hard synthesis problem.
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} [
NP-complete 2 NP-complete 2 NP-complete 3 NP-complete 4 NP-complete 4 NP-complete 4 NP-complete 24+8 NP-complete 24+8
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 [
In this paper, we tackle 67 of them with a common NP-hardness proof scheme
and, additionally, reestablish the result for elementary net systems [
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 [
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) [
Due to space limitation, we are not able to present all proofs. However, all
omitted proofs are given in the technical report [
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) = s0 is interpreted as s e s0. 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 s0 ∈ 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 s0 by a directed path. 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
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} . nop free res 0 out, swap res, swap 1 nop nop 0 set, swap inp, swap 1 nop used set
A boolean Petri net N = (P, T, M0, f ) of type τ , (τ -net, for short) is given by finite and disjoint sets P of places and T of transitions, an initial marking M0 : 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 0 : P → − { 0, 1} where M 0(p) = δ τ (M (p), f (p, t)) for all p ∈ P . This is denoted by M t M 0. Given a τ -net N = (P, T, M0, 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 M0, can be reached by rfiing a sequence of transitions. For every reachable marking M and transition t ∈ T with M t M 0 the state transition function δ of A is defined as δ (M, t) = M 0.
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 s0 of A leads to a transition sup(s) sig(e) sup(s0) 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(τ 0) = { e ∈ E | sig(e) ∈ τ 0} for τ 0 ⊆ τ .
For a TS A = (S, E, ,δ s 0) and a type of nets τ , a pair of states s 6= s0 ∈ S is τ
separable if there is a τ -region (sup, sig) such that sup(s) 6= sup(s0). 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 [
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 τ = τ 0 ∪ ω for τ 0 ∈ { τ 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 [
If A0 = (S0, E0, δ 0, s00), . . . , An = (Sn, En, δ n, s0n) are (initialized) TSs with pairwise disjoint states (but not necessarily disjoint events) we say that U (A0, . . . , An) is their union. By S(U ), we denote the entirety of all states in A0, . . . , An 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 U1 = U (A10, . . . , A1n1 ), . . . , Um = (A0m, . . . , Annm ) are unions (possibly with Ui = U () or Ui = Ai) then U (U1, . . . , Um) is the union U (A10, . . . , A1n1 , . . . , A0m, . . . , Annm ).
We lift the concepts of regions, SSP, and ESSP to unions U = U (A0, . . . , An) 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 supi(s) = sup(s), s ∈ Si and sigi(e) = sig(e), e ∈ Ei provide a region (supi, sigi) of Ai. U has the τ -SSP if for all different states s, s0 ∈ S(U ) of the same TS Ai there is a τ -region (sup, sig) of U with sup(s) 6= sup(s0). 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 (A0, . . . , An) into a single TS, we define the joining A(U ): If s00, . . . , s0n 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.
δ (s, e) = si0, if s = ⊥ i and e = if s = ⊥ i and e = ⊥ i+1, i+1, δ i(s, e), if s ∈ Si and e ∈ Ei, i, ⊥ 0 0 A0 1 ⊥ 1 1 A1 2 . . .
n ⊥ n n An
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 6= ∅ . If U = U (A0, . . . , An) is a union of TSs A0, . . . , An 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.
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 τ˜. 3.2
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 ∪ ω | ω ⊆ { σ 2 = { τ 3 ∪ { swap} ∪ σ 3 = { τ 2 ∪ ω | ω ⊆ { used, free} ∪ { τ 3 ∪ ω | ω ⊆ { ω | ω ⊆ { out, res, used, free} used, free} out, res, 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 h0,6 ∈ S(Uϕ σ ) and there are events
V = { v0, . . . , v3m− 1} ⊆ E(Uϕ σ ) and W = { w0, . . . , w3m− 1} ⊆ E(Uϕ σ ). 3. If τ ∈ σ and (sup, sig) a τ -region inhibiting k at h0,6 then one of the following conditions is true: (a) sig(k) = inp and V ⊆ sig− 1(enter) and W ⊆ sig− 1(keep− ), (b) sig(k) = out and V ⊆ sig− 1(exit) and W ⊆ sig− 1(keep+). 4. If (sup, sig) is a region of Uϕ σ satisfying Condition 3.a or Condition 3.b then M = { X ∈ V (ϕ ) | sig(X) 6= nop} is a one-in-three model of ϕ . 5. If ϕ has a one-in-three model M and τ ∈ σ then there is a τ -region (sup, sig) with sig(k) = inp and sup(h0,6) = 0. Especially, (sup, sig) inhibits k at h0,6 and satisfies Condition 3.a. 6. If τ ∈ σ and k is τ -inhibitable at h0,6 then Uϕ σ has the τ -ESSP and the τ -SSP.
A polynomial time reduction scheme with these properties proves Theorem 1 as the following implications are justified: 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 h0,6. Due to space limitation, the proof that Uϕ σ
also has Condition 6 is moved to the technical report [
h0,1 h0,2
h0,3 To satisfy Condition 2, every union Uϕ σ implements the following transition system H that provides the event k, the state h0,6, where ¬ h0,6 k , and the events of Z = { z0, . . . , z3m− 1} , V = { v0, . . . , v3m− 1} and W = { w0, . . . , w3m− 1} (the colored areas are to be explained later): k z0 v0 k q0 z0 h0,4 h0,5 h0,0 h3m− 1,0 h3m,0 k k k h6m− 1,1 w3m− 1 h6m− 1,2 p3m− 1 h6m− 1,3 h6m− 1,0
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 h0,6 satisfies Condition 3. Thus, to achieve this goal other gadgets are necessary. By theirs different types (having h6m− 1,4 y3m− 1 h6m− 1,5 w3m− 1 h6m− 1,6 h0,6 c0 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 h0,6. The union Uϕ σ 1 implements additionally the following two TSs F0, F1: s k s0. Hence, we have sup(f0,3) = sup(f1,1) = sup(h0,4) = 1. By definition of inp, res we have that e s and sig(e) ∈ { inp, res} implies sup(s) = 0. Hence, by z0 f0,3 and q0 f1,1 we have that sig(z0), sig(q0) 6∈ { inp, res} . Moreover, we observe that swap 6∈ τ for all τ ∈ σ 1. Thus, sig(z0), sig(q0) ∈ keep+ such that sup(h0,4) = sup(h0,5) = sup(h0,6) = 1 which contradicts ¬ sup(h0,6) sig(k) . Hence, sig(k) 6= used. Similarly, one argues that sig(k) 6= free implies that sup(h0,6) = 0, again a contradiction. Hence, we have that sig(k) = inp and sup(h0,6) = 0 or sig(k) = out and sup(h0,6) = 1.
As a next step, we show that sig(k) = inp and sup(h0,6) = 0 implies sig(v0) ∈ enter and sig(z0) ∈ keep− : By sig(k) = inp and k h0,1 and h0,3 k that sup(h0,1) = 0 and sup(h0,3) = 1. By z0 h0,6, sup(h0,6) = 0 and swap 6∈ τ we have that sig(z0) ∈ keep− . Moreover, by sup(h0,1) = 0 and sig(z0) ∈ keep− it is sup(h0,2) = 0 which, by h0,2 v0 h0,3 and sup(h0,3) = 1, implies sig(v0) ∈ enter. Notice, that this reasoning purely bases on sig(k) = inp and sup(h0,6) = 0. Similarly, one argues that sig(k) = out and sup(h0,6) = 1 implies sig(v0) ∈ exit and sig(z0) ∈ keep+. Uϕ σ 1 uses for every i ∈ { 0, . . . , 6m − 2} the following TS Gc,c to transfer the support-value sup(h0,6) to the states h1,6, . . . , h6m− 1,6: i we have Gic,c= gic,,0c k gic,,2c ci ci gic,,1c
k gic,,3c
By doing so, it transfers the outcome of the latter observation to the events v1, . . . , v3m− 1 and w0, . . . , w3m− 1: If sig(k) = inp, then we have sup(gic,,0c) = sup(gic,,0c) = 1 and sup(gic,,2c) = sup(gic,,3c) = 0, that is, sig(ci) = nop. Symmetrically, if sig(k) = out then sig(ci) = nop. Hence, if sig(k) = inp and sup(h0,6) = 0 then sup(hi,6) = 0 for all i ∈ { 0, . . . , 6m − 1} . Perfectly similar to the discussion for z0 and v0 we obtain that V ⊆ sig− 1(enter) and W ⊆ sig− 1(keep− ), respectively. Symmetrically, sig(k) = out and sup(h0,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 F0, F1 (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 Gic,c and for i ∈ { 0, . . . , 3m − 1} following gadget TSs Gi,q and Gi,y:
Gi,y = gi,,0y k gi,,2y
yi F2 = f2,0 k f2,2 gi,,1y gi,,3y
k f2,1
k f2,3 Gi,q = gi,,0q k gi,,2q
qi G0n, = g0n,,0 k g0n,,2 gi,,1q gi,,3q
k g0n,,1
k g0n,,3 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 = { q0, . . . , q3m− 1} and Y = { y0, . . . , y3m− 1} . Moreover, Uϕ σ 2 adds the TS F0 (originally introduced for σ 1) and the next TS G0n, while Uϕ σ 3 uses also F0 and the following TS F2: n0 n0
That Uϕ σ 2 and Uϕ σ 3 differ in G0n, and F2, 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 s0 implies sup(s) = sup(s0) = 1. Applying this to F2, G0n, and G0,q we obtain that sig(n0), sig(q0) ∈ keep+. By sig(n0) ∈ keep+ and sup(f0,1) = 1 we obtain sup(f0,2) = 1 which, by sup(f0,3) = 1, implies sig(z0) ∈ keep+. Finally, by sup(h0,3) = 4 and sig(z0), sig(q0) ∈ keep+, we get sup(h0,6) = 1 which contradicts ¬ sup(h0,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(h0,6) = 0 implies V ⊆ sig− 1(enter) and W ⊆ sig− 1(keep− ): By sig(k) = inp we get again sig(ci) = nop and, thus, sup(hi,6) = 0 for all i in question. Moreover, by sig(k) = inp we get sup(s) = 0 for all k s. Applying this to Gi,q and Gi,y yields Q, Y ⊆ sig− 1(keep− ). By Q, Y ⊆ sig− 1(keep− ) and sup(hi,4) = 0 (for all i ∈ { 0, . . . , 6m − 1} ) we get sup(hi,5) = 0 which, by sup(hi,6) = 0, implies W, Z ⊆ sig− 1(keep− ). Finally, by Z ⊆ sig− 1(keep− ) and sup(hi,1) = 0 we conclude sup(hi,2) = 0 implying with sup(hi,3) = 1 that sig(vi) ∈ enter for every i ∈ { 0, . . . , 3m − 1} : V ⊆ sig− 1(enter). Symmetrically, sig(k) = out and sup(h0,6) = 1 implies W ⊆ sig− 1(keep+) and V ⊆ sig− 1(exit). Hence, Uϕ σ 2 and Uϕ σ 3 satisfy Condition 3. 3.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 e1 . . . en s0 the image R(P ) = sup(s) sig(e1) . . . sig(en) sup(s0) is a path in τ . Moreover, if sup(s) 6= sup(s0) = 0 then there has to be an event ei mapped to an interaction of τ that allows a state change in τ : sig(ei) 6∈ { nop, used, free} . Our target is to exploit this observation in the following way: Firstly, represent every clause ζ i = { Xi,0, Xi,1, Xi,2} by a path Pi,0 = ti,0,2 Xi,0 ti,0,3 Xi,1 ti,0,4 Xi,2 ti,0,5. Secondly, ensure that region (sup, sig) (inhibiting k at h0,6) requires sup(ti,0,2) 6= sup(ti,0,5) for every i ∈ { 0, . . . , m− 1} . Thirdly, ensure that there is exactly one variable event X ∈ { Xi,0, Xi,1, Xi,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) 6= nop} is a one-in-three model of ϕ as two different clauses ζ i, ζ j are represented by different paths Pi,0, Pj,0. Let’s discuss the case that region (sup, sig) satisfies sup(ti,0,2) = 1 and sup(ti,0,5) = 0. Unfortunately, generally there are many possibilities for the signature of the variable events Xi,0, Xi,1, Xi,2 and not even one of them need to be mapped to nop. For example, sig(X) = res or sig(X) = swap for X ∈ { Xi,0, Xi,1, Xi,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 Pi,0, Pi,1, Pi,2 which for every variable event X ∈ { Xi,0, Xi,1, Xi,2} use an additional mirror event x: Pi,0 = ti,0,2 Pi,2 = ti,2,2
Xi,0 xi,0 Xi,2 xi,2
Notice that, by the arbitrariness of i, we have for every X ∈ { X0, . . . , Xm− 1} = V (ϕ ) its unique mirror event x ∈ { x0, . . . , xm− 1} . Moreover, by definition, if s X s0 is a an edge (of any forward-backward path) then s x s0 is too. The paths Pi,0, Pi,1, Pi,2 are similar but the variable events are once and twice leftshifted, respectively. Secondly, we ensure that (sup, sig) also satisfies sup(ti,1,2) = sup(ti,2,2) = 1 and sup(ti,1,5) = sup(ti,2,5) = 0, that is, sup synchronizes the states ti,0,2, ti,1,2, ti,2,2 and the states ti,0,5, ti,1,5, ti,2,5, respectively. As a result, we have for every variable event X ∈ {
Xi,0, Xi,1, Xi,2} an edge X s such that sup(s) = 0. Consequently, we have that sig(X) ∈6 { 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) 6= 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 ∈ { Xi,0, Xi,1, Xi,2} with sig(X) ∈ { inp, res} implies that sig(Y ) = nop for Y ∈ { Xi,0, Xi,1, Xi,2} \ { Y } . We explicitly justify this claim only for X = Xi,0 as, by symmetry, the cases X = Xi,1 and X = Xi,2 are quite similar: By sig(Xi,0) ∈ { inp, res} we have sup(ti,0,3) = 0 which by sup(ti,0,2) = 1 and ti,0,2 xi,0 ti,0,3 implies sig(xi,0) ∈ { out, set, swap} . Again by sig(Xi,0) ∈ { inp, res} we have sup(ti,2,4) = 0 implying with sig(xi,0) ∈ { out, set, swap} that sup(ti,2,3) = 1. By ti,2,2 Xi,2 ti,2,3, sup(ti,2,2) = sup(ti,2,3) = 1 and sig(Xi,2) ∈ { nop, inp, res, swap} we conclude sig(Xi,2) = nop. Furthermore, by sup(ti,1,5) = 0 and sig(xi,0) ∈ { out, set, swap} we have sup(ti,1,4) = 1. By sig(Xi,2) = nop, ti,1,3 Xi,2 ti,1,4 and sup(ti,1,4) = 1 we obtain that sup(ti,1,3) = 1. Finally, by sup(ti,1,2) = sup(ti,1,3) = 1, ti,1,2 Xi,1 ti,1,3 and sig(Xi,1) ∈ { nop, inp, res, swap} we obtain sig(Xi,1) = nop.
So far, we have already argued that for types τ with swap 6∈ τ the following is true: A τ -region that synchronizes ti,0,2, ti,1,2, ti,2,2 and ti,0,5, ti,1,5, ti,2,5 as announced ensures that there is exactly one variable event of Xi,0, Xi,1, Xi,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 ∈ { Xi,0, Xi,1, Xi,2} and sig(X) = swap then sig(Y ) = nop for Y ∈ { Xi,0, Xi,1, Xi,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 ) 6∈ { inp, res} for Y ∈ { Xi,0, Xi,1, Xi,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 ∈ { Xi,0, Xi,1, Xi,2} then sig(x) = swap for all x ∈ { xi,0, xi,1, xi,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 xi ∈ { x0, . . . , xm− 1} , that is, especially for xi,0, xi,1, xi,2, the gadget TS Gix, which is defined in Figure 5.4. As ( sup, sig) satisfies sig(k) ∈ { inp, out} we have sup(gix,,0 ) = sup(gix,,1 ) which implies sig(xi) 6= swap for i ∈ { 0, . . . , m − 1} . Similarly, the union Uϕ σ 3 installs for every i ∈ { 0, . . . , m − 1} the gadget TS Gi,x 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) 6= nop} is a onein-three model of ϕ . Moreover, an analogous argument shows that sup(ti,0,2) = sup(ti,1,2) = sup(ti,2,2) = 0 and sup(ti,0,5) = sup(ti,1,5) = sup(ti,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 ti,0,2, ti,1,2, ti,2,2 and the states ti,0,5, ti,1,5, ti,2,5 become synchronized? To achieve this, we enhance Pi,0, Pi,1, Pi,2 as follows: If σ ∈ { σ 1, σ 2} then we enhance Pi,0, Pi,1, Pi,2 to Ti,0, Ti,1, Ti,2 in accordance to Figure 5.1- Figure 5.3, respectively. Ti,0, Ti,1 and Ti,2 apply the event k and the events v3i, v3i+1, v3i+2 and w3i, w3i+1, w3i+2. To make it clear: Besides the corresponding gadgets introduced in Section 3.3, Uϕ σ 1 and Uϕ σ 2 (additionally) implement the TSs Ti,0, Ti,1 and Ti,2 for every i ∈ { 0, . . . , m − 1} . Moreover, Uϕ σ 2 implements also Gix, 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(h0,6) = 0) imply V ⊆ sig− 1(enter) and W ⊆ sig− 1(keep− ). Moreover, by sig(K) = inp, we have sup(ti,0,1) = sup(ti,1,1) = sup(ti,2,1) = 0. Altogether, this implies sup(ti,0,2) = sup(ti,1,2) = sup(ti,2,2) = 1 and sup(ti,0,5) = sup(ti,1,5) = sup(ti,2,5) = 0. ti,1,4 ti,2,4 w3i w3i+1 w3i+2 Xi,2 xi,2 Xi,0 xi,0 Xi,1 xi,1
Moreover, if sig(k) = out then V ⊆ sig− 1(exit), implying sup(ti,0,2) = sup(ti,1,2) = sup(ti,2,2) = 0, and W ⊆ sig− 1(keep+), implying sup(ti,0,5) = sup(ti,1,5) = sup(ti,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 Ti,0, Ti,1, Ti,2 the transition system Ti0,0, Ti0,1, Ti0,2 defined in Figure 5.4-Figure 5.6, respectively. Ti0,0, Ti0,1, Ti0,2 also implement Pi,0, Pi,1, Pi,2 but switch the position of v3i, v3i+1, v3i+2 with w3i, w3i+1, w3i+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. ti,0,2 ti,1,2 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(h0,6) = 0 and V ⊆ sig− 1(enter) and W ⊆ sig− 1(keep− ).
For a start, let’s restrict to σ 1, σ 2 and the TSs Ti,0, Ti,1Ti,2 implemented by Uϕ σ 1 , Uϕ σ 2 and Gix, used by Uϕ σ 2 where i ∈ { 0, . . . , m − 1} : We define sig(k) = inp, sig(v3i), sig(v3i+1), sig(v3i+2) ∈ enter and sig(w3i), sig(w3i+1), sig(w3i+2) ∈ keep− , i ∈ { 0, . . . , m − 1} . This requires sup(ti,0,2) = sup(ti,1,2) = sup(ti,2,2) = 1 and sup(ti,0,5) = sup(ti,1,5) = sup(ti,2,5) = 0. That is, for every Ti,0, Ti,1, Ti,2 we have a path from 1 to 0 labeled by Xi,0, Xi,1, Xi,2 and a path from 0 to 1 labelled by xi,0, xi,1, xi,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.1Figure 5.3: The red area sketches the case sig(Xi,0) = inp, the green area sig(Xi,1) = inp and the blue area sig(Xi,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 Ti,0, Ti,1, Ti,2 alone, this is also true for σ 2. However, for σ 2 we also need to take the TSs Gx0, , . . . , Gxm,− 1 into account. Here, by sig(k) = inp we have that sup(gix,,0 ) = sup(gix,,1 ) = 1 such that sig(xi) ∈ keep+. Hence, we need that sig(xi) ∈ enter ∩ keep+, that is, sig(xi) = 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 s0 where s is in a red colored area and s0 is not, define sig(e) = inp. Similarly, if s0 is in a red colored area and s is not, define sig(e) ∈ enter. Finally, if either both of s, s0 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 6∈ τ 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(ti,0,2) = sup(ti,1,2) = sup(ti,2,2) = 0 and
sup(ti,0,5) = sup(ti,1,5) = sup(ti,2,5) = 1. That is, for every Ti0,0, Ti0,1, Ti0,2 we
have a path from 0 to 1 which is labeled by Xi,0, Xi,1, Xi,2 and a path from 1
to 0 labelled by xi,0, xi,1, xi,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 G0,x, . . . , Gm,x
− 1 into account and, by sig(k) = inp
we have sup(gi,,2x) = sup(gi,,3x) = 0 which is compatible with sig(xi) = 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} .
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 [
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 [
Secondly, one can put restrictions on the TS from which N is 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 [