Synthesis of Structurally Restricted b-bounded Petri Nets: Complexity Results

Abstract

Let $b\in \mathbb {N}^+$. A b-bounded Petri net (b-net) solves a transition system (TS) if its reachability graph and the TS are isomorphic. Synthesis (of b-nets) is the problem of finding for a TS A a b-net N that solves it. This paper investigates the computational complexity of synthesis, where the searched net is structurally restricted in advance. The restrictions relate to the cardinality of the preset and the postset of N’s transitions and places. For example, N is choice-free (CF) if the postset-cardinality of its places do not exceed one. If additionally the preset-cardinality of N’s transitions is at most one then it is fork-attribution. This paper shows that deciding if A is solvable by a pure or test-free b-net N which is choice-free, fork-attribution, free-choice, extended free-choice or asymmetric-choice, respectively, is NP-complete. Moreover, we show that deciding if A is solvable by a b-bounded weighted (m, n)-T-systems, $m,n\in \mathbb {N}$, is NP-complete if m, n belong to the input. On the contrary, synthesis for this class becomes tractable if $m,n\in \mathbb {N}$ are chosen a priori. We contrast this result with the fact that synthesis for weighted (m, n)-S-systems, being the T-systems’s dual class, is NP-complete for any fixed $m,n\ge 2$.

1 Introduction

Examining the behaviour of a system and deducing its behavioral properties is the task of system analyses. Its counterpart, synthesis, is the task to find for a given behavioral specification an implementing system. A valid synthesis procedure computes systems which are correct by design. However, the chances for obtaining an (efficient) algorithm for both analyses and synthesis, depend drastically on the given specification and the searched system: In [8] it has been shown that deciding liveness (the behavioral property) is EXPSPACE-hard for bounded Petri nets (the system), while it is NP-complete for free-choice Petri nets and polynomial for 1-safe free-choice nets. Similarly, the reachability problem is EXPSPACE-hard for bounded Petri nets, PSPACE-complete for free-choice 1-safe nets, NP-complete for acyclic 1-safe and conflict-free nets and polynomial for 1-safe conflict-free nets [8, 10].

In [12] it has been shown that it is impossible to decide if a modal transition system (the specification) can be implemented by a bounded Petri net, while synthesis of bounded Petri nets can be done in polynomial time if the specification is a transition system (TS, for short) [1]. An even better procedure for synthesis from TS is possible if the searched bounded Petri net is to be choice-free or a marked graph [4, 7]. Moreover, restricting the searched system to b-bounded Petri nets makes synthesis from modal TSs decidable for every fixed integer b [13].

In this paper, we investigate the following instance of synthesis: The specification is a TS A and the searched system is a b-bounded Petri net N (b-net, for short). We demand that N implements A up to isomorphism, that is, N’s reachability graph and A are isomorphic. Recently, in [15] we have shown that deciding the existence of N is NP-complete for every fixed $b\ge 1$. However, the former examples provide several results where restricting the system makes the corresponding analyses and synthesis problems easier. Encouraged by these results, we continue our work of [15] in this paper and address whether structurally restricting a searched b-net N influences positively the computational complexity of synthesis. The restrictions relate to the preset- and postset-cardinality of N’s transitions and places and correspond to well-known subclasses of Petri nets [3, 6, 9, 14]. Surprisingly, it turns out that almost all applied net restrictions do not bring the synthesis down to polynomial time. More exactly, we show that synthesis remains intractable if N is pure or test-free and satisfies one of the following properties: choice-free [6, 14], fork-attribution [14], free-choice, extended free-choice or asymmetric-choice [3]. Moreover, we adapt the classes of (weighted) T-systems and (weighted) marked graphs [9] for b-nets and introduce for $m,n\in \mathbb {N}$ their extension of weighted (m, n)-T-systems restricting the cardinality of the preset and the postset of N’s places by m and n, respectively. We show that synthesis of weighted (m, n)-T-systems is hard if m, n are part of the input and becomes tractable for every fixed m, n. In particular, synthesis of b-bounded weighted T-systems is polynomial which answers partly a question from [5, p.144]. Furthermore, we introduce their dual class of weighted (m, n)-S-systems which restricts the cardinality of the preset and postset of N’s transitions by m and n, respectively. In contrast to the result of its dual class, deciding if A is implementable by a pure or test-free b-net, being a weighted (m, n)-S-system, is NP-complete for every fixed $m,n\ge 2$. We get all intractability results by a reduction of the cubic monotone one-in-three-3-sat-problem and partly apply our methods from [15]. However, the reductions here are extremely specialized and tailored to synthesis of restricted nets.

The next Sect. 2 introduces all necessary preliminary notions, Sect. 3 presents our main result and Sect. 4 closes the paper.

2 Preliminaries

This section introduces all necessary preliminary notions and Fig. 1 gives corresponding examples. In the remainder of this paper, if not stated explicitly otherwise then $b\in \mathbb {N}^+$ is assumed to be arbitrary but fixed.

Transition Systems. An initialized transition system (TS, for short) $A=(S,E,\delta , s_0)$ consists of a finite disjoint set S of states, E of events, a partial transition function $\delta : S\times E\rightarrow S$ and an initial state $s_0\in S$. A can be interpreted as edge-labeled directed graph where every triple $\delta (s,e)=s'$ is an e-labeled edge , called transition. An event e occurs at state s, denoted by , if $\delta (s,e)=s'$ for some state $s'$. This notation is extended to words $w'=wa$, $w\in E^*, a\in E$, by inductively defining for all $s\in S$ and if and only if there is a state $s'\in S$ satisfying and . If $w\in E^*$ then denotes that there is a state $s'\in S$ such that . We assume all TSs to be reachable: .

b -bounded Petri Nets. A b-bounded Petri net (b-net, for short) $N=(P,T,f,M_0)$ consists of finite and disjoint sets of places P and transitions T, a (total) flow function $f: P \times T\rightarrow \{0,\dots , b\}^2$ and an initial marking $M_0: P \rightarrow \{0,\dots , b\}$. If $f(p,t)=(m,n)$ then $f^-(p,t)=m$ defines the consuming effect of t on p. Similarly, $f^+(p,t)=n$ defines t’s producing effect on p. The preset of a place p is defined by $\,^{\!\bullet }p=\{t\in T \mid f^+(p,t)>0\}$, the set of transitions that produce on p. Accordingly, p’s postset is defined by $p^{\bullet } =\{t\in T \mid f^-(p,t)>0\}$ and contains the transitions that consume from p. Similarly, the preset $\,^{\!\bullet }t=\{ p\in P \mid f^-(p,t)>0\}$ of a transition t is defined by the places from which t consumes and its postset $t^{\bullet } =\{p\in P \mid f^+(p,t)>0\}$ by the places on which t produces. Notice that neither $\,^{\!\bullet }p \cap p^{\bullet }$ nor $\,^{\!\bullet }t \cap t^{\bullet }$ is necessarily empty. A transition $t\in T$ can fire or occur in a marking $M:P\rightarrow \{0,\dots ,b\}$, denoted by , if $M(p)\ge f^-(p,t)$ and $M(p)-f^-(p,t)+f^+(p,t) \le b$ for all places $p\in P$. The firing of t in marking M leads to the marking $M'(p)=M(p)-f^-(p,t)+f^+(p,t)$ for $p\in P$, denoted by . Again, this notation extends to sequences $\sigma \in T^*$ and the reachability set contains all of N’s reachable markings. The firing rule preserves the b-boundedness of N by definition: $M(p) \le b$ for all places p and all $M\in RS(N)$. The reachability graph of N is the TS $A_N=(RS(N), T,\delta , M_0)$, where for every reachable marking M of N and transition $t \in T$ with the transition function $\delta$ of $A_N$ is defined by .

Structurally Restricted Subclasses of b-nets. A b-net N is pure if $\forall (p,t) \in P \times T : f^-(p,t)=0 \text { or } f^+(p,t) =0$, that is, $\forall p\in P: \,^{\!\bullet }p \cap p^{\bullet }=\emptyset$; test-free if $\forall (p,t) \in P \times T : f(p,t)\not =(0,0) \Rightarrow f^-(p,t)\not =f^+(p,t)$; choice-free (CF) or place-output-nonbranching if $\forall p\in P: \vert p^{\bullet } \vert \le 1$; fork-attribution (FA) if it is CF and, additionally, $\forall t\in T: \vert \,^{\!\bullet }t\vert \le 1$; free-choice (FC) if $\forall p,\tilde{p}\in P: p^{\bullet } \cap \tilde{p}^{\bullet } \not =\emptyset \Rightarrow \vert p^{\bullet } \vert = \vert \tilde{p}^{\bullet } \vert =1$; extended-free-choice (EFC) if $\forall p,\tilde{p}\in P: p^{\bullet }\cap \tilde{p}^{\bullet } \not =\emptyset \Rightarrow p^{\bullet } = \tilde{p}^{\bullet }$; asymmetric-choice (AC) if $\forall p,\tilde{p}\in P: p^{\bullet } \cap \tilde{p}^{\bullet } \not =\emptyset \Rightarrow (p^{\bullet } \subseteq \tilde{p}^{\bullet } \text { or } \tilde{p}^{\bullet } \subseteq p^{\bullet })$; for $m,n\in \mathbb {N}$ a weighted (m, n)-T-system if $\forall p\in P: \vert \,^{\!\bullet }p \vert \le m, \vert p^{\bullet } \vert \le n$; for $m,n\in \mathbb {N}$ a weighted (m, n)-S-system if $\forall t\in T: \vert \,^{\!\bullet }t \vert \le m, \vert t^{\bullet } \vert \le n$.

Fig. 1.

Top: Input TS A. Middle: For $i\in \{1,2,3,4,5\}$ pure 2-regions $R_i=(sup_i, sig_i)$ of A, where $R_1,\dots , R_4$ already solve all of A’s (E)SSP atoms. For example, the region $R_1$ solves $(k, s_i)$, $\forall i \in \{2,3,6\}$ and $(o,s_i)$, $\forall i\in \{0,1,4,5\}$. Bottom: Pure 2-net $N^{\mathcal {R}}_A$, built by $\mathcal {R}=\{R_1,R_2,R_3,R_4\}$, where, for example, $\,^{\!\bullet }R_3=\{ o \}$ and $R_3\!^{\bullet }=\{z\}$ and $\,^{\!\bullet }o=\{R_1\}$ and $o^{\bullet }=\{R_3 \}$. Moreover, $N^{\mathcal {R}}_A$ is FA because of $\vert R^{\bullet } \vert \le 1$ and $\vert \,^{\!\bullet }e_{\mathcal {R}} \vert \le 1$ for all $R\in \mathcal {R}$ and $e\in E(A)$. The net $N^{\mathcal {R}}_A$ origins from $N^{\mathcal {R}'}_A$, where $\mathcal {R}'=\mathcal {R} \cup \{\ R_5\ \}$, by removing $R_5$. Both $\mathcal {R}$ and $\mathcal {R}'$ are b-admissible sets. Thus, the reachability graphs of their synthesized nets are both isomorphic to A. However, because $z\in R_3\!^{\bullet } \cap R_5\!^{\bullet }$ and $R_5\!^{\bullet } = \{z,o\}$, the net $N^{\mathcal {R}'}_A$ is not even free-choice.

b -bounded Regions. For the purpose of finding a b-net N implementing a TS A, we want to synthesize N’s components purely from the input A. Demanding A and $A_N$ to be isomorphic suggests that A’s events correspond to N’s transitions. However, the notion of a place is not known for TSs. A b-bounded region R (b-region, for short) of a TS $A=(S,E,\delta ,s_0)$ is a pair $R=(sup, sig)$ of support $sup: S\rightarrow \{0,\dots , b\}$ and signature $sig: E\rightarrow \{0,\dots , b\}^2$, where $sig^-(e)=m$ and $sig^+(e)=n$ for $sig(e)=(m,n)$, such that for every edge of A holds $sup(s)\ge sig^-(e)$ and $sup(s')=sup(s)-sig^-(e)+sig^+(e)$. A region (sup, sig) models a place p and the corresponding part of the flow function f: $sig^+(e)$ models $f^+(e)$, $sig^-(e)$ models $f^-(e)$ and sup(s) models M(p) in the marking $M\in RS(N)$ corresponding to $s\in S(A)$. Accordingly, a region R is test-free if $sig(e)\not =(0,0)$ implies $sig^-(e)\not =sig^+(e)$. The preset of R is defined by $\,^{\!\bullet }R=\{e\in E \mid sig^+(e) > 0\}$ and its postset by $R^{\bullet } =\{e\in E \mid sig^-(e) > 0\}$. The Region R is pure if $\,^{\!\bullet }R \cap R^{\bullet } =\emptyset$. For a set $\mathcal {R}$ of b-regions and $e\in E$ we define by $\,^{\!\bullet }e_{\mathcal {R}}=\{(sup, sig)\in \mathcal {R} \mid sig^-(e)>0 \}$ the preset and by $e_{\mathcal {R}}^{\bullet } =\{(sup, sig) \in \mathcal {R} \mid sig^+(e)>0 \}$ the postset of e (in accordance to $\mathcal {R}$). Every set $\mathcal {R}$ of b-regions of A defines the synthesized b-net $N^{\mathcal {R}}_A=(\mathcal {R}, E, f, M_0)$ with flow function $f((sup, sig),e)=sig(e)$ and initial marking $M_0((sup, sig))=sup(s_{0})$ for all $(sup, sig)\in \mathcal {R}, e\in E$. We emphasize once again that a region R of $\mathcal {R}$ becomes a place of $N^{\mathcal {R}}_A$ with the preset $\,^{\!\bullet }R$ and the postset $R^{\bullet }$. Moreover, every event $e\in E$ becomes a transition of $N^{\mathcal {R}}_A$ with preset $\,^{\!\bullet }e = \,^{\!\bullet }e_\mathcal {R}$ and postset $e^{\bullet } = e_\mathcal {R}\!^{\bullet }$. It is well known that $A_{N^{\mathcal {R}}_A }$ and A are isomorphic if and only if $\mathcal {R}$’s regions solve certain separation atoms [2], to be introduced next.

A pair $(s, s')$ of distinct states of A define a state separation atom (SSP atom, for short). A b-region $R=(sup, sig)$ solves $(s,s')$ if $sup(s)\not =sup(s')$. The meaning of R is to ensure that $N^{\mathcal {R}}_A$ contains at least one place R such that $M(R)\not =M'(R)$ for the markings M and $M'$ corresponding to s and $s'$, respectively. If there is a b-region that solves $(s,s')$ then s and $s'$ are called b-solvable. If every SSP atom of A is b-solvable then A has the b-state separation property (b-SSP, for short).

A pair (e, s) of event $e\in E$ and state $s\in S$ where e does not occur at s, that is , define an event state separation atom (ESSP atom, for short). A b-region $R=(sup, sig)$ solves (e, s) if $sig^-(e) > sup(s)$ or $sup(s)-sig^-(e)+sig^+(e)>b$. The meaning of R is to ensure that there is at least one place R in $N^{\mathcal {R}}_A$ such that for the marking M corresponding to s. If there is a b-region that solves (e, s) then e and s are called b-solvable. If every ESSP atom of A is b-solvable then A has the b-event state separation property (b-ESSP, for short).

A set $\mathcal {R}$ of b-regions of A is called b-admissible if for every of A’s (E)SSP atoms there is a b-region R in $\mathcal {R}$ that solves it. The following lemma, borrowed from [2, p.163], summarizes the already implied connection between the existence of b-admissible sets of A and (the solvability of) synthesis:

Lemma 1

([2]). A b-net N has a reachability graph isomorphic to a given TS A if and only if there is a b-admissible set $\mathcal {R}$ of A such that $N=N^{\mathcal {R}}_A$.

We say a b-net N solves A if $A_N$ and A are isomorphic. By Lemma 1, searching for a restricted b-net reduces to finding a b-admissible set of accordingly restricted regions. The following two examples illustrate this fact.

Example 1

If $\mathcal {R}$ is a b-admissible set of pure regions of A satisfying $\forall R\in \mathcal {R}: \vert R^{\bullet } \vert \le 1$ and $\forall e \in E(A): \vert \,^{\!\bullet }e_{\mathcal {R}}\vert \le 1$ then $N^{\mathcal {R}}_A$ is a pure FA b-net solving A.

Example 2

If $\mathcal {R}$ is a b-admissible set of pure regions of A and $\forall e \in E(A): \vert \,^{\!\bullet }e_{\mathcal {R}} \vert \le 2, \vert e_{\mathcal {R}}\!^{\bullet }\vert \le 2$ then $N^{\mathcal {R}}_A$ is a pure solving b-net, being a weighted (2, 2)-S-system.

3 Our Contribution

Theorem 1

For a given TS A the following conditions are true:

• 1. If $P\in \{CF, FA, FC, EFC, AC \}$ then to decide if A is solvable by a pure or a test-free b-net which is P is NP-complete.

• 2. Given integers $\ell ,\ell '\in \mathbb {N}$, deciding if A is solvable by a pure or a test-free b-net, being a weighted $(\ell ,\ell ')$-T-System, is NP-complete.

• 3. For any fixed $\ell ,\ell ' \ge 2$, deciding if A is solvable by a pure or a test-free b-net, being a weighted $(\ell ,\ell ')$-S-system, is NP-complete.

• 4. For any fixed $\ell ,\ell ' \in \mathbb {N}$, one can decide in polynomial time if A is solvable by a b-net, being a weighted $(\ell ,\ell ')$-T-System.

To prove Theorem 1.1–Theorem 1.3 we show that the corresponding decision problems are in NP and NP-hard. Membership in NP can be seen as follows: By Lemma 1, if N is a b-net that solves A then there is a b-admissible set $\mathcal {R}'$ of A such that $N^{\mathcal {R}'}_A=N$. By definition, A has at most $\vert S\vert ^2$ SSP atoms and at most $\vert E\vert \cdot \vert S\vert$ ESSP atoms. Thus, there is a b-admissible subset $\mathcal {R} \subseteq \mathcal {R}'$ with $\vert \mathcal {R} \vert \le \vert S\vert ^2 + \vert E\vert \cdot \vert S\vert$. In particular, $N^{\mathcal {R}}_A$ originates from $N^{\mathcal {R}'}_A=N$ by (possibly) removing places, which can not increase any preset- or postset cardinality. Consequently, removing places preserves property $P\in \{CA, FA, FC,EFC, AC\}$, the weighted (m, n)-T-system property and the weighted (m, n)-S-system property. This makes $N^{\mathcal {R}}_A$ a searched net. A non-deterministic Turing machine can guess in polynomial time a corresponding set $\mathcal {R}$, check its b-admissibility, build $N^{\mathcal {R}}_A$ and check its structural properties in accordance to the regarded decision problem.

To show hardness we use the NP-complete problem cubic monotone one-in-three-3-sat (cm 1-in-3 3sat) from [11] which is defined as follows: The input for cm 1-in-3 3sat is a negation-free boolean expression $\varphi =\{ \zeta _0, \dots , \zeta _{m-1}\}$ of three-clauses $\zeta _0,\dots , \zeta _{m-1}$ with set of variables $V(\varphi )$ where every variable occurs in exactly three clauses. Notice that this implies $\vert V(\varphi )\vert =m$. The question is whether there is a subset $M\subseteq V(\varphi )$ satisfying $\vert M \cap \zeta _i \vert =1$, $\forall i\in \{0,\dots , m-1\}$.

For Theorem 1.(1–2) we reduce an input instance $\varphi$ with m clauses (in polynomial time) to a TS $A^b_\varphi$ satisfying the following condition:

Condition 1

• 1. If a test-free b-net solves $A^b_\varphi$ then $\varphi$ is one-in-three satisfiable.

• 2. If $\varphi$ is one-in-three satisfiable then there is a b-admissible set $\mathcal {R}$ of pure regions of $A^b_\varphi$ satisfying $\forall R\in \mathcal {R}: \vert R^{\bullet } \vert \le 1 \wedge \vert \,^{\!\bullet }R \vert \le 7m+4$ and $\forall e \in E(A): \vert \,^{\!\bullet }e_{\mathcal {R}}\vert \le 1$.

A reduction that satisfies Condition 1 proves Theorem 1.(1–2) as follows: By definition of test-freeness, every b-net of Theorem 1.(1–2) is at least test-free, although possibly further restricted. Hence, Condition 1.1 ensures that if $A^b_\varphi$ is solvable by such a net then $\varphi$ has a one-in-three model. Moreover, a b-admissible set $\mathcal {R}$ that satisfies Condition 1.2 implies that $N^{\mathcal {R}}_{A^b_\varphi }$ is a pure b-net that is FA and solves A, cf. Example 1. Every pure FA b-net is test-free (by $f^+(p,t)=0$ or $f^-(p,t)=0$) and CF (by definition). By $N^{\mathcal {R}}_{A^b_\varphi }$ being CF, all of its places p satisfy $\vert p^{\bullet } \vert \le 1$. Thus, the net is also FC, EFC and AC. Finally, by $\ell = 7m+4$ and $\ell '=1$, the net $N^{\mathcal {R}}_{A^b_\varphi }$ is a weighted $(\ell ,\ell ')$-T-system. Altogether, Condition 1 ensures that $A^b_\varphi$ is solvable by a b-net of Theorem 1.(1–2) if and only if $\varphi$ is one-in-three satisfiable.

For Theorem 1.3 we reduce $\varphi$ to a TS $B^b_\varphi$ that satisfies the following condition:

Condition 2

• 1. If a test-free b-net solves $B^b_\varphi$ then $\varphi$ is one-in-three satisfiable.

• 2. If $\varphi$ is one-in-three satisfiable then there is a b-admissible set $\mathcal {R}$ of pure regions such that $\vert \,^{\!\bullet }e_{\mathcal {R}} \vert \le 2$ and $\vert e_{\mathcal {R}}\!^{\bullet } \vert \le 2$ for all $e \in E(A)$.

A reduction satisfying Condition 2 proves Theorem 1.3 as follows: By the definition of test-freeness and weighted (m, n)-S-systems, a pure weighted (2, 2)-S-system is a test-free weighted (m, n)-S-System for all $m,n\ge 2$. Moreover, a b-admissible set that satisfies Condition 2.2 implies that $N^{\mathcal {R}}_{B^b_\varphi }$ is a pure weighted (2, 2)-S-system solving $B^b_\varphi$, cf. Example 2. Thus, Condition 2 ensures that $B^b_\varphi$ is solvable by a b-net of Theorem 1.3 if and only if $\varphi$ is one-in-three satisfiable.

3.1 The Reduction and the Proof of Condition 1.1 and Condition 2.2

In accordance to Condition 1.1 and Condition 2.1, our goal is to combine the existence of a b-admissible set $\mathcal {R}$, the b-solvability of $A^b_\varphi$ and $B^b_\varphi$, with the one-in-three satisfiability of $\varphi$. For this purpose, both TSs (among others) apply gadgets that represent $\varphi$’s clauses and use their variables as events. Moreover, both $A^b_\varphi$ and $B^b_\varphi$ have a certain separation atom and the signature of a solving region (sup, sig) defines a one-in-three model of $\varphi$ via the variable events. So far, this approach is like that of [15]. However, the main difference and the biggest challenge is to consider the restrictions of Condition 1.1 and Condition 2.2. To master this challenge, we apply refined, specialized and different gadgets. Particularly noteworthy in this context is the representation of $\varphi$’s clauses by $\{0,\dots , b\}^3$-grids instead of simple sequences, as it has been done in [15].

We proceed by introducing the gadgets of $A^b_\varphi$ and $B^b_\varphi$ that represent $\varphi$’s clauses. In particular, the clause-gadgets’ functionality will serve as motivation for the remaining parts of $A^b_\varphi$ and $B^b_\varphi$, which are presented afterwards.

Let $i\in \{0,\dots , m-1\}$. The TSs $A^b_\varphi$ and $B^b_\varphi$ have for the clause $C_i=\{X_{i,0}, X_{i,1}, X_{i,2}\}$ the $\{0,\dots , b\}^3$-grid $C^b_i$ with transitions that use the variables of $C_i$ as events. More exactly, the $\{0,\dots , b\}^3$-grid $C^b_i$ is built by the following sequences $P^{i,0}_{\alpha ,\beta }, P^{i,1}_{\alpha ,\beta }, P^{i,2}_{\alpha ,\beta }$, where $\alpha ,\beta \in \{0,\dots , b\}$. Figure 2 shows $C^2_i$.

Among others, $C^b_i$ provides the following sequence $P_i$ where each of $X_{i,0}, X_{i,1}$ and $X_{i,2}$ occur b times in a row:

Notice that, except for $t^i_{b,b,b}$, every variable of $C_i$ occur at every state of $C^b_i$. This has the advantage that we never have to solve an ESSP atom (X, s) such that $X\in \{X_{i,0}, X_{i,1}, X_{i,2}\}$ and s occur in the same grid and s is a source of another variable event $Y\in \{X_{i,0}, X_{i,1}, X_{i,2}\}\setminus \{X\}$. This property is crucial to ensure Condition 1.2 and Condition 2.2. In particular, it prevents atoms like $( X_{i,1},t^i_{b-1,0,0})$ which would be unsolvable for $b\ge 2$.

The TSs $A^b_\varphi$ and $B^b_\varphi$ use the grid $C^b_i$ as follows: Both TSs have at least one separation atom such that a corresponding b-solving region (sup, sig) satisfies either $sup(t^i_{0,0,0})=0$ and $sup(t^i_{b,b,b})=b$ or $sup(t^i_{0,0,0})=b$ and $sup(t^i_{b,b,b})=0$. In the following, we assume $sup(t^i_{0,0,0})=0$ and $sup(t^i_{b,b,b})=b$ and argue that this implies that there is exactly one $X\in \{X_{i,0}, X_{i,1}, X_{i,2}\}$ with $sig(X)\not =(0,0)$. If $X\in \{X_{i,0}, X_{i,1}, X_{i,2}\}$ then, by $sup(t^i_{0,0,0})=0$ and , we have immediately $sig^-(X)=0$ (no consuming is possible). Moreover, by the definition of regions, we have $sup(s')=sup(s)-sig^-(e)+sig^+(e)$ for every . We use all this together and obtain inductively that $b=sup(t^i_{b,b,b})=b\cdot (sig^+(X_{i,0})+sig^+(X_{i,1})+sig^+(X_{i,2})) > 0 = sup(t^i_{0,0,0})$. It is easy to see that this expression is satisfied if and only if there is exactly one variable event with a positive value $sig^+$ (and this value equals 1). Thus, there is exactly one event $X\in \{X_{i,0}, X_{i,1}, X_{i,2}\}$ with $sig(X)\not =(0,0)$. By the arbitrariness of i this is simultaneously true for all grids $C^b_0,\dots , C^b_{m-1}$. Consequently, the set $M=\{X\in V(\varphi )\mid sig(X)\not =(0,0)\}$ selects exactly one element of every clause $C_i$ which makes it a one-in-three model of $\varphi$. Similarly, if $sup(t^i_{0,0,0})=b$ and $sup(t^i_{b,b,b})=0$ then M yields also a one-in-three model of $\varphi$.

With the just presented functionality of $C^b_i$ in mind, in what follows, we introduce $A^b_\varphi$’s and $B^b_\varphi$’s remaining parts. In particular, we explain how they collaborate to ensure the existence of a region satisfying $sup(t^i_{0,0,0})=0$ and $sup(t^i_{b,b,b})=b$ or $sup(t^i_{0,0,0})=b$ and $sup(t^i_{b,b,b})=0$. Before we start, the following lemma provides a basic result, to be used in the sequel, and shows how to connect the signature of some events with the solvability of an ESSP atom.

Fig. 2.

A snippet of $A^2_\varphi$ showing the sequences $Q^2$, $M^2_i$, $N^2_i$, the $\{0,1,2\}^3$-grid $C^2_i$ for the clause $C_i=\{X_{i,0}, X_{i,1}, X_{i,2}\}$ and the paths $L_{i,0}$ and $L_{i,1}$. For clarity, edges labeled by the same variable event have the same color. The coloring of the states corresponds to the 2-region $R_1$ which is defined in Table 1 and where $X_{i,0}\in M$: Light (dark) red colored states are mapped to 1 (2) and the others are mapped to 0. (Color figure online)

Lemma 2

Let be a sequence of a TS $A=(S,E,\delta ,s_0)$, where $e_1,e_2,e_3$ are pairwise distinct events, which starts and ends with $e_1$ b-times in a row. A test-free b-region solves the ESSP atom $(e_1,q_{b+1})$ if and only if $sig(e_1)=(0,1)$, $sig^-(e_2)=sig^+(e_2)$ and $sig(e_3)=(b,0)$ or $sig(e_1)=(1,0)$, $sig^-(e_2)=sig^+(e_2)$ and $sig(e_3)=(0,b)$.

We start by introducing the parts of $A^b_\varphi$. Figure 2 sketches a snippet of $A^2_\varphi$. The initial state of $A^b_\varphi$ is s. Firstly, the TS $A^b_\varphi$ has the sequence $Q^b$:

The sequence $Q^b$ provides the ESSP-atom $(k,q_{b+1})$. If $A^b_\varphi$ is b-solvable then, by Lemma 1, there is a b-admissible set $\mathcal {R}$ of (test-free) regions such that $N=N^\mathcal {R}_{A^b_\varphi }$. As $\mathcal {R}$ is b-admissible, there is a test-free b-region $(sup, sig) \in \mathcal {R}$ that solves $(k,q_{b+1})$. By Lemma 2, we have either $sig^-(z)=sig^+(z)$ and $sig(o)=(b,0)$ or $sig^-(z)=sig^+(z)$ and $sig(o)=(0,b)$. Let’s discuss the former case. The region R implies for transitions and (of $A^b_\varphi$) that $sup(s)=b$, $sup(s')=0$ and $sup(s'')=sup(s''')$. The TS $A^b_\varphi$ uses this to ensure a particular signature of the events $k_{2i}, k_{2i+1}$ that are provided by the following sequences $N^b_i$ and $M^b_i$, for all $i\in \{0,\dots , m-1\}$:

The TS $A^b_\varphi$ uses $M^b_i$, $N^b_i$, R and the occurrences of z and o for the announced goal as follows: By $sig(o)=(b,0)$, we have $sup(m_{i,1})=sup(n_{i,1})=0$ and $sup(m_{i,3})=sup(n_{i,3})=b$ which, by $sig^-(z)=sig^+(z)$, implies $sup(m_{i,2})=sup(n_{i,2})=b$. By , this leads to $sig(k_{2i})=sig(k_{2i+1})=(0,b)$. In particular, for all edges and of $A^b_\varphi$ holds $sup(s)=sup(s'')=0$ and $sup(s')=sup(s''')=b$. Finally, $A^b_\varphi$ uses other occurrences of $k_{2i}$ and $k_{2i+1}$ to ensure $sup(t^i_{0,0,0})=0$ and $sup(t^i_{b,b,b})=b$. More exactly, $A^b_\varphi$ installs the paths and . On the one hand, $L_{i,0}$ ensures reachability of $A^b_\varphi$. On the other hand, by , and the discussion above, $L_{i,0}, L_{i,1}$ ensure that $sup_0(t^i_{0,0,0})=0$ and $sup_0(t^i_{b,b,b})=b$.

Similarly, one argues that $sig(o)=(0,b)$ and $sig^-(z)=sig^+(z)$ yields $sig(k_{2i})=sig(k_{2i+1})=(b,0)$, implying $sup_1(t^i_{0,0,0})=b$ and $sup_1(t^i_{b,b,b})=0$. By the discussed functionality of the grids, this proves that $A^b_\varphi$ satisfies Condition 1.1.

We proceed by presenting the remaining gadgets of $B^b_\varphi$. The TS $B^b_\varphi$ has the initial state s and it has for every $i\in \{0,\dots , m-1\}$ the following six sequences:

In terms of Condition 2.2, the gadgets $M^b_i, N^b_i, L_{i,0}$ and $L_{i,1}$ work similar to the corresponding ones of $A^b_\varphi$. However, Condition 2.2 requires to distribute the task of one event to multiple events. For example, the events $z_0,\dots , z_{2m-1}$ of $B^b_\varphi$ play the same role as z of $A^b_\varphi$. This is achieved by $F^b_i$ and $G^b_i$. More exactly, if $B^b_\varphi$ is b-solvable then, by Lemma 1, every atom $(k, f^i_{b+1})$ is too. By Lemma 2, if (sup, sig) is a solving test-free b-region then $sig(k)=(0,1)$ and $sig(o)=(b,0)$ or $sig(k)=(1,0)$ and $sig(o)=(0,b)$. If $sig(k)=(0,1)$ then, by $sup(f^i_b)=sup(g^i_b)=b\cdot sig^+(k)=b$ and $sup(f^i_{b+1})=sup(f^i_{b+1})=b$, we get $sig^+(z_i)=sig^-(z_i)$ and, thus, $sig(k_i)=(0,b)$, $\forall i\in \{0,\dots , 2m-1\}$. Similarly, if $sig(k)=(1,0)$ then $sig(k_i)=(b,0)$, $\forall i\in \{0,\dots , 2m-1\}$. Thus, by the grids’ functionality, the set $M=\{X\in V(\varphi ) \mid sig(X)\not =(0,0)\}$ is a sought model.

3.2 The Proof of Condition 1.2 and Condition 2.2

In this section, we provide b-admissible sets of $A^b_\varphi$ and $B^b_\varphi$ in accordance to Condition 1.2 and Condition 2.2, respectively. For the sake of simplicity, we present for every region (sup, sig) only its signature sig and the value sup(s) of the initial state s. Because $A^b_\varphi$ and $B^b_\varphi$ are reachable and $sup(s'')=sup(s')-sig^-(e)+sig^+(e)$ for every transition , this completely defines the region. In the remainder of this section, unless stated explicitly otherwise, let $i\in \{0,\dots , m-1\}$ and M be a one-in-three model of $\varphi$. Moreover, for $\alpha \in \{0,1,2\}$ let $\beta _\alpha ,\gamma _\alpha \in \{0,\dots , m-1\}\setminus \{i\}$ be the distinct indices such that $X_{i,\alpha }\in C_i\cap C_{\beta _\alpha }\cap C_{\gamma _\alpha }$, that is, $\beta _\alpha ,\gamma _\alpha$ choose the other two clauses of $\varphi$ containing $X_{i,\alpha }$.

Table 1. Pure regions of $A^b_\varphi$ that solve $k,z,o,k_{2i}, k_{2i+1}$ and $X_{i,0}, X_{i,1}, X_{i,2}$.

We start with Condition 1.2 and provide a b-admissible set $\mathcal {R}$ of pure regions of $A^b_\varphi$ such that $\vert R^{\bullet }\vert \le 1$ and $\vert \,^{\!\bullet }e_{\mathcal {R}} \vert \le 1$ for all $R\in \mathcal {R}$ and $e\in E(A^b_\varphi )$. Moreover, because $A^b_\varphi$ has exactly $7m+4$ events, every region R of $A^b_\varphi$ satisfies $\vert \,^{\!\bullet }R \vert \le 7m+4$. For abbreviation, we define $U=\{u_0,\dots , u_{m-1}\}, V=\{v_0,\dots , v_{m-1}\}, W=\{w_0,\dots , w_{m-1}\}, Y=\{y_0,\dots , y_{m-1}\}$ and $K=\{k_0,\dots ,k_{2m-1}\}$. We solve all atoms concerning the events of $\{a\}\cup U\cup V\cup W\cup Y$ with the region $R=(sup, sig)$, defined by $sup(s)=0$ and $sig(e)=(0,b)$ if $e\in \{a\}\cup U\cup V\cup W\cup Y$ and, otherwise, $sig(e)=(0,0)$. This region satisfies $\vert R^{\bullet } \vert =0$ (no event consumes). Moreover, none of the subsequently presented regions of $A^b_\varphi$ is in the preset of any of $\{a\}\cup U\cup V\cup W\cup Y$, thus, $\vert \,^{\!\bullet }e_{\mathcal {R}}\vert \le 1$ for $e\in \{a\}\cup U\cup V\cup W\cup Y$. We proceed with presenting for every event $k,z,o,v, k_{2i}, k_{2i+1}$ and $X_{i,0}, X_{i,1}, X_{i,2}$ corresponding regions that solves it. Every row of Table 1 (below) defines a region $R=(sup_R, sig_R)$ with $sup_R(s)=0$ as follows: For every $e\in E(A^b_\varphi )$ we have either $sig_R(e)=(0,0)$ or $sig_R(e)\in \{(1,0), (0,1), (b,0), (0,b)\}$. In the latter case, e occurs according to its signature in the corresponding column either as a single event or as member of the event set shown. For example, for $R_1$ we have $sig_{R_1}(k)=(0,1)$ and $sig_{R_1}(e)=(0,1)$ for $e\in M$.

The regions of Table 1 solve the events $k,z,o,k_{2i}, k_{2i+1}$ and $X_{i,0}, X_{i,1}, X_{i,2}$ as follows. (k): $R_1$ solves k at the sinks of z and $R_2$ solves k at the remaining states. (z): $R_2$ solves z at the sources of k and $R_3$ solves z at o’s sources and at s. $R^z_{k_{2i}}$ and $R^z_{k_{2i+1}}$, where $i\in \{0,\dots , m-1\}$, solve z at the sources of $k_0,\dots , k_{2m-1}$. Finally, $R_4$ solves z at the remaining states. (o): $R_1$ solves o at the sources of k, $k_{0},\dots , k_{2m-1}$ and at s and $R_3$ solves o at the remaining states. $(k_{2i})$: $R_1$ solves $k_{2i}$ at all sources of o and all sources of $X_{i,\alpha }$ in $C^b_i$, where $X_{i,\alpha }\in M$. $R^z_{k_{2i}}$ solves $k_{2i}$ at all sources of $k_j$, where $2i\not = j\in \{0,\dots , 2m-1\}$ and at s. The remaining atoms are solved by (the two regions defined by) $R^\alpha _{k_{2i}}$, where $\alpha \in \{0,1,2\}$ such that $X_{i,\alpha }\not \in M$. $(k_{2i+1})$: $R_1$ solve $k_{2i+1}$ at $n_{i,0}$ and $R^z_{k_{2i+1}}$ at s and $R_{k_{2i+1}}$ at all remaining states. $(X_{i,\alpha })$: If $X_{i,\alpha }\in M$ then the region $R_1$ solves it at $t^i_0$, otherwise, $X_{i,\alpha }$ is solved at $t^i_0$ by $R^\alpha _{k_{2i}}$. The remaining atoms are solved by $R_{X_{i,\alpha }}$.

In the following we argue that $A^b_\varphi$ has the SSP, too: To separate $S(Q_b)$ from $S(A^b_\varphi )\setminus S(Q_b)$ we use the region $R_Q=(sup_Q,sig_Q)$ where $sup_Q(s)=0$, $sig_Q(a)=(0,b)$ and $sig_Q(e)=(0,0)$ for the other events. Moreover, the states of $Q_b$ are pairwise separated by $R_1,R_2$ and $R_4$. To separate the states $S(M^b_i)$ from $S(A^b_\varphi )\setminus S(M^b_i)$ we define the region $R_{M_{i}}=(sup_{M_i},sig_{M_i)}$ where $sup_{M_i}(s)=0$, $sig_{M_i}(w_i)=(0,b)$ and $sig_{M_i}(e)=(0,0)$ for the other events. The states of $M^b_i$ are pairwise separated by $R_1, R_2, R_3$ and $R_4$. Similarly, the states $S(N^b_i)$ are separated by $R_1, R_2, R_3,R_4$ and $R_{N_{i}}=(sup_{N_i},sig_{N_i)}$ where $sup_{N_i}(s)=0$, $sig_{N_i}(y_i)=(0,b)$ and $sig_{N_i}(e)=(0,0)$ for the other events. To separate the states of $S(C^b_i)\cup \{t^i_0, s_i\}$ from all the other states we use the region $R_{C_i}=(sup_{C_i}, sig_{C_i})$ where $sup(C_i)(s)=0$, $sig_{C_i}(u_i)=sig_{C_i}(v_i)=(0,b)$ and $sig_{C_i}(e)=(0,0)$ for the other events. Moreover, the states of $S(C^b_i)\cup \{t^i_0, s_i\}$ are pairwise separated by $R_1,R_{k_{2i+1}}$ and $R^\alpha _{X_{i,\alpha }}$, where $X_{i,\alpha } \not \in M$.

Altogether, the set $\mathcal {R}=\mathcal {R}_1\cup \mathcal {R}_2\cup \mathcal {R}_3\cup \mathcal {R}_4$ where $\mathcal {R}_1=\{R_1,R_2,R_3,R_4\}$, $\mathcal {R}_2= \{R^z_{k_{2i}}, R^z_{k_{2i+1}}, R^\alpha _{k_{2i}}, R_{k_{2i+1}}\mid i\in \{0,\dots ,m-1 \},\alpha \in \{0,1,2\}, X_{i,\alpha }\not \in M\}$, $\mathcal {R}_3= \{R_{X_{i,\alpha }} \mid i\in \{0,\dots ,m-1 \},\alpha \in \{0,1,2\}\}$ and $\mathcal {R}_3= \{R_Q, R_{M_{i}}, R_{N_{i}}, R_{C_i}\mid i\in \{0,\dots , m-1\} \}$, is an admissible set of $A^b_\varphi$. We briefly argue that it is FA: It is easy to see that every presented region $R\in \mathcal {R}$ satisfy $\vert R^{\bullet } \vert \le 1$. Moreover, $\vert \,^{\!\bullet }e_{\mathcal {R}} \vert \le 1$ is also true for $e\in E(A^b_\varphi )$: The regions $R_1\in \,^{\!\bullet }o$, $R_2\in \,^{\!\bullet }k$, $R_3\in \,^{\!\bullet }z$ and $R^z_{k_{2i}}\in \,^{\!\bullet }k_{2i}$ and $R^z_{k_{2i+1}}\in \,^{\!\bullet }k_{2i+1}$ are unique. Furthermore, if $X_{i,\alpha }=X_{j,\beta }=X_{\ell ,\gamma }$ then $R_{X_{i,\alpha }}=R_{X_{j,\beta }}=R_{X_{\ell ,\gamma }}$ where $i,j,\ell \in \{0,\dots , m-1\}, \alpha , \beta , \gamma \in \{0,1,2\}$. As $\mathcal {R}$ is a set, this region is the only element in $\,^{\!\bullet }X_{i,\alpha }$. No other region $(sup, sig)\in \mathcal {R}$ satisfies $sig^-(e)>0$ for any $e\in E(A^b_\varphi )$. Thus, $A^b_\varphi$ satisfies Condition 1.2.

To prove Condition 2.2 we provide a b-admissible set $\mathcal {R}$ of pure regions of $B^b_\varphi$ such that $\vert e_\mathcal {R}\! ^{\bullet } \vert \le 2$ and $\vert \,^{\!\bullet }e_{\mathcal {R} } \vert \le 2$ for all $e\in E(B^b_\varphi )$. For brevity, we define for $j\in \{0,\dots , m-1\}$ the following sets: $B_j=\{b^i_j \mid i\in \{0,\dots , m-1\}\}$, $D_j=\{d^i_j \mid i\in \{0,\dots , m-1\}\}$, $U_j=\{u^i_j \mid i\in \{0,\dots , m-1\}\}$, $V_j=\{v^i_j \mid i\in \{0,\dots , m-1\}\}$, $W_j=\{w^i_j \mid i\in \{0,\dots , m-1\}\}$, $Y_j=\{y^i_j \mid i\in \{0,\dots , m-1\}\}$, $K=\{k_i \mid i\in \{0,\dots , 2m-1\} \}$ and $Z=\{z_i \mid i\in \{0,\dots , 2m-1\}\}$. By a little abuse of notation, we let $\mathcal {C}_i=F^b_i\cup G^b_i\cup M^b_i\cup N^b_i\cup F^b_i\cup C^b_i \cup L_{i,0}\cup L_{i,1}$ and $\delta _i=2m+5-i$. Table 2 (below) defines a regions R of $B^b_\varphi$ with $sup_R(s)= 0$.

Table 2. Pure b-regions of $B^b_\varphi$ that solve several separation atoms.

(k), (o): The regions $R_1$ and $R_2$ solve k and the regions $R_1$ and $R_3$ solve o. $(z_{2i}), (z_{2i+1})$: The region $R_2$ solves $z_{2i}, z_{2i+1}$ at k’s sources and $R_3$ solves them at o’s sources, at $s_{i,1}, s_{i,2}, s_{i,3}$ and at $r_{i,1}, r_{i,2}, r_{i,3}$. $R^2_{2i}$ solves $z_{2i}$ at the remaining states of $\mathcal {C}_i\setminus \{t^i_0\}$ and $R_{z_{2i}}$ solves $z_{2i}$ at the remaining states of $B^b_\varphi$. $R^0_{z_{2i+1}}$ solves $z_{2i+1}$ at $n^i_0, n^i_1$ and $s_{i,1}$ and $R^1_{z_{2i+1}}$ solves it at the remaining states.

$(k_{2i})$: For a correct referencing, we need the following definitions: If $j\in \{0,\dots , m-1\}$ then let $\alpha _j\in \{0,1,2\}$ be the index such that $X_{j,\alpha _j}\in M$ and let by $\beta _j < \gamma _j\in \{0,1,2\}\setminus \{\alpha _j\}$ the other variable events of $C^b_j$ be chosen. Moreover, let $\ell \not =j\in \{0,\dots , m-1\}$ such that $X_{i,\beta _i}\in C_i\cap C_\ell , \cap C_j$ and let $\ell ' \not =j'\in \{0,\dots , m-1\}$ such that $X_{i,\gamma _i}\in C_i\cap C_{\ell '}, \cap C_{j'}$. That is, $\ell ,j$ and $\ell ',j'$ choose the other two clauses where $X_{i,\beta _i}, X_{i,\gamma _i}$ occur. We use this to define the region $R^0_{2i}=(sup^0_{2i}, sig^0_{2i})$ where $sup^0_{2i}(s)=0$, $sig(X_{i,\beta _i})=(1,0)$ and for $\delta \in \{i,\ell , j\}$ it is $sig^0_{2i}(k_{2\delta })=(b,0)$ and $sig^0_{2i}(w^\delta _0)=(0,b)$ if $X_{i,\beta _i}=X_{\delta , \beta _\delta }$ and $sig^0_{2i}(w^\delta _2)=(0,b)$ if $X_{i,\beta _i}=X_{\delta , \gamma _\delta }$. Similarly, we define the region $R^1_{2i}=(sup^1_{2i}, sig^1_{2i})$ by $sup^1_{2i}(s)=0$, $sig(X_{i,\gamma _i})=(1,0)$ and for $\delta \in \{i,\ell ', j'\}$ it is $sig^1_{2i}(k_{2\delta })=(b,0)$ and $sig^1_{2i}(w_{\delta ,2})=(0,b)$ if $X_{i,\gamma _i}=X_{\delta , \gamma _\delta }$ and $sig^1_{2i}(w_{\delta ,0})=(0,b)$ if if $X_{i,\gamma _i}=X_{\delta , \beta _\delta }$. Notice that if $X_{i,\beta _i}=X_{\delta ,\gamma _\delta }$ then $R^0_{2i}= R^1_{2\delta }$ and if $X_{i,\gamma _i}=X_{\delta ,\beta _\delta }$ then $R^1_{2i}= R^0_{2\delta }$. This is our way to correctly, restrict the postset of the events $w^{\cdots }_0$ and $w^{\cdots }_2$. The region $R_1$ solves $k_{2i}$ at $m^i_0$ and the sinks of $X_{i,\alpha _i}$. $R^0_{2i}$ and $R^1_{2i}$ solve $k_{2i}$ at all states of $C^b_i \cup \{s\}$ and $\bigcup _{j=1}^{2m+5}\{q^\ell _j, p^\ell _j, a^\ell _j, c^\ell _j, r^\ell _j, s^\ell _j \mid \ell \in \{0,\dots , m-1\}\setminus \{i\}\}$. Finally, to solve $k_{2i}$ at the remaining states we use the region $R^2_{2i}$defined as follows: If $\alpha = 2m+5-i$ then $R^2_{2i}=(sup^2_{2i}, sig^2_{2i})$ is defined by $sup^2_{2i}(s)=0$, $sig^2_{2i}(k_{2i})=sig^2_{2i}(b_{i,0})=sig^2_{2i}(e)$, where $e \in \{v_{j,\alpha }, u_{j,\alpha }, b_{j,\alpha }, d_{j,\alpha }, w_{j,\alpha }, y_{j,\alpha }\mid j\in \{\ 0,\dots ,m-1\} \setminus \{ i \} \}$ and $sig^2_{2i}(z_{2i})=(b,0)$.

$(k_{2i+1})$: $R_1$ and $R_{k_{2i+1}}$ solve $k_{2i+1}$ at all states of $B^b_\varphi$.

$(X_{i,0},X_{i,1}, X_{i,2})$: Let $\alpha _i,\beta _i,\gamma _i$ be defined as above. To separate $X_{i,\alpha _i}=X_{\ell ,\alpha _\ell }=X_{j,\alpha _j}$, $i,j,\ell$ pairwise distinct, from $q^i_1, q^i_2, q^\ell _1, q^\ell _2, q^j_1, q^j_2$, respectively, we use the region $R^i_q=R^\ell _q=R^j_q$ that maps s to 0, $X_{i,\alpha _1}$ to (0, b), $v^i_0, v^\ell _0, v^j_0$ to (b, 0), $v^i_2, v^\ell _2, v^j_2$ to (0, b) and the other events to (0, 0). This region is necessary as the presets $\,^{\!\bullet }v^i_0, \,^{\!\bullet }v^\ell _0, \,^{\!\bullet }v^j_0$ have already two elements. To separate $X_{i,\alpha _i}$ from the remaining states, we use $R^i_{\alpha _i}=(sup^i_{\alpha _i}, sig^i_{\alpha _i})$, where $sup^i_{\alpha _i}(s)=0$, $sig^i_{\alpha _i}(X_{i\alpha _i})=(1,0)$ $sig^i_{\alpha _i}(v^i_1)=sig^i_{\alpha _i}(v^\ell _1)=sig^i_{\alpha _i}(v^j_1)=(0,b)$ and $X_{i,\alpha _i}\in C_i\cap C_\ell \cap C_j$.

The regions $R^i_{\beta _i}$ for $X_{i,\beta _i}$ and $R^i_{\gamma _i}$ for $X_{i,\gamma _i}$ are defined accordingly, where we use $v^{\dots }_3$ and $v^{\dots }_4$ (without repetition or confusion) as preset events, respectively. Notice that, so far, $X_{i,\beta _i}, X_{i,\gamma _i}$ are already separated from $q_1,\dots , q_{2m+5}$ by $R^0_{2i}$ and $R^1_{2i}$, respectively.

$(u^i_j, v^i_j, b^i_j, d^i_j, w^i_j, y^i_j, j\in \{1,\dots ,2m-5\})$: So far, for all of these events e holds $\vert \,^{\!\bullet }e_{\mathcal {R}} \vert =0$ and, even more, if $j\not =1$ then $\vert e_{\mathcal {R}}\!^{\bullet } \vert \le 1$. Hence, for $e,e'\in \{ u^i_j, v^i_j, b^i_j, d^i_j, w^i_j, y^i_j, j\in \{1,\dots ,2m-4\}\}$ with we use the region $(sup_e, sig_e)$ where $sup_e(s)=0$, $sig_e(e')=(0,b)$ and $sig_e(e)=(b,0)$ and $sig_e(e'')=(0,0)$ for $E(B^b_\varphi )\setminus \{e,e'\}$. Notice that $e,e'$ are unique and that this region also separates x. For the $2m+5$-indexed events we use the region where all these (and only these) events are mapped to (b, 0) and s is mapped to b.

So far, the presented regions justify $B^b_\varphi$’s b-ESSP. It remains to justify its b-SSP: One verifies that all distinct states $s,s'\in \mathcal {C}_i$ are separated by the already presented regions. If $e\in \{u^i_j, v^i_j, b^i_j, d^i_j, w^i_j, y^i_j \mid i\in \{0,\dots , m-1\}, j\in \{1,\dots ,2m-5\}\}$ and then s is separated by the region defined for the separation of e. Moreover, so far, if $e\in \{u^i_j, v^i_j, b^i_j, d^i_j, w^i_j, y^i_j \mid i\in \{0,\dots , m-1\}, j\in \{m, \dots ,2m+6\}\}$ then $\vert e_{\mathcal {R}}\!^{\bullet } \vert \ =1$. Hence, we choose for every $i\in \{0,\dots , m-1\}$ the region $R_{\mathcal {C}_i}=(sup_{\mathcal {C}_i}, sig_{\mathcal {C}_i})$ where $sup_{\mathcal {C}_i}(s)=0$, $sig_{\mathcal {C}_i}(e)=(0,b)$ if $e\in \{ u^i_j, v^i_j, b^i_j, d^i_j, w^i_j, y^i_j \mid j= 2m+5-i\} \}$ and, otherwise, $sig_{\mathcal {C}_i}(e)=(0,0)$. Clearly, $R_{\mathcal {C}_i}$ separates the remaining states in question from $S(B^b_\varphi )\setminus \mathcal {C}_i$. Moreover, the regions $R_{\mathcal {C}_0},\dots , R_{\mathcal {C}_{m-1}}$ preserve the (2, 2)-S-system property.

Altogether, the union of all introduced regions yields a b-admissible set $\mathcal {R}$ of pure regions that has the (2, 2)-S-system property.

3.3 The Proof of Theorem 1.4

By Lemma 1, a b-net N, being a weighted (m, n)-T-system, solves A if and only if there is a b-admissible set $\mathcal {R}$ with $N=N^{\mathcal {R}}_A$. By definition, every $R=(sup, sig)\in \mathcal {R}$ satisfies $\vert \,^{\!\bullet }R \vert = \vert \{ e\in E(A) \mid sig^+(e)>0 \} \vert \le m$ and $\vert R^{\bullet } \vert =\vert \{ e\in E(A) \mid sig^-(e)>0 \} \vert \le n$. The maximum set $\mathcal {R}$ of $A'$s b-regions that satisfy the (m, n)-condition is computable in polynomial time: To define $R=(sup, sig)\in \mathcal {R}$ we have for $\ell \in \{1,\dots , m\}$ and $\ell '\in \{1,\dots , n\}$ at most $\left( {\begin{array}{c}\vert E\vert \\ \ell \end{array}}\right)$ and $\left( {\begin{array}{c}\vert E\vert \\ \ell '\end{array}}\right)$ events for $\,^{\!\bullet }R$ and $R^{\bullet }$, respectively. This makes at most $\left( {\begin{array}{c}\vert E\vert \\ \ell \end{array}}\right) \cdot \left( {\begin{array}{c}\vert E\vert \\ \ell '\end{array}}\right) \cdot (b+1)^{\ell +\ell '}$ possibilities for sig, each of it is to combine with the at most $b+1$ values for $sup(s_0)$. As b, m and n are not part of the input, altogether, there are at most $\mathcal {O}(\vert E\vert ^{m+n})$ b-regions. Moreover, one can decide in polynomial time if $sup(s_0)$ and sig define actually a fitting b-region as follows: Firstly, compute a spanning tree $A'$ of A, having at most $\vert S(A)\vert$ paths, in time $\mathcal {O}(\vert E(A)\vert \cdot \vert S(A)\vert ^3)$ [16]. Secondly, use $sup(s_0)$ and sig to determine $sup(s_j)$ for all $s_j\in S(A)$ by the unique path . Thirdly, check for the at most $\vert S\vert ^2 \cdot \vert E\vert$ edges if both $sup(s)\ge sig^-(e)$ and $sup(s')=sup(s)+sig^-(e)+sig^+(e)\le b$ are satisfied.

Having computed the (maximum) set $\mathcal {R}$, it remains to check (in polynomial time) whether the at most $\vert S\vert ^2 + \vert S\vert \cdot \vert E\vert$ separation atoms of A are solved by $\mathcal {R}$.

4 Conclusion

This paper shows that deciding if a TS is solvable by a b-net which is CF, FA, FC, EFC or AC remains NP-complete. Moreover, our proof imply that synthesis is also hard if the searched net is to be behaviorally free choice, behaviorally asymmetric choice or reducedly asymmetric choice [3]. Furthermore, we show that synthesis of (m, n)-S-systems is NP-complete for every fixed $m,n\ge 2$. While synthesis of weighted (m, n)-T-systems, being dual to the S-systems, is also hard if m, n are part of the input, it becomes tractable for any fixed m, n. In particular, fixing m, n puts the problem into the complexity class XP. Consequently, for future work, it remains to be investigated whether the synthesis of weighted (m, n)-T-systems parameterized by $m+n$ is fixed parameter tractable.