Fixed Parameter Tractability and Polynomial Time Results for the Synthesis of b-bounded Petri Nets

Abstract

Synthesis for a type of Petri nets is the problem of finding, for a given transition system (TS, for short) A, a Petri net N of this type whose state graph is isomorphic to A if such a net exists. The decision version of this search problem, called -feasibility, asks if, for a given TS A, there exists a Petri net N of type with a state graph isomorphic to A. In this case, A is called -feasible. A’s feasibility is equivalent to fulfilling two so-called separation properties. In fact, a transition system A is -feasible if and only if it satisfies the type related state separation property (SSP) and event state separation property (ESSP). Both properties, SSP and ESSP, define decision problems. In this paper, we introduce for $b\in \mathbb {N}$ the type of restricted $\mathbb {Z}_{b+1}$-extended b-bounded P/T-nets and show that synthesis and deciding ESSP and SSP for this type is doable in polynomial time. Moreover, we demonstrate that, given a TS A, deciding if A has the SSP can be done in polynomial time for the types of (pure) $\mathbb {Z}_{b+1}$-extended b-bounded P/T-nets. Finally, we exhibit that deciding if a TS A is feasible or has the ESSP for the types of (pure) $\mathbb {Z}_{b+1}$-extended b-bounded P/T-nets is fixed parameter tractable if the number of occurrences of events is considered as parameter.

1 Introduction

Synthesis for a Petri net type (-synthesis, for short) is the task to find for a transition system A a Petri net N of type (-net, for short) with a state graph isomorphic to A. The associated decision version, which we call feasibility for (-feasibility, for short), asks whether there is a corresponding -net for the input A. If such a net exists then we call A -feasible. A’s feasibility is equivalent to fulfilling two so-called separation properties. More exactly, A is -feasible if and only if it has the state separation property and the event state separation property for (-SSP and -ESSP, for short) [5]. Both, -SSP and -ESSP, define decision problems asking whether the input A has the -SSP or the -ESSP, respectively.

Petri net synthesis has been investigated for many years and is applied in numerous fields. It yields implementations which are correct by design and allows extracting concurrency and distributability information from sequential specifications as transition systems and languages [6, 7]. Further application areas of Petri net synthesis currently cover, among others, the reconstruction of a model from its execution traces (process discovery), supervisory control for discrete event systems and the synthesis of speed-independent circuits [1, 9, 13].

A type of Petri nets is called bounded if there is a positive integer b which is not exceeded by the number of tokens on any place in every reachable marking. This paper deals with the computational complexity of synthesis, feasibility, SSP and ESSP for b-bounded Petri net types, that is, bounded Petri nets where b is predetermined.

In [3, 5], Badouel et al. showed that Synthesis, feasibility, SSP and ESSP for the type of bounded and pure bounded place/transition nets (P/T-nets, for short) are solvable in polynomial time if no bound b is preselected. On the contrary, SSP, ESSP and feasibility are NP-complete for pure 1-bounded P/T-nets [4, 12]. This remains true even for strongly restricted input transition systems [19, 21]. In [18], we showed that feasibility, SSP and ESSP are NP-complete for (pure) b-bounded P/T-nets for arbitrary $b\in \mathbb {N}^+$.

In [16], Schmitt advanced the pure 1-bounded P/T-net type by an interaction between places and transitions simulating addition of integers modulo 2. This brings the complexity of synthesis, feasibility, ESSP and SSP for the resulting pure $\mathbb {Z}_2$-extended 1-bounded P/T-nets down to polynomial time. On the contrary, we proved in [18] that extending (pure) b-bounded P/T-nets by $\mathbb {Z}_{b+1}$ yields no tractable type if $b\ge 2$. In particular, feasibility and ESSP for (pure) $\mathbb {Z}_{b+1}$-extended b-bounded P/T-nets, $b\ge 2$, are NP-complete. We continued research on the impact of interactions on the computational complexity of synthesizing 1-bounded Petri nets in [20]. Here, we investigated 43 1-bounded types purely defined by interactions which they have or not. While for 37 of them synthesis is tractable, feasibility and ESSP for the remaining 7 are NP-complete.

Results of [2, 8] show that putting restrictions on the sought nets’s (syntactical) structure can have a positive impact on the complexity of synthesis. In particular, in [2], Agostini et al. proposed a polynomial time synthesis algorithm for Free-Choice Acyclic pure 1-bounded P/T-nets having applications in workflow models. Moreover, in [8], Best et al. showed that it suffices to check certain structural properties of the input A if the sought net is a pure b-bounded live marked graph. Whether A has these properties or not is decidable in polynomial time [14].

In this paper, we examine whether there are also types of b-bounded P/T-nets for which synthesis is tractable if $b\ge 2$. We affirm this question and propose the restricted $\mathbb {Z}_{b+1}$-extended b-bounded P/T-nets, $b\in \mathbb {N}$. This paper shows, that synthesis, feasibility, ESSP and SSP are solvable in polynomial time for this type. Moreover, our results prove that deciding whether a transition system (TS, for short) A has the SSP for the types of (pure) $\mathbb {Z}_{b+1}$-extended b-bounded P/T-nets, $b\in \mathbb {N}$, is also doable in polynomial time. Notice, that this discovers the first Petri net type where the provable computational complexity of SSP is different to ESSP and feasibility.

To decide whether a TS A is -feasible or has the -ESSP, where corresponds to (pure) $\mathbb {Z}_{b+1}$-extended b-bounded P/T-nets, $b\ge 2$, is NP-complete [18]. Hence, this problem is considered inherently hard to solve algorithmically. Consequently, one expects that every corresponding decision algorithm has an exponential running time if complexity is measured in terms of the input size of A only. In this paper, we analyze the computational complexity of feasibility and ESSP for these types in finer detail. To do so, we apply parameterization, a typical approach of modern complexity theory to tackle hard problems. The running time of parameterized algorithms is not only expressed in the input’s size, but it also takes the parameters into account. The number k of occurrences of events, the maximum number of different transitions at which an event occur, is one of the most obvious parts of a TS which can be considered as a parameter. We show that feasibility and ESSP related to the types of (pure) $\mathbb {Z}_{b+1}$-extended b-bounded P/T-nets are only exponential in the size of k while polynomial in the size of the input. Hence, both problems are fixed parameter tractable if k is considered as parameter. This result could not be foreseen with certainty. In fact, in [19], we showed that feasibility, ESSP and SSP remain NP-complete for pure 1-bounded P/T-nets even if every event occurs at most twice. Hence, related to pure 1-bounded P/T-nets, these problems parameterized by k are not fixed parameter tractable as long as P $\not =$ NP.

2 Preliminaries

A transition system (TS for short) $A = (S,E,\delta )$ consists of finite disjoint sets S of states and E of events and a partial transition function $\delta : S\times E\rightarrow S$. Usually, we think of A as an edge-labeled directed graph with node set S where every triple $\delta (s,e)=s'$ is interpreted as an e-labeled edge , called transition. We say that an event e occurs at state s if $\delta (s,e)=s'$ for some state $s'$ and abbreviate this with . 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 and . If $w\in E^*$ then denotes that there is a state $s'\in S$ such that . An initialized TS $A=(S,E,\delta , s_0)$ is a TS with an initial state $s_0 \in S$ where every state is reachable: . The language of A is the set . In the remainder of this paper, if not explicitly stated otherwise, we assume all TSs to be initialized and we refer to the components of an (initialized) TS A consistently by $A=(S_A, E_A, \delta _A, s_{0,A})$.

Fig. 1.

Top: The type . Edges with several labels represent different transitions. Discarding the (1, 1), (1, 2), (2, 1) and (2, 2) labeled transitions yields . Bottom: The type .

The following notion of types of nets has been developed in [5]. It allows us to uniformly capture several Petri-net types in one general scheme. Every introduced Petri-net type can be seen as an instantiation of this general scheme. A type of nets is a TS and a Petri net $N = (P, T, f, M_0)$ of type , -net for short, is given by finite and disjoint sets P of places and T of transitions, an initial marking , and a flow function . The meaning of a -net is to realize a certain behavior by cascades of firing transitions. In particular, a transition $t \in T$ can fire in a marking and thereby produces the marking if for all $p\in P$ the transition exists in . This is denoted by . Again, this notation extends to sequences $\sigma \in T^*$. Accordingly, is the set of all reachable markings of N. Given a -net $N=(P, T, f,M_0)$, its behavior is captured by the TS $A_N=(RS(N), T,\delta , M_0)$, called the state graph of N, where for every reachable marking M of N and transition $t \in T$ with the transition function $\delta$ of $A_N$ is defined by $\delta (M,t) = M'$. The following types of b-bounded P/T-nets and pure b-bounded P/T-nets build the basis of the announced $\mathbb {Z}_{b+1}$-extensions:

• 0. The type of b-bounded P/T-nets is defined by where for and the transition function is defined by if $s\ge m$ and $s-m+n \le b$, and undefined otherwise.

• 1. The type of pure b-bounded P/T-nets is a restriction of -nets that discards all events (m, n) from where both, m and n, are positive. To be exact, , and for and we have .

Having and , their following $\mathbb {Z}_{b+1}$-extension allows them to simulate the addition of integers modulo $b+1$.

• 2. The type of $\mathbb {Z}_{b+1}$-extended b-bounded P/T-nets arises from such that, firstly, extends the event set by the elements $0,\dots , b$ and, secondly, the transition function extends by the addition of integers modulo $b+1$. More exactly, where for and we have that if and if $e \in \{0,\dots , b\}$.

• 3. The type of $\mathbb {Z}_{b+1}$-extended pure b-bounded P/T-nets is defined by where for and the transition function is given by if and if $e\in \{0,\dots , b\}$.

The new Petri net type arises as a restriction of :

• 4. The type of restricted $\mathbb {Z}_{b+1}$-extended b-bounded P/T-nets , $b\in \mathbb {N}^+$, origins from and has the same state set, , and the same event set, , but a restricted transition function . In particular, the transition function restricts in way that for and we have that if $s=m$ and, otherwise, if $s\not =m$ then remains undefined. Hence, every occurs exactly once in . Furthermore, if $(s,e)\in \{0,\dots ,b\}^2$ then .

Fig. 2.

Upper left, top: Input TS A. Bottom: The table depicts the set of -regions $\mathcal {R}=\{R_1,R_2,R_3,R_4,R_5\}$ where $R_i=(sup_i,sig_i)$ for $i\in \{1,\dots , 5\}$. All regions of $\mathcal {R}$ are also -regions and all of $\mathcal {R}\setminus \{R_1\}$ are also -regions. One verifies that $\mathcal {R}$ contains a witness for every ESSP atom and every SSP atom of A. Hence, if then A and the synthesized -net $N^{\mathcal {R}}_A$ has a state graph that is isomorphic to A. However, the set $\{R_2,\dots , R_5\}$ contains no witness for the solvability of (c, 1) and $R_1$ is no -region. The ESSP atom (c, 1) is not -solvable at all, hence, A is not -feasible. Upper right: The graphical representation of the synthesized -net $N^{\mathcal {R}}_A=(\mathcal {R}, \{a,b,c\}, f, 21210)$, where $f(R_i,x)=sig_i(x)$ for every $x\in \{a,b,c\}$ and $M_0(R_1)\cdots M_0(R_5) =sup_1(0)\dots sup_5(0)$. For readability, 0-labeled flow arcs for the representation of $f(R_5,x)=0$ for $x\in \{b,c,d\}$ are neglected and flow arcs to the same place are drawn in the same color. Upper left, bottom: The state graph $A_{N^{\mathcal {R}}_A}$ of $N^{\mathcal {R}}_A$ where the reachable markings (states) are represented by 5-tupels $M(R_1)\cdots M(R_5)$. Obviously, $A_{N^{\mathcal {R}}_A}$ is isomorphic to A.

In the remainder of this paper we assume and $b\in \mathbb {N}^+$, unless stated otherwise. Notice, that coincides with Schmitt’s type [16]. Figure 1 gives a graphical representation of and . The following notion of -regions allows us, on the one hand, to define the type related ESSP and SSP and, on the other hand, to reveal in which way we are able to obtain a -net N for a given TS A if it exists. Figure 2 shows examples of all subsequently introduced terms.

If is a type of nets then a -region of a TS A is a pair of mappings (sup, sig), where and , such that, for each transition of A, we have that is a transition of . If (sup, sig) is a -region of A then for $e\in E_A$ we define $sig^-(e)=m$, $sig^+(e)=n$ and $\vert sig(e)\vert =0$ if and, otherwise, $sig^-(e)=sig^+(e)=0$ and $\vert sig(e)\vert = sig(e)$ if $sig(e)\in \{0,\dots , b\}$. Hence, by definition of , (sup, sig) is a -region if and only if entails $sup(s')=(sup(s)-sig^-(e)+sig^+(e)+\vert sig(e)\vert )\text { mod } (b+1)$.

Two distinct states $s,s'\in S_A$ define an SSP atom $(s,s')$, which is said to be -solvable if there is a -region (sup, sig) of A such that $sup(s)\not =sup(s')$. An event $e\in E_A$ and a state $s\in S_A$ at which e does not occur, that is , define an ESSP atom (e, s). The atom is said to be -solvable if there is a -region (sup, sig) of A such that . A -region solving an ESSP or a SSP atom (x, y) is a witness for the -solvability of (x, y). A TS A has the -ESSP (-SSP) if all its ESSP (SSP) atoms are -solvable. Naturally, A is said to be -feasible if it has the -ESSP and the -SSP.

The following fact is well known from [5, p. 161]: A set $\mathcal {R}$ of -regions of A contains a witness for all ESSP and SSP atoms if and only if the synthesized -net $N^{\mathcal {R}}_A=(\mathcal {R} , E_A, f, M_0)$ has a state graph that is isomorphic to A. The flow function of $N^{\mathcal {R}}_A$ is defined by $f((sup, sig), e)= sig(e)$ and its initial marking is $M_0((sup,sig))=sup(s_{0,A})$ for all $(sup, sig) \in \mathcal {R}, e\in E_A$. The regions of $\mathcal {R}$ become places and the events of $E_A$ become transitions of $N^{\mathcal {R}}_A$. Hence, for a -feasible TS A where $\mathcal {R}$ is known, we can synthesize a net N with state graph isomorphic to A by constructing $N^{\mathcal {R}}_A$.

3 Polynomial Time Results

Theorem 1

Solving -synthesis for a TS A or deciding if A has the -ESSP is doable in polynomial time. Moreover, for one can decide in polynomial time whether a given TS A has the -SSP.

The contribution of Theorem 1 is threefold. Firstly, in [18] it has been shown that deciding the -ESSP and -feasibility is a NP-complete problem for . Hence, by showing that deciding the -SSP for is doable in polynomial time, Theorem 1 discovers the first Petri net types where the provable computational complexity of SSP is different to ESSP and feasibility.

In [16], Schmitt advanced pure 1-bounded P/T-nets by the additive group of integers modulo 2 and discovered a tractable superclass. In [18], we showed that lifting this approach to (pure) b-bounded P/T-nets where $b\ge 2$ do not lead to superclasses with a tractable synthesis problem. Thus, Theorem 1 proposes the first tractable type of b-bounded Petri nets, $b\ge 2$, so far. Finally, Theorem 1 gives us insight into which of the -net properties, , cause the synthesis’ hardness. In particular, flow arc relations (events in ) between places and transitions in a -net define conditions when a transition is able to fire. For example, if N is a -net with transition t and place p such that $f(p,t)=(1,0)$ then the firing of t in a marking M requires $M(p)\ge 1$. By Theorem 1, the hardness of finding a -net N for A origins from the potential possibility of -nets to satisfy such conditions by multiple markings $M(p)\in \{1,\dots ,b\}$. In fact, the definition of implies that $f(p,t)=(m,n)$ requires $M(p)=m$ for the firing of t and prohibits the possibility of multiple choices. By Theorem 1, this makes -synthesis tractable. It should be noted that the results of [4, 12] show that the restriction to “unambiguous markings” of p satisfying conditions defined by f(p, t) does not guarantee tractability.

While the question of whether there are superclasses of , $b\ge 2$, for which synthesis is doable in polynomial time remains unanswered, the following lemma shows that the type yields at least a tractable superclasses of Schmitt’s type [16]. In particular, if $b < b'$ then the class of -nets is strictly more comprehensive than the class of -nets.

Lemma 1

If $b < b'\in \mathbb {N}^+$ and if $\mathcal {T}$ is the set of -feasible TSs and $\mathcal {T'}$ the set of -feasible TSs then $\mathcal {T }\subset \mathcal {T'}$.

Proof

To proof the lemma, we consider a TS A which is -feasible but not -feasible. Let A defined by $A=(\{s_0,\dots , s_{b'}\},\{a\},\delta , s_0)$ the TS with transition function $\delta (s_i, a)=s_{i+1}$ for $i\in \{0,\dots , b'-1\}$ and $\delta (s_{b'},a)=s_0$. By other words, A is a directed labeled cycle where every transition is labeled by a. Notice, that A has no ESSP atom and, hence, the -ESSP for every type of nets. Consequently, A is -feasible if and only if it has the -SSP.

Assume, for a contradiction, that A is -feasible. By $b <b'$, A provides the SSP atom $(s_0, s_{b+1})$ and A’s -feasibility implies that there is a -region (sup, sig) solving it. If $sig(a)=(m,n)$ then $sup(s_1)=sup(s_0)-m+n\not =sup(s_0)$ and, by definition of , . This is a contradiction to . Hence, $sig(a)\in \{1,\dots , b\}$. By induction, $sup(s_{b+1})=sup(s_0) + (b+1)\cdot sig(a) = sup(s_0) \text { mod } (b+1)$ implying $sup(s_{b+1})=sup(s_0)$. Thus, (sup, sig) does not solve $(s_0, s_{b+1})$, which proves that A not to be -feasible.

On the contrary, it is easy to see that the -region (sup, sig), which is defined by $sup(s_0)=0$, $sig(e)=1$ and $sup(s_{i+1})=sup(s_i)+ sig(a)$ for $i\in \{0,\dots , b'-1\}$, solves every SSP atom of A. Hence, A is -feasible.    $\square$

3.1 Abstract Regions and Fundamental Cycles

Unless otherwise stated, in the remainder of this paper we assume that A is a (non-trivial) TS with at least two states, $\vert S_A\vert \ge 2$ and event set $E_A=\{ e_1,\dots , e_n \}$. Recall that and $b\in \mathbb {N}^+$.

The proof of Theorem 1 bases on a generalization of the approach used in [16] that reduces ESSP and SSP to systems of linear equations modulo $b+1$. It exploits that the solvability of such systems is decidable in polynomial time which is the statement of the following lemma borrowed from [11]:

Lemma 2

([11]). If $A \in \mathbb {Z}^{k \times n}_{b+1}$ and $c\in \mathbb {Z}^k_{b+1}$ then deciding if there is an element $x\in \mathbb {Z}^n_{b+1}$ such that $Ax=c$ is doable in time $\mathcal {O}(nk\cdot max\{n,k\})$.

Essentially, our generalization composes for every ESSP atom and every SSP atom $\alpha =(x,y)$ of A, respectively, a system of equations modulo $b+1$ which is solvable if and only if $\alpha$ is -solvable. Moreover, a solution of the corresponding system shall provide a -region of A that solves $\alpha$. On the one hand, this approach ensures that having a solution for every system defined by single ESSP atoms and SSP atoms implies the -ESSP and -SSP for A, respectively. On the other hand, it provides a -solving region for every atom in question and, hence, a set $\mathcal {R}$ of -regions that witnesses the -ESSP and -SSP of A. Thus, $\mathcal {R}$ allows us to construct the synthesized net $N^\mathcal {R}_A$ with a state graph isomorphic to A. In the following, we establish the notions of abstract regions and fundamental cycles which make such a translation possible.

We proceed by deducing the notion of abstract regions. Our starting point is the goal to obtain regions (sup, sig) of A as solutions of linear equation systems modulo $b + 1$. By definition, (sup, sig) is a -region of A if and only if for every transition it is true that

$$\begin{aligned} sup(s')=(sup(s)-sig^-(e)+sig^+(e)+\vert sig(e) \vert ) \text { mod } (b+1) \end{aligned}$$

(1)

Hence, installing for every transition the corresponding Eq. 1 yields a linear system of equations whose solutions are regions of A. If (sup, sig) is a solution of this system such that for $e\in E_A$ then, by definition, for every transition it has to be true that $m \le sup(s)$ and $sup(s')-m+n\le b$. Unfortunately, the conditions $m \le sup(s)$ and $sup(s')-m+n\le b$ can not be tested in the group $\mathbb {Z}_{b+1}$. To cope with this obstacle, we abstract from elements by restricting to regions (solutions) that identify (m, n) with the unique element $x\in \{0,\dots , b\}$ such that $x= (n-m) \text { mod } (b+1)$. This leads to the notion of abstract -regions. A -region (sup, sig) of A is called abstract if sig’s codomain restricts to $\{0,\dots , b\}$, that is, $sig: E_A\longrightarrow \{0,\dots , b\}$. If (sup, sig) is an abstract region, then we call sig an abstract signature. For the sake of clarity, we denote abstract signatures by abs instead of sig and abstract regions by (sup, abs) instead of (sup, sig).

By definition, two mappings $sup, abs: \{0,\dots , b\} \longrightarrow \{0,\dots , b\}$ define an abstract -region if and only if for every transition of A it is true that

$$\begin{aligned} sup(s')=(sup(s) + abs(e)) \text { mod } (b+1) \end{aligned}$$

(2)

Obviously, for abstract regions Eq. 1 reduces to Eq. 2. Installing for every transition of A its corresponding Eq. 2 yields a system modulo $b+1$ whose solutions are abstract regions. Uncomfortably, such systems require to deal with sup and abs simultaneously. It is better to first obtain abs independently of sup and then define sup with the help of abs. The following observations show how to realize this idea.

By induction and Eq. 2, one immediately obtains that (sup, abs) is an abstract region if and only if for every directed labeled path of A from the initial state $s_{0,A}$ to the state $s_m$ the path equation holds:

$$\begin{aligned} sup(s_m) = (sup(s_{0,A}) + abs(e'_1)+ \dots + abs(e'_m)) \text { mod }(b+1) \end{aligned}$$

(3)

To exploit Eq. 3 we, firstly, identify every abstract signature abs with the unique element $abs=(abs(e_1),\dots , abs(e_n))\in \mathbb {Z}^n_{b+1}$. Secondly, we say that $\psi ^{p}_{b+1}=(\#^p_{e_1},\dots ,\#^p_{e_n})\in \mathbb {Z}^n_{b+1}$ is the Parikh-vector of p that counts the number $\#^p_{e_i}$ of occurrences of every event $e_i\in E_A$ on the path p modulo $(b+1)$. Thirdly, for two elements $v,w\in \mathbb {Z}_{b+1}^n$ we define $v\cdot w = v_1w_1 + \dots + v_nw_n$. As a result, considering p and abs as elements of $\mathbb {Z}^n_{b+1}$ allows us to reformulate the path equation by $sup(s_m)=(sup(s_{0,A}) + \psi ^{p}_{b+1}\cdot abs) \text { mod } (b+1)$. Especially, if $p,p'$ are two different paths from $s_{0,A}$ to $s_m$ then $\psi ^{p}_{b+1}\cdot abs =\psi ^{p'}_{b+1}\cdot abs$. Thus, the support sup is fully determined by $sup(s_{0,A})$ and abs. By the validity of the path equation, every abstract signature abs implies $b+1$ different abstract -regions of A, one for every $sup(s_{0,A})\in \{0,\dots , b\}$. Altogether, we have argued that the challenge of finding abstract regions of A reduces to the task of finding A’s abstract signatures. In the following, we deduce the notion of fundamental cycles defined by chords of a spanning tree of A which enables us to find abstract signatures. For readability, we often write $x=y_1+\dots + y_\ell \mod (b+1)$ instead of $x=(y_1+\dots + y_\ell ) \mod (b+1)$

Fig. 3.

A spanning tree $A'$ of running example TS A introduced in Fig. 2. The unique Parikh vectors $\psi _0,\dots \psi _7$ of $A'$ (written as rows) are given by $\psi _0= (0,0,0,0), \psi _1=(1,0,0,0), \psi _2= (1,1,0,0), \psi _3=(1,1,1,0), \psi _4=(1,1,2,0), \psi _5= (0,0,1,0)$, $\psi _6=(0,0,2,0)$ and $\psi _7=(1,0,2,0)$. The transitions $\delta _A(7,d)=4$, $\delta _A(4,c)=2$ and $\delta _A(6,c)=0$ of A define the chords of $A'$. The corresponding fundamental cycles are given by $\psi _t=\psi _7 +(0,0,0,1) -\psi _4 = (0,2,0,1)$ and $\psi _{t'}= \psi _4 + (0,0,1,0)-\psi _2 =(0,0,0,0)$ and $\psi _{t''}=\psi _6 + (0,0,1,0)-\psi _0 =(0,0,0,0)$. Hence, if $abs=(x_a,x_b,x_c,x_d)$ then $\psi _t\cdot abs= 0\cdot x_a +2\cdot x_b +0\cdot x_c + x_d=2\cdot x_b + x_d$. By $\psi _{t'}\cdot abs = \psi _{t''}\cdot abs =0$ for every map abs, only the equation $2\cdot x_b + x_d=0$ contributes to the basic part of every upcoming system.

A spanning tree $A'$ of A is a sub-transition system $A'=(S_{A}, E_{A}, \delta _{A'}, s_{0,A})$ of A with a restricted transition function $\delta _{A'}$ such that, firstly, $\delta _{A'}(s,e)=s'$ entails $\delta _A(s,e)=s'$ and, secondly, for every $s\in S_{A'}$ there is exactly one path in $A'$. By other words, the underlying undirected graph of $A'$ is a tree in the common graph-theoretical sense. Every transition of A which is not in $A'$ is called a chord (of $A'$). The chords of $A'$ are exactly the edges that induce a cycle in $A'$’s underlying undirected graph. This gives rise to the following notion of fundamental cycles. For $e_i\in \{e_1,\dots , e_n\}$ we define $1_i=(x_1,\dots ,x_n)^t\in \mathbb {Z}^n_{b+1}$, where $x_j=1$ if $j=i$ and, else $x_j=0$. If is a chord of $A'$ then there are unique paths p from $s_{0,A}$ to s and $p'$ from $s_{0,A}$ to $s'$ in $A'$ such that t corresponds to the unique element $\psi _t= \psi ^p_{b+1} + 1_i - \psi ^{p'}_{b+1}\in \mathbb {Z}^n_{b+1}$, called the fundamental cycle of t.

The following lemma teaches us how to use fundamental cycles to generate abstract signatures of A:

Lemma 3

If $A'$ is a spanning tree of a TS A with chords $t_1,\dots , t_k$ then $abs \in \mathbb {Z}^n_{b+1}$ is an abstract signature of A if and only if $\psi _{t_i} \cdot abs = 0$ for all $i\in \{1,\dots , k\}$. Two different spanning trees $A'$ and $A''$ provide equivalent systems of equations.

Proof

We start with proving the first statement. If: Let $abs \in \mathbb {Z}^n_{b+1}$ such that $\psi _{t_i} \cdot abs = 0$ for all $i\in \{1,\dots , k\}$ and $sup(s_{0,A})\in \{0,\dots , b\}$. If $s\in S_{A'}$ then there is a unique path in $A'$ from $s_{0,A}$ to s. By defining $sup(s)=sup(s_{0,A}) + \psi ^p_{b+1} \cdot abs$ we obtain inductively that every transition of $A'$ satisfies $sup(s')=sup(s) + abs(e)$. It remains to prove that this definition is consistent with the remaining transitions of A, the chords of $A'$. Let $t=$ be a chord of $A'$ and let and be the unique paths from $s_{0,A}$ to s and $s'$ in $A'$, respectively. By $sup(s)=sup(s_{0,A}) + \psi ^p_{b+1} \cdot abs$ and $sup(s')=sup(s_{0,A}) + \psi ^{p'}_{b+1} \cdot abs$ we have that

$$\begin{aligned} 0&= \psi _t \cdot abs&\Longleftrightarrow \\ 0&= (-\psi ^{p'}_{b+1} + 1_i + \psi ^p_{b+1} ) \cdot abs&\Longleftrightarrow \\ 0&= -\psi ^{p'}_{b+1} \cdot abs+ abs(e) + \psi ^p_{b+1} \cdot abs&\Longleftrightarrow \\ \psi ^{p'}_{b+1} \cdot abs&= abs(e) + \psi ^p_{b+1} \cdot abs&\Longleftrightarrow \\ sup(s_{0,A}) + \psi ^{p'}_{b+1} \cdot abs&= sup(s_{0,A}) + \psi ^p_{b+1} \cdot abs + abs(e)&\Longleftrightarrow \\ sup(s')&= sup(s) + abs(e)&\end{aligned}$$

where $0 = \psi _t \cdot abs$ is true by assumption. Hence, abs is an abstract signature of A and the proof shows how to get a corresponding abstract region (sup, abs) of A.

Only-if: If abs is an abstract region of A then we have $sup(s') = sup(s) + abs(e)$ for every transition in A. Hence, if $t=$ a chord of a spanning tree $A'$ of A then working backwards the equivalent equalities above proves $\psi _t\cdot abs =0$.

The second statement is implied by the first: If $A'$, $A''$ are two spanning trees of A with fundamental cycles $\psi ^{A'}_{t_1},\dots , \psi ^{A'}_{t_k}$ and $\psi ^{A''}_{t'_1},\dots , \psi ^{A''}_{t'_k}$, respectively, then we have for $abs\in \mathbb {Z}^n_{b+1}$ that $\psi ^{A'}_{t_i}\cdot abs =0 ,i\in \{1,\dots , k\}$ if and only if abs is an abstract signature of A if and only if $\psi ^{A''}_{t'_i}\cdot abs =0 ,i\in \{1,\dots , k\}$.    $\square$

In the following, justified by Lemma 3, we assume $A'$ to be a fixed spanning tree of A with chords $t_1,\dots , t_k$. By $M_{A'}$ we denote the system of equations $\psi _{t_i} \cdot abs = 0$, $i\in \{1,\dots , k\}$. Moreover, by $\psi _s$ we abridge for $s\in S_A$ the Parikh-vector $\psi ^p_{b+1}$ of the unique path in $A'$. A spanning tree of A is computable in polynomial time: As $\delta _A$ is a function, A has at most $\vert E\vert \vert S_A\vert ^2$ transitions and $A'$ contains $\vert S_A\vert -1$ transitions. Thus, by $2 \le \vert S_A\vert$, $A'$ has at most $\vert E\vert \vert S_A\vert ^2 -1$ chords. Consequently, a spanning tree $A'$ of A is computable in time $\mathcal {O}(\vert E\vert \vert S_A \vert ^3)$ [17].

To get polynomial time solvable systems of equations, we have restricted ourselves to equations like Eq. 2. This restriction results in the challenge to compute abstract signatures of A. By Lemma 3, abstract signatures of A are solutions of $M_{A'}$. An (abstract) -region (sup, abs) of A arises from abs by defining $sup(s_{0,A})$ and $sup(s)=sup(s_{0,A})+\psi _s \cdot abs$, $s\in S(A)$. However, if $(s, s')$ is a SSP atom of A then $sup(s)\not =sup(s')$ is not implied. Moreover, by definition, to -solve ESSP atoms (e, s) we need (concrete) -regions (sup, sig) such that . The next section shows how to extend $M_{A'}$ to get -solving regions.

3.2 The Proof of Theorem 1

This section shows how to extend $M_{A'}$ for a given (E)SSP atom $\alpha$ to get a system $M_\alpha$, whose solution yields a region solving $\alpha$ if there is one.

If $\alpha$ is an SSP atom $(s,s')$ then we only need to assure that the (abstract) region (sup, abs) built on a solution of $M_{A'}$ satisfies $sup(s)\not =sup(s')$. By $sup(s)=sup(s_{A,0}) + \psi _s\cdot abs$ and $sup(s')=sup(s_{A,0}) + \psi _{s'}\cdot abs$, it is sufficient to extend $M_{A'}$ in a way that ensures $\psi _s\cdot abs\not = \psi _{s'}\cdot abs$. The next lemma proves this claim.

Lemma 4

If then a -SSP atom $(s,s')$ of A is -solvable if and only if there is an abstract signature abs of A with $\psi _{s}\cdot abs \not = \psi _{s'}\cdot abs$.

Proof

If: If abs is an abstract signature with $\psi _{s}\cdot abs \not = \psi _{s'}\cdot abs$ then the -region (sup, abs) with $sup(s_{0,A})=0$ and $sup(s)=\psi _{s}\cdot abs$ satisfies $sup(s)\not =sup(s')$. Only-if: If (sup, sig) is a -region then we obtain a corresponding abstract -region (sup, abs) as defined in Lemma 6. Clearly, abs is an abstract signature and satisfies the path equations. Consequently, by $sup(s_0)+\psi _{s}\cdot abs= sup(s) \not = sup(s')=sup(s_0)+\psi _{s'}\cdot abs$, we have that $\psi _{s}\cdot abs \not =\psi _{s'}\cdot abs$.    $\square$

The next lemma applies Lemma 4 to get a polynomial time algorithm which decides the -SSP if .

Lemma 5

If then to decide whether a TS A has the -SSP is doable in time $\mathcal {O}(\vert E_A\vert ^3 \cdot \vert S_A \vert ^6\cdot )$.

Proof

If $\alpha =(s,s')$ is a SSP atom of A then the (basic) part $M_{A'}$ of $M_\alpha$ consists of at most $\vert E\vert \cdot \vert S_A\vert ^2 - 1$ equations for the fundamental cycles. To satisfy $\psi _{s}\cdot abs \not = \psi _{s'}\cdot abs$, we add the equation $(\psi _{s}-\psi _{s'})\cdot abs = q$, where initially $q=1$, and get (the first possible) $M_\alpha$. A solution of $M_\alpha$ provides an abstract region satisfying $\psi _{s} \not = \psi _{s'}$. By Lemma 4, this proves the solvability of $\alpha$. If $M_\alpha$ is not solvable then we modify $M_\alpha$ to $M_\alpha '$ simply by incrementing q and try to solve $M_\alpha '$. Either we get a solution or we modify $M_\alpha '$ to $M_\alpha ''$ by incrementing q again. By Lemma 4, if $(s,s')$ is solvable then there is a $q\in \{1,\dots , b\}$ such that the corresponding (modified) system has a solution. Hence, after at most b iterations we can decide whether $(s,s')$ is solvable or not. Consequently, we have to solve at most b linear systems with at most $\vert E_A\vert \cdot \vert S_A\vert ^2$ equations for $(s,s')$. The value b is not part of the input. Thus, by Lemma 2, this is doable in $\mathcal {O}(\vert E_A\vert ^3 \cdot \vert S_A\vert ^4)$ time. We have at most $\vert S_A \vert ^2$ different SSP atoms to solve. Hence, we can decide the -SSP in time $\mathcal {O}(\vert E_A\vert ^3 \cdot \vert S_A\vert ^6)$.    $\square$

As a next step, we let and prove the polynomial time decidability of -ESSP. But before that we need the following lemma that tells us how to obtain abstract regions from (concrete) regions:

Lemma 6

If (sup, sig) is a -region of a TS A then we obtain a corresponding abstract -region (sup, abs) by defining abs for $e\in E_A$ as follows: If $sig(e)=(m,n)$ then $abs(e)=-m+n \text { mod } (b+1)$ and, otherwise, if $sig(e)\in \{0,\dots , b\}$ then $abs(e)=sig(e)$.

Proof

We have to show that in A entails in . If $abs(e)=sig(e)\in \{0,\dots , b\}$ this is true as (sup, sig) is a -region.

If $sig(e)=(m,n)$ then, by definition, we have $sup(s')=sup(s)-m+n \text { mod } (b+1)$ implying $sup(s')-sup(s)= -m+n \text { mod } (b+1)$. By $abs(e)=-m+n \text { mod } (b+1)$ and symmetry, we get $-m+n = abs(e) \text { mod } (b+1)$ and, by transitivity, we obtain $sup(s')-sup(s) = abs(e) \text { mod } (b+1)$ which implies $sup(s')= sup(s) + abs(e) \text { mod } (b+1)$. Thus .    $\square$

Let $\alpha$ be an ESSP atom (e, s) and let $s_1,\dots , s_k$ be the sources of e in A. By definition, a -region (sup, sig) solves $\alpha$ if and only if $sig(e)=(m,n)$ and for a . By definition of , every element occurs at exactly one state in and this state is m. Hence, $sup(s_1)=\dots =sup(s_k)=m$ and $sup(s)\not =m$. We base the following lemma on this simple observation. It provides necessary and sufficient conditions that an abstract region must fulfill to imply a solving (concrete) region.

Lemma 7

Let and A be a TS and let be the e-labeled transitions in A, that is, if $s'\in S_A\setminus \{s_1,\dots , s_k\}$ then . The atom (e, s) is -solvable if and only if there is an event and an abstract region (sup, abs) of A such that the following conditions are satisfied:

• 1. $abs(e) = -m+n \text { mod } (b+1)$,

• 2. $\psi _{s_1}\cdot abs = m - sup(s_{A,0}) \text { mod } (b+1)$,

• 3. $(\psi _{s_1}-\psi _{s_i})\cdot abs = 0 \text { mod } (b+1)$ for $i\in \{2,\dots , k\}$,

• 4. $(\psi _{s_1}-\psi _s)\cdot abs \not = 0 \text { mod } (b+1)$.

Proof

If: Let (sup, abs) be an abstract region that satisfies the conditions 1–4. We obtain a -solving region (sup, sig) with (the same support and) the signature sig defined by $sig(e')=abs(e')$ if $e'\not =e$ and $sig(e')=(m, n)$ if $e'=e$. To argue that (sup, sig) is a -region we have to argue that in A implies . As (sup, abs) is an abstract region this is already clear for transitions where $e'\not =e$. Moreover, (sup, abs) satisfies $\psi _{s_1}\cdot abs = m - sup(s_{A,0}) \text { mod } (b+1)$ and the path equation holds, that is, $sup(s_1)=sup(s_{A,0}) + \psi _{s_1}\cdot abs \text { mod } (b+1)$ which implies $sup(s_1)=m$. Consequently, by definition of , we have in . Furthermore, by $abs(e)= -m+n \text { mod } (b+1)$ we have $m+abs(e) = n\text { mod } (b+1)$. Hence, by , we conclude $sup(s'_1)=n$ and, thus, . By $(\psi _{s_1}-\psi _{s_i})\cdot abs = 0 \text { mod } (b+1)$ for $i\in \{2,\dots , k\}$, we obtain that $sup(s_1)=\dots =sup(s_k)=m$. Therefore, similar to the discussion for , we obtain by that the transitions are present in for $i\in \{2,\dots , k\}$. Consequently, (sup, sig) is a -region.

Finally, by $(\psi _{s_1}-\psi _s)\cdot abs \not = 0 \text { mod } (b+1)$, have that $sup(s_1)\not =sup(s)$ and, thus, . This proves (e, s) to be -solvable by (sup, sig).

Only-if: Let (sup, sig) be a -region that solves (e, s) implying, by definition, . We use (sup, sig) to define a corresponding abstract -region (sup, abs) in accordance to Lemma 6. If $sig(e)\in \{0,\dots ,b\}$ then , a contradiction. Hence, it is such that for $i\in \{1,\dots , k\}$ and . This immediately implies $sup(s)\not =sup(s_1)$ and, hence, $(\psi _{s_1}-\psi _s)\cdot abs \not = 0 \text { mod } (b+1)$. By and definition of , we have that $sup(s_i)=m$ and $sup(s'_i)=n$ for $i\in \{1,\dots , k\}$ implying $(\psi _{s_1}-\psi _{s_i})\cdot abs = 0 \text { mod } (b+1)$ for $i\in \{2,\dots , k\}$. Moreover, by we have $abs(e) = sup(s'_1)-sup(s_1)\text { mod } (b+1)$. Hence, it is $abs(e)= -m+n \text { mod } (b+1)$. Finally, by the path equation, we have $sup(s_1)=sup(s_{A,0})+\psi _{s_1}\cdot abs \text { mod } (b+1)$ which with $sup(s_1)=m$ implies $\psi _{s_1}\cdot abs = m - sup(s_{A,0})\text { mod } (b+1)$. This proves the lemma.    $\square$

The next lemma’s proof exhibits a polynomial time decision algorithm for the -ESSP: Given a TS A and a corresponding ESSP atom $\alpha$, the system $M_{A'}$ is extended to a system $M_\alpha$. If $M_\alpha$ has a solution abs then it implies a region (sup, abs) satisfying the conditions of Lemma 9. By Lemma 9, this implies $\alpha$’s solvability. Reversely, by Lemma 9, if $\alpha$ is solvable then there is an abstract region (sup, abs) which satisfies the conditions (1–4). The abstract signature abs is the solution of a corresponding equation system $M_\alpha$. Hence, we get a solvable $M_\alpha$ if and only if $\alpha$ is solvable. We argue that the number of possible systems is bounded polynomially in the size of A. The solvability of every system is also decidable in polynomial time. Consequently, by the at most $\vert E_A\vert \cdot \vert S_A\vert$ ESSP atoms to solve, this yields the announced decision procedure.

Lemma 8

If a TS A has the -ESSP is decidable in time $\mathcal {O}(\vert E_A\vert ^4\cdot \vert S_A\vert ^5)$.

Proof

To estimate the computational complexity of deciding the -ESSP for A observe that A has at most $\vert S_A\vert \cdot \vert E_A \vert$ ESSP atoms to solve. Hence, the maximum costs of deciding the -ESSP for A equals $\vert S_A\vert \cdot \vert E_A \vert$-times the maximum effort for a single atom.

To decide the -solvability of a single ESSP atom (e, s), we compose systems in accordance to Lemma 7. The maximum costs can be estimated as follows: The (basic) part $M_{A'}$ of $M_\alpha$ has at most $\vert E_A \vert \cdot \vert S_A \vert ^2$ equations. Moreover, e occurs at most at $\vert S_A\vert -1$ states. This makes at most $\vert S_A\vert$ equations to ensure that e’s sources will have the same support, the third condition of Lemma 7. According to the first and the second condition, we choose an event , a value $sup(s_{A,0})\in \{0,\dots , b\}$, define $abs(e)=-m+n \text { mod } (b+1)$ and add the corresponding equation $\psi _{s_1} \cdot abs = m - sup(s_{A,0})$. For the fourth condition we choose a fixed value $q \in \{1,\dots , b\}$ and add the equation $(\psi _{s_1} - \psi _{s})\cdot abs =q$. Hence, the system has at most $2 \cdot \vert E_A\vert \cdot \vert S_A\vert ^2$ equations.

By Lemma 2, one checks in time $\mathcal {O}(\vert E_A\vert ^3 \cdot \vert S_A\vert ^4 )$ if such a system has a solution. Notice, we use that $2\cdot \vert E_A\vert \cdot \vert S_A\vert ^2 = max\{\vert E_A\vert , 2 \cdot \vert E_A\vert \cdot \vert S_A\vert ^2 \}$. There are at most $(b+1)^2$ possibilities to choose a corresponding and only $b+1$ possible values for x and for q, respectively. Hence, for a fixed atom (e, s), we have to solve at most $(b+1)^4$ such systems and b is not part of the input. Consequently, we can decide in time $\mathcal {O}(\vert E_A\vert ^3\cdot \vert S_A\vert ^4 )$ if (e, s) is solvable. A provides at most $\vert S_A \vert \cdot \vert E_A \vert$ ESSP atoms. Hence, the -ESSP for A is decidable in time $\mathcal {O}(\vert E_A\vert ^4 \cdot \vert S_A\vert ^5)$.    $\square$

The following lemma completes the proof of Theorem 1 and shows that -synthesis is doable in polynomial time.

Corollary 1

To construct for a TS A a -net N with a state graph $A_N$ isomorphic to A if it exists is doable in time $\mathcal {O}(\vert E_A\vert ^3 \cdot \vert S_A\vert ^5 \cdot max\{ \vert E_A\vert , \vert S_A\vert \})$.

Proof

By [5], if $\mathcal {R}$ is a set of regions of A containing for each ESSP and SSP atom of A a solving region, respectively, then the -net $N^\mathcal {R}_A=(\mathcal {R}, E_A, f, M_0)$, where $f((sup,sig),e)=sig(e)$ and $M_0((sup,sig))=sup(s_{0,A})$ for $(sup, sig)\in \mathcal {R}, e\in E_A$, has a state graph isomorphic to A. Hence, the corollary follows from Lemmas 5 and 8.    $\square$

3.3 Examples

We pick up our running example TS A introduced in Fig. 2 and its spanning tree $A'$ presented in Fig. 3. We present two steps of the method given by Lemma 8 for the type and check -solvability of the ESSP atom (c, 1).

For a start, we choose $(m,n)=(0,1)$ and $sup(0)=0$ and determine $abs(c)=-0+1=1$ which yields $abs=(x_a, x_b, 1 , x_d)$. We have to add $\psi _0\cdot abs=m-sup(0)=0$ which, by $\psi _0=(0,0,0,0)$, is always true and do not contribute to the system. Moreover, for $i\in \{0,2,3,4,5,6\}$, we add the equation $(\psi _0-\psi _i)\cdot abs =0$. We have $\psi _0-\psi _6=(0,0,-2,0)$ and $(0,0,-2,0)\cdot abs= 0\cdot x_a - 0\cdot x_b - 2 -0\cdot x_d=0$ yields a contradiction. Hence, (c, 1) is not solvable by a region (sup, sig) where $sup(0)=0$ and $sig(c)=(0,1)$. Similarly, we obtain that the system corresponding to $sup(0)\in \{1,2\}$ and $sig(c)=(0,1)$ is also not solvable.

For another try, we choose $(m,n)=(2,2)$ and $sup(0)=2$. In accordance to the first and the second condition of Lemma 7 this determines $abs=(x_a, x_b, 0 , x_d)$ and yields the equation $\psi _0 \cdot abs=m-sup(0)=2-2=0$ which is always true. For the fourth condition, we pick $q=2$ and add the equation $(\psi _0-\psi _1)\cdot abs= 2\cdot x_a=2$. Finally, for the third condition, we add for $i\in \{0,2,3,4,5,6\}$ the equation $(\psi _0-\psi _i)\cdot abs =0$ and obtain the following system of equations modulo $(b+1)$:

This system is solvable by $abs=(1,2,0,2)$. We construct a region in accordance to the proof of Lemma 7: By $sup(0)=2$ we obtain $sup(1)=2+\psi _1\cdot abs=2+(1,0,0,0)\cdot (1,2,0,2)=0$. Similarly, by $sup(i)=2+\psi _i\cdot abs$ for $i\in \{2,\dots , 7\}$ we obtain $sup(2)=sup(3)=sup(4)=sup(5)=sup(6)=2$ and $sup(7)=0$. Hence, by defining $sig(c)=(2,2)$, $sig(a)=1$, $sig(b)=2$ and $sig(d)=2$ we obtain a fitting -region (sup, sig) that solves (c, 1).

A closer look shows, that this support equals $sup_1$ which is presented in Fig. 2 and allows the signature $sig_1$, hence, $(sup, sig_1)=(sup_1, sig_1)$. The -region $(sup, sig_1)$ solves a lot of further ESSP and SSP atoms. This observation reveals a first possible improvement of the method introduced by Lemma 8 and suggest, given a solution abs, to map as many events of A to a signature different from $0,\dots , b$ as possible.

4 Fixed Parameter Tractability Results

Classical complexity theory measures the computational complexity of decision problems only in the size of the input. In [18], we showed that deciding if a TS A is -feasible or has the -ESSP, respectively, is NP-complete for . Thus, both problems are intractable from the perspective of classical complexity. Unfortunately, measuring the complexity purely in the size of A tells us nothing about the “source” of this negative result. On the contrary, parameterized complexity, developed by Downey and Fellows [10], allows us to study in which way different parameters of a TS A influence the complexity. This makes a finer analysis possible. Moreover, if we find a parameter, typically small on input instances of real-world applications, then algorithms, exponential in the size of the parameter but polynomial in the size of A, may work well in practice.

Formally, we say that a (decision) problem P is fixed paramter tractable with respect to parameter k if there exists an algorithm that solves P in time $\mathcal {O}(f(k)n^c)$, where f is some computable function, n is the size of the input and c is a constant independent from parameter k.

Let A be a TS and let for $e\in E_A$ the set containing the states of A at which e occur. The (maximum) number of occurrences of events is defined by $k=max\{ \vert S_e \vert \mid e\in E_A \}$. In [19] it has been shown that deciding -feasibility and -ESSP is NP-complete even if $k=2$. If there is a $\mathcal {O}(f(k)\vert A\vert ^c)$-time algorithm for these problems then, for $k=2$, it runs in polynomial time in A’s size. This is because f(2) is a constant. Thus, -feasibility and -ESSP, parameterized by k, are not fixed parameter tractable as long as P$\not =$NP.

On the contrary, the main result of this paper discovers that -ESSP and -feasibility parameterized by k are fixed parameter tractable. This reveals, that the number of occurrences of events is a structural property of the input A that makes -ESSP and -feasibility problems inherently hard to solve.

Theorem 2

Let and let A be a TS system with number of occurrences of events k. The -ESSP and the -feasibility are fixed parameter tractable with respect to parameter k.

Given an ESSP atom $\alpha$ of a TS A, the following lemma provides conditions which an abstract -region of A satisfies if and only if $\alpha$ is -solvable. Moreover, it teaches us how to gain a corresponding -solving region from an abstract region satisfying the conditions.

Lemma 9

Let , let (e, s) be an ESSP atom of A and let $s_1,\dots , s_k$ be the sources of e in A, that is, for $i\in \{1,\dots , k\}$ and if $s'\in S_A\setminus \{ s_1,\dots , s_k\}$ then .

The ESSP atom (e, s) is -solvable if and only if there is an event and an abstract region (sup, abs) of A that satisfies the following conditions:

• 1. $abs(e) = -m+n \text { mod } (b+1)$,

• 2. $\psi _{s_i}\cdot abs = sup(s_i) -sup(s_{A,0}) \text { mod } (b+1)$ and $m\le sup(s_i) \le b+m-n$ for $i\in \{1,\dots , k\}$,

• 3. $\psi _{s}\cdot abs = sup(s) -sup(s_{A,0}) \text { mod } (b+1)$ and $0 \le sup(s) \le m-1$ or $b+m-n+1 \le sup(s) \le b$

Proof

If: Let (sup, abs) be an abstract -region of A satisfying (1)–(3). We get a -solving region (sup, sig) as follows: For $e'\in E_A$ we define $sig(e')=abs(e')$ if $e'\not = e$ and, otherwise, we set $sig(e')=(m,n)$ if $e'= e$. Firstly, we show that (sup, sig) is a region and, secondly, we argue that it -solves (e, s).

We have to show, that in A implies in . If $e'\not =e$, then this is true by (sup, abs) being a -region. It remains to show that implies for $i\in \{0,\dots , k\}$. By $m \le sup(s_i) \le b+m-n$ and the definition of , there is an with . This implies . The assumption $abs(e)= -m + n \text { mod }(b+1)$ yields . Hence, we have that $sup(s_i)+abs(e) = sup(s_i) - m + n \text { mod }(b+1)$. By we get $sup(s_i')= sup(s_i)+abs(e) \text { mod }(b+1)$ such that $sup(s_i')=sup(s_i) - m + n\text { mod }(b+1)$. Consequently, implying making (sup, sig) a -region.

Moreover, by $0\le sup(s)\le m-1$ or $b+m-n+1 \le sup(s) \le b$ we have that such that (sup, sig) -solves (e, s).

Only-If: Let (sup, sig) be a -region that solves (e, s). In accordance to Lemma 6, we define the -abstract region (sup, abs) originating from (sup, sig). We argue that (sup, abs) satisfies the conditions (1)–(3).

As (sup, sig) -solves (e, s) there is an event such that , $i\in \{1,\dots , k\}$, and . By abs’s definition, $abs=-m+n\text { mod } (b+1)$ implying the first condition. Moreover, (sup, abs) satisfies the path equation. Hence, we have $sup(s_i)=sup(s_{A,0}) +\psi _{s_i}\cdot abs \text { mod } (b+1)$ implying $\psi _{s_i}\cdot abs = sup(s_i) -sup(s_{A,0}) \text { mod } (b+1)$ for $i\in \{1,\dots , k\}$. Furthermore, by and ’s definition, we have $m\le sup(s_i) \le b+m-n$. Thus, the second condition is satisfied. Similarly, the path equation implies $\psi _{s}\cdot abs = sup(s) -sup(s_{A,0}) \text { mod } (b+1)$ and, by , we obtain $0\le sup(s) \le m-1$ or $b+m-n+1 \le sup(s) \le b$. Hence, the third condition is also true.    $\square$

The following lemma shows that deciding the -ESSP for A is only exponential in parameter k but polynomial in the size of the input.

Lemma 10

If , then to decide for a k-fold TS A whether it has the -ESSP is possible in time $\mathcal {O}((b+1)^{k+4}\cdot \vert E_A\vert ^4 \cdot \vert S_A\vert ^5)$.

Proof

An ESSP atom (e, s) of A is a -solvable if and only if there is an abstract region (sup, abs) of A that satisfying the conditions of Lemma 9. Using Lemma 9, to decide the solvability of (e, s) we iteratively construct systems of linear equations $M_\alpha$. There is an abstract region (sup, abs), fulfilling the conditions, if and only if at least one $M_\alpha$ is solvable by abs. A single system to be computed modulo $b+1$ is obtained as follows:

Firstly, it implements the basic part $M_{A'}$ requiring at most $\vert E\vert \vert S_A\vert ^2 - 1$ equations.

Secondly, we choose an event $(m,n)\in E_A$ and a value $sup(s_{A,0}) \in \{0,\dots , b\}$ and, in accordance to Lemma 9.1, set $abs(e)=-m+n\text { mod }(b+1)$. Thus, the number of unknown becomes $\vert E_A\vert -1$.

Thirdly, in accordance to Lemma 9.2, we choose for every source $s'$ of e in A () a value $sup(s')$ satisfying $m \le sup(s') \le b+m-n$. After that we add the equation $\psi _{s'}\cdot abs = sup(s') - sup(s_{A,0})$. By definition of k, there are at most k sources of e. This yields at most k additional equations.

Finally, we choose sup(s) such that $0 \le sup(s) \le m-1$ or $b + m- n+1\le sup(s) \le b$, respectively. Then we add the equation $\psi _{s}\cdot abs = sup(s) - sup(s_{A,0})$. Now, a solution satisfies the condition of Lemma 9.3.

Altogether, by Lemma 9, this defines a fitting system whose solvability proves the -solvability of (e, s). Moreover, the system has at most $\vert E_A\vert \cdot \vert S_A\vert ^2+k\le 2\cdot \vert E_A\vert \cdot \vert S_A\vert ^2$ equations.

We estimate how many such systems must be maximally resolved for a single atom: By definition of , we have at most $(b+1)^2$ possible choices for $(m,n)\in \{0,\dots , b\}^2$, and at most $b+1$ different values for $sup(s_{A},0)\in \{0,\dots , b\}$, respectively. Furthermore, having (m, n) and $sup(s_{A,0})$ already chosen, there are at most $b+1$ possible choices for sup(s) with $0 \le sup(s) \le m-1$ or $b + m- n+1\le sup(s) \le b$. Similarly, for every source $s'$ of e we have at most $b+1$ choices for $sup(s')$ with $m \le sup(s') \le b+m-n$. By definition of k this makes at most $(b+1)^k$ different possible choices for the sources of k. Altogether, we have at most $(b+1)^{k+4}$ possibilities to define a system of linear equations whose solvability implies the -solvability of (e, s). Moreover, each system has at most size $2 \cdot \vert E_A\vert \cdot \vert S_A\vert ^2$.

Hence, by Lemmas 2 and 9 and $\vert E_A\vert \le \vert E_A\vert \cdot \vert S_A\vert ^2$, we can decide in time $\mathcal {O}((b+1)^{k+4}\cdot \vert E_A\vert ^3 \cdot \vert S_A\vert ^4)$ if the atom (e, s) is -solvable. Consequently, by the at most $\vert E_A\vert \cdot \vert S_A\vert$ different ESSP atoms of A, we can decide whether A has the -ESSP in $\mathcal {O}((b+1)^{k+4}\cdot \vert E_A\vert ^4 \cdot \vert S_A\vert ^5)$ time.    $\square$

If then, by Lemmas 5 and 9, deciding if a TS A has the -SSP and the -ESSP is doable in time $\mathcal {O}(\vert E_A\vert ^3 \cdot \vert S_A\vert ^6)$ and $\mathcal {O}((b+1)^{k+4}\cdot \vert E_A\vert ^4 \cdot \vert S_A\vert ^5)$, respectively. Thus, the following corollary is justified and completes the proof of Theorem 2.

Corollary 2

If then to decide if a TS A has the -feasibility is doable in time $\mathcal {O}((b+1)^{k+4}\cdot \vert E_A\vert ^3 \cdot \vert S_A\vert ^5 \cdot max\{ \vert E_A\vert , \vert S_A\vert \} )$.

5 Conclusion

In this paper, we investigate the computational complexity of synthesis, feasibility, ESSP and SSP for several types of b-bounded P/T-nets, $b\in \mathbb {Z}_{b+1}$. We introduce the new Petri net type of restricted $\mathbb {Z}_{b+1}$-extended b-bounded P/T-nets and show that for this type synthesis and all corresponding decision problems are solvable in polynomial time. Moreover, we show that SSP is decidable in polynomial time for the types of (pure) $\mathbb {Z}_{b+1}$-extended b-bounded P/T-nets. Finally, we prove that feasibility and ESSP for (pure) $\mathbb {Z}_{b+1}$-extended b-bounded P/T-nets are fixed parameter tractable if the (maximum) number of occurrences of events is considered as parameter.

It remains for future work to search for other parameters that makes feasibility for Petri net types fixed parameter tractable. Moreover, the question whether there are tractable superclasses of (pure) b-bounded P/T-nets is still open. One might also investigate the computational complexity for other Petri nets related synthesis problems: The exact complexity status of synthesis up to language equiavalence is unknown. In [3], Badouel et al. proposed an algorithm that requires exponential space. Another open question has been stated in [15]: Schlachter et al. suggested to characterize the complexity of synthesis for b-bounded P/T-nets from modal transitions systems. Here, the task is to find, for a given modal TS M, a Petri net N that implements M. So far, we are at least aware of some (new) lower and upper bounds:

Conjecture 1

Let $b\ge 2$. Deciding, for a given TS A, if there is a (pure) b-bounded P/T-net N such that its state graph has the same language as A is NP-hard. Moreover, the problem is in PSPACE. To decide for a given modal TS M if there exists a (pure) b-bounded P/T-net N that implements M is NP-hard.