Reachability in Petri Nets with Inhibitor arcs ^{∗}

Klaus Reinhardt

Wilhelm-Schickhard Institut für Informatik, Universität Tübingen Sand 13, D-72076 Tübingen e-mail: reinhard@informatik.uni-tuebingen.de

November 9, 1995

Abstract

We define a new structure called nested Petri net. We show that the question whether a complex transition in a nested Petri net can fire is decidable. From this it follows that the reachability problem is decidable for those Petri nets where the places can be ordered in such a way that, if a transition has an inhibitor arc from a place, then this transition has an inhibitor arc from every smaller place. Especially the reachability problem is decidable for Petri nets with only one inhibitor arc, which solves an open problem from [KLM89] .

As a consequence the emptiness problem and the halting problem are decidable for priority-multicounter-automata which can only perform a zero test of a counter if all counters with smaller index are already zero, and for restricted priority-multipushdown-automata.

1 Introduction

The decidability of the reachability problem in Petri nets without inhibitor arcs is proved in [May84] and later in [Kos84]. On the other hand, the reachability problem is undecidable for Petri nets with two inhibitor arcs. An open problem in [KLM89] was the reachability problem for Petri nets with one inhibitor arc. We solve the problem and, furthermore, show that the reachability problem is decidable in such Petri nets where the places can be ordered in a way such that a place has an inhibitor arc to all those transitions which have an inhibitor arc to a preceding place. We use this order for building a nested Petri net. The smallest places are only accessible in the innermost levels of the nested Petri net, whereas the transitions having the most inhibitor arcs appear in the outermost levels, where the places, from where those inhibitor arcs come, do not appear (thus can not have tokens). The main difference to the structured nets in [CK86] is that only the start- and end-marking of an inner net influence the behavior of a complex transition. The algorithm which works on the nested Petri net is structurally based on the algorithm in [Kos84]; but, in order to be able to work recursively on the structure of nestedness, additional features have been added. On the other hand, the states of the vector addition systems in [Kos84] are not necessary anymore, since the regular control can be expressed by the structure of nestedness (like a regular expression replacing a finite automaton). The decidability of the emptiness problem for priority-multicounter-automata has consequences in trace theory: it allows to decide the maximality and synchronizability of trace languages [Rei94] and the injectivity of a morphism between trace monoids [HM95] in a larger set of cases (both problems are undecidable in general). The restricted priority-multipushdown-automata generalize the result in [JKLP90] that \underline{LIN}%D′_{1}^{∗} (the class of languages generated by linear grammar and deletion of semi Dyck words) is recursive. The problems whether \underline{CF} %D′_{1}^{∗} is recursive and whether emptiness is decidable for pushdown-automata with weak counters, are still open.

∗This research has been supported by the EBRA working group No. 3166 ASMICS and by the DFG Project La 618/3-1 KOMET.

1.1 Multisets

For the sake of a flexible description, we use multi-sets instead of vectors. A multi-set over B is a function in ℕ^{B}. We regard a function f : A ↦ ℕ^{B} as multi-set in ℕ^{B×A} with f(b, a) = f(a)(b), f(., a) = f(a) and f(b, .) = {a ↦ f(b, a) | a ∈ A} or as B × A-matrix. For A ⊆ B it holds ℕ^{A} ⊆ ℕ^{B}, where a function is extended to zero for undefined values. It holds ℕ^{A} ∩ ℕ^{B} = ℕ^{A∩B}. The neutral element for addition is ∅ with ∅(x) = 0 for all x. The restriction of a multi-set f ∈ ℕ^{B} to A is f |_{A}:= {b ↦ f(b) | b ∈ A}. The complement operation is f |\overline{A}:= \{b ↦ f(b) | b ∉ A\}, thus f = f |_{A} +f |\overline{A}. Let M ⊆ ℕ^{A} be a finite set of multi-sets, then the identity id_{M} ∈ M^{M} ⊆ ℕ^{A×M} with ∀m ∈ M id_{M}(., m) = id_{M}(m) := m is a A × M-matrix. For a finite set M of multi-sets, M^{∗} := { Σ_{m∈M} mf(m) | f ∈ ℕ^{M}} is the set of all linear

combinations.

1.2 Petri nets with inhibitor arcs

An inhibitor arc from a place to a transition means that the transition can only fire, if no token is on the place. We describe such a Petri net as the 6-tuple (P, T, W, I, m_{0}, m_{e}) with the places P, the transitions T, the weight function W ∈ ℕ^{P ×T ∪T ×P}, the inhibitor arcs I ⊆ P × T and the start and end markings m_{0}, m_{e} ∈ ℕ^{P}. We will denote an inhibitor arc in the pictures by ————• . A transition t ∈ T can fire from a marking m ∈ ℕ^{P} to a marking m′ ∈ ℕ^{P}, denoted by m[t⟩m′, if m − W (., t) = m′ − W (t, .) ∈ ℕ^{P} and ∀p ∈ P (p, t) ∈ I → m(p) = 0. A firing sequence w = t_{1}...t_{n} ∈ T^{∗} can fire from m_{0} to m_{n}, denoted by m_{0}[w⟩m_{n}, if m_{1}, ...m_{n−1} exist with m_{0}[t_{1}⟩m_{1}[t_{2}⟩...[t_{n}⟩m_{n}. The reachability problem for a Petri net (P, T, W, I, m_{0}, m_{e}) is to decide, whether there exists a w ∈ T^{∗} with m_{0}[w⟩m_{e}. In the following two lemmata, we restrict the cases for which we have to regard the reachability problem. The aim of the first lemma is to make the reachability problem symmetric, that means the reachability problem is the same for (P, T, W^{−1}, I, m_{e}, m_{0}) with W^{−1} := {(x, y) | (y, x) ∈ W }:

Lemma 1.1 Each Petri net (P, T, W, I, m_{0}, m_{e}) can be changed in a way such that the condition ∀p ∈ P, t ∈ T (p, t) ∈ I → W (t, p) = 0 holds without changing the inhibitor arcs or the reachability problem.

Proof: Consider a transition t ∈ T such that there exists a p ∈ P with (p, t) ∈ I and W (t, p) = x > 0, depicted by

[figure: p; t; •; x]

We add a new transition t′ in T′ := T ∪{t′} and two new places p′ and p′′ in P′ := P ∪{p′, p′′}. The start-marking m′_{0} := m_{0} + {p′′ ↦ 1} and the end-marking m′_{e} := m_{e} + {p′′ ↦ 1} get an additional token on p′′. Set W′(t′, .) := W (t, .) + {p′′ ↦ 1}, that means all the arcs from the transition t and an arc to p′′ are now arcs from the transition t′. An arc from p′′ to t is added, that means W′(., t) := W (., t) + {p′′ ↦ 1}. Set W′(t, .) := W′(., t′) := {p′ ↦ 1}, W′(t_{a}, .) := W (t_{a}, .) + {p′′ ↦ 1} and W′(., t_{a}) := W (., t_{a}) + {p′′ ↦ 1} for every t_{a} ∈ T \ {t}.

[figure: p; t; p′; t′; p′′; t_{a}; •; x]

There will always be exactly one token either on p′ or p′′. If t fires, then no token is on p′′ and so t′ is the only transition which can fire. The firing of tt′ (together) has the same effect on the net as the firing of t before the change, hence the reachability problem remains the same. A general aim of the decision algorithm explained below is to reduce the number of places and transitions and keep the information in a structural description instead. But in the next lemma we do a step in the opposite direction in order to make the translation to nested Petri nets easier.

Lemma 1.2 Each Petri net (P, T, W, I, m_{0}, m_{e}) can be changed in a way such that the condition ∀p ∈ P, t ∈ T (p, t) ∈ I → m_{0}(p) = m_{e}(p) = 0 holds without changing the inhibitor arcs, the condition in Lemma 1.1 or the reachability problem.

Proof: We add a two new transitions t and t′ in T′ := T ∪ {t, t′} and three new places p, p′ and p′′ in P′ := P ∪ {p, p′, p′′}. Set W′(t, .) := m_{0} + {p′ ↦ 1}, W′(., t′) := m_{e} + {p′ ↦ 1}, W′(., t) := {p ↦ 1}, W′(t′, .) := {p′′ ↦ 1}, m′_{0} := {p ↦ 1} and m′_{e} := {p′′ ↦ 1}. For every t_{a} ∈ T we set W′(t_{a}, .) := W (t_{a}, .) + {p′ ↦ 1} and W′(., t_{a}) := W (., t_{a}) + {p′ ↦ 1}, which prevents a firing before t and after t′. This means that t is the first and t′ is the last transition to fire and they can only fire once. Obviously the reachability problem from the marking after the firing of t to the marking before the firing of t′ is the same as before.

2 Nested Petri nets

On the top level, we consider T as a set of transitions of the form t = (K, c, Γ) where P_{T} is the set of places which are accessed by transitions in T on the upper level, K is a set of nested sub-Petri nets (P_{T_{i}}^{+}, T_{i}), where P_{T_{i}}^{+} is the set of those places in P_{T_{i}} which are restricted to never having a negative marking. The multi-sets in

\{c\} ∪ Γ ⊂ ℕ^{(\{+,−\}×(P_{T} ˙∪ ˙⋃_{(P{+ \atop T_{i}} ,T_{i})∈K} P_{T_{i}} )}

describe the connection of the external switching behavior of t and the internal switching condition on the subnet level by the linear set c + Γ^{∗}. This inductive definition starts with elementary transitions having K = ∅. Using the reachability relation R_{(P_{T_{i}}^{+},T_{i})} defined recursively for the subnets, we get the restriction

E_{t} := {f ∈ c + Γ^{∗} | ∀(P_{T_{i}}^{+}, T_{i}) ∈ K (f(+)|_{P_{T_{i}}} , f(−)|_{P_{T_{i}}}) ∈ R_{(P_{T_{i}}^{+},T_{i})} }

of the linear set c+Γ^{∗} to all possible behaviors of the transition t. The restriction is that in every subnet (P_{T_{i}}^{+}, T_{i}) there is a firing sequence from the marking f(+)|_{P_{T_{i}}} to the marking f(−)|_{P_{T_{i}}} (no further token may be left). Thus, for elementary transitions t = (∅, c, Γ), we have simply E_{t} = c + Γ^{∗}. For a set of transitions, we take the union E_{T} := ⋃_{t∈T} E_{t} of all possible behaviors. The switch-ability problem for T is the question whether E_{T} ≠ ∅. The extended reachability relation for a set of transitions

ER_{T} := {(m, m′, f) | m − f(−)|_{P_{T}} = m′ − f(+)|_{P_{T}} , f ∈ E_{t}}

additionally describes the effect of the behavior of a transition in T on a marking m where f(−)|_{P_{T}} is subtracted, and then f(+)|_{P_{T}} is added to reach the following marking m′. The reachability relation for a set of transitions is R_{T} := {(m, m′) | (m, m′, f) ∈ ER_{T} }. The reachability relation for a subnet (P_{T}^{+}, T)

R_{(P_{T}^{+},T)} := id_{P_{T}} ∪ T ransClos(R_{T} ∩ (ℕ^{P_{T}^{+}} + ℤ^{P_{T}})^{2})

describes the effect of arbitrarily many applications of transitions in T by the transitive closure (including no application described by id_{P_{T}}) where the places in P_{T}^{+} may never have a negative marking. Analogously the extended reachability relation for a subnet (P_{T}^{+}, T) is

ER_{(P_{T}^{+},T)} := \{(m, m′, f) | ∃ m_{0} = m, ..., m_{n} = m′ ∀ \begin{matrix}i < n (m_{i}, m_{i+1}, f_{i}) ∈ ER_{T} , \\ ∀p ∈ P_{T}^{+} m_{i}(p) ≥ 0, f = ∑_{i=1}^{n−1} f_{i}\} \end{matrix}

and E_{(P_{T}^{+},T)} := {f | (m, m′, f) ∈ ER_{(P_{T}^{+},T)}}. It is easy to see that E_{(P_{T}^{+},T)} = E_{T}^{∗} by taking m and m′ large enough to keep all markings in the sequence positive.

Example: Let T = {t} with one outer place in P_{T} = {p′′_{1}} have one transition t = ({({p_{1}, p_{2}, p_{3}}, {t_{1}, t_{2}}), ({p′_{1}, p′_{3}}, {t_{3}})}, c, Γ) with

t_{1} = (∅, {(−, p_{1}) ↦ 1, (+, p_{2}) ↦ 2}, ∅)
t_{2} = (∅, {(−, p_{2}) ↦ 1, (+, p_{3}) ↦ 1}, ∅),
t_{3} = (∅, {(−, p′_{3}) ↦ 1, (+, p′_{1}) ↦ 2}, ∅),

and c = {(−, p′′_{1}) ↦ 1, (+, p_{1}) ↦ 2, (−, p_{3}) ↦ 1, (+, p′_{3}) ↦ 3, (−, p′_{1}) ↦ 1, (−, p′_{3}) ↦ 1, (+, p′′_{1}) ↦ 2} represented by the picture

[figure: p′′_{1}; p_{1}; p_{2}; t_{1}; p_{3}; t_{2}; p′_{3}; p′_{1}; t_{3}; 2; 2; 3; 2; 2]

The periods in Γ = \{ \begin{matrix}\{(−, p′′_{1}) ↦ 1, (+, p_{1}) ↦ 1\}, \{(−, p_{1}) ↦ 1, (+, p′_{1}) ↦ 1\}, \\ \{(−, p_{3}) ↦ 1, (+, p′_{3}) ↦ 1\}, \{(−, p′_{1}) ↦ 1, (+, p′′_{1}) ↦ 1\}\} \end{matrix}

are invisible in the picture. From this we get R_{({p_{1},p_{2},p_{3}},{t_{1},t_{2}})} =

\{ \begin{matrix}(\{p_{1} ↦ x_{1} + y_{1}, p_{2} ↦ x_{2} + y_{2}, p_{3} ↦ x_{3}\}, \{p_{1} ↦ x_{1}, p_{2} ↦ x_{2} + 2y_{1}, p_{3} ↦ x_{3} + y_{2}\}) \\ | x_{1}, y_{1}, y_{2}, x_{2} + y_{2}, x_{2} + y_{1}, x_{3} ≥ 0\} \end{matrix}

and R_{({p′_{1},p′_{3}},{t_{3}})} =

{({p′_{1} ↦ x′_{1}, p′_{3} ↦ x′_{3} + y_{3}}, {p′_{1} ↦ x′_{1} + 2y_{3}, p′_{3} ↦ x′_{3}}) | x′_{1}, x′_{3}, y_{3} ≥ 0},

where y_{i} is the number of firings of t_{i}. Solving a systems of equations we get E_{t} = c′ + Γ^{′∗} ∪ c′′ + Γ^{′∗} with

c′ = { (−, p′′_{1}) ↦ 1, (+, p_{1}) ↦ 2, (−, p_{1}) ↦ 1, (−, p_{3}) ↦ 2,
(+, p′_{1}) ↦ 1, (+, p′_{3}) ↦ 4, (−, p′_{1}) ↦ 7, (−, p′_{3}) ↦ 1, (+, p′′_{1}) ↦ 8},
c′′ = { (−, p′′_{1}) ↦ 1, (+, p_{1}) ↦ 2, (−, p_{1}) ↦ 0, (−, p_{3}) ↦ 4,
(+, p′_{1}) ↦ 0, (+, p′_{3}) ↦ 6, (−, p′_{1}) ↦ 10, (−, p′_{3}) ↦ 1, (+, p′′_{1}) ↦ 11},
Γ′ = { {(−, p′′_{1}) ↦ 1, (+, p_{1}) ↦ 1, (−, p_{1}) ↦ 1, (+, p′_{1}) ↦ 1, (−, p′_{1}) ↦ 1, (+, p′′_{1}) ↦ 1},

{(−, p′′_{1}) ↦ 1, (+, p_{1}) ↦ 1, (−, p_{3}) ↦ 2, (+, p′_{3}) ↦ 2, (−, p′_{1}) ↦ 4, (+, p′′_{1}) ↦ 4}}.

Thus R_{{t}} = {(−, p′′_{1}) ↦ 1, (+, p′′_{1}) ↦ 8} + Γ^{′′∗} ∪ {(−, p′′_{1}) ↦ 1, (+, p′′_{1}) ↦ 11} + Γ^{′′∗} with

Γ′′ = {{(−, p′′_{1}) ↦ 1, (+, p′′_{1}) ↦ 1}, {(−, p′′_{1}) ↦ 1, (+, p′′_{1}) ↦ 4}}.

2.1 Transformation of a Petri net with one inhibitor arc

Example: Consider the following Petri net:

[figure: p_{2}; t_{1}; t̂; p_{1}; p_{3}; t_{2}; 5; 7; 3; 2; •]

with the start marking {p_{2} ↦ 4, p_{3} ↦ 2} and the end marking {p_{2} ↦ 4, p_{3} ↦ 3}. It is clear that we can cut the firing sequences in (t_{1} + t_{2} + t̂)^{∗} = ((t_{1} + t_{2})^{∗} + t̂)^{∗} into parts in (t_{1} + t_{2})^{∗} and t̂ all starting and ending with no token on p_{1}. The idea is to represent those firing sequences in (t_{1} + t_{2})^{∗} by only one switching of the complex transition t_{k}:

[figure: p′_{2}; p′_{2}; p_{2}; t_{k}; t_{1}; t_{2}; p_{1}; p′_{3}; p′_{3}; p_{3}; =; y; z; y; z; y; z; 3; 2]

Here, y and z correspond to {(−, p′_{2}) ↦ 1, (+, p_{2}) ↦ 1} and {(−, p_{3}) ↦ 1, (+, p′_{3}) ↦ 4}. In order to obtain a switch-ability problem we construct one complex transition t′_{k} on the top level:

[figure: p′_{2}; t_{k}; p′_{3}; t̂; 2; 4; y; z; 7; 5; 3; 4]

Looking at the subnet in t_{k}, it is easy to see that t_{k} can fire with y = 2x and z = 3x for x ≥

0. Thus, there is the firing sequence ( \begin{matrix}4 \\ 2 \end{matrix} )[t_{k}^{x=2}⟩( \begin{matrix}0 \\ 8 \end{matrix} )[t̂⟩( \begin{matrix}5 \\ 1 \end{matrix} )[t_{k}^{x=2}⟩( \begin{matrix}1 \\ 7 \end{matrix} )[t̂⟩( \begin{matrix}6 \\ 0 \end{matrix} )[t_{k}^{x=1}⟩( \begin{matrix}4 \\ 3 \end{matrix} )

which fulfills the condition for the firing of t′_{k}.

Theorem 2.1 For a Petri-net (P, T, W, {(p_{1}, t̂)}, m_{0}, m_{e}) with only one inhibitor arc (p_{1}, t̂) the reachability problem is decidable.

Proof: Let the Petri-net have the properties of lemmata 1.1 and 1.2. The innermost net (P, T_{1}) consists of all transitions

T_{1} := {(∅, c_{t}, ∅) | t ∈ T \ {t̂} ∧ c_{t}(−, .) = W (., t) ∧ c_{t}(+, .) = W (t, .)}

except t̂. The next net is (P′, T_{2}) consisting of the places P′ = {p′ | p ∈ P \ {p_{1}}} and the transitions

\begin{matrix}T_{2} := \{t_{k}\} ∪ \{ (∅, c′_{t}, ∅) | t ∈ T ∧ c′_{t}(−, .′) = W (., t) ∧ c′_{t}(+, .′) = W (t, .) \\ ∧ W (p_{1}, t) = W (t, p_{1}) = 0 \} \end{matrix}

with

t_{k} = ({(P, T_{1})}, ∅, {{(−, p′) ↦ 1, (+, p) ↦ 1}, {(−, p) ↦ 1, (+, p′) ↦ 1} | p ∈ P }) .

On the top level we have T_{3} := {t′_{k}} with

t′_{k} = ({(P′, T_{2})}, {(+, p′) ↦ m_{0}(p), (−, p′) ↦ m_{e}(p) | p ∈ P }, ∅).

To decide the reachability problem using Corollary 3.1, we have to show that ∃w ∈ T^{∗} m_{0}[w⟩m_{e} iff R_{T_{3}} ≠ ∅: The firing sequence w can be decomposed in minimal firing sequences w_{1}...w_{k} having the property m_{0}[w_{1}⟩m_{1}[w_{2}⟩...[w_{k}⟩m_{k} = m_{e} such that m_{i}(p_{1}) = 0 for all i ≤ k. If w_{i} = t_{i} ∈ T then W (p_{1}, t_{i}) = W (t_{i}, p_{1}) = 0 consequently t′_{i} = (∅, c′_{t_{i}}, ∅) ∈ T_{2} thus (m′_{i−1}, m′_{i}, c′_{t_{i}}) ∈ ER_{T_{2}} and hence (m′_{i−1}, m′_{i}) ∈ R_{T_{2}}. Otherwise, w_{i} = t_{1}...t_{l}, having the property m_{i−1} = m′_{0}[t_{1}⟩m′_{1}[t_{2}⟩...[w_{l}⟩m′_{l} = m_{i} such that m_{i}(p_{1}) > 0 for all 0 < j < l (else w_{i} would not be minimal). Thus t_{j} ≠ t̂ for all 0 < j ≤ l therefore t′′_{j} = (∅, c_{t_{j}}, ∅) ∈ T_{1} consequently (m_{j−1}, m_{j}, c_{t_{j}}) ∈ ER_{T_{1}} hence (m_{j−1}, m_{j}) ∈ R_{T_{1}} for all 0 < j ≤ l. This means (m_{i−1}, m_{i}) ∈ R_{(P,T_{1})} thus f :=

∑_{p∈P} m_{i−1}(p){(−, p′) ↦ 1, (+, p) ↦ 1} + m_{i}(p){(−, p) ↦ 1, (+, p′) ↦ 1} ∈ E_{t_{k}}

therefore (m′_{i−1}, m′_{i}, f) ∈ ER_{T_{2}} hence (m′_{i−1}, m′_{i}) ∈ R_{T_{2}} as well. This means (m_{0}, m_{e}) ∈ R_{(P′,T_{2})} consequently f′ :=

∑_{p∈P}{(+, p′) ↦ m_{0}(p), (−, p′) ↦ m_{e}(p)} ∈ E_{t′_{k}}

therefore (∅, ∅) ∈ ER_{T_{3}} hence (∅, ∅) ∈ R_{T_{3}}. The other direction follows simply by composing firing sequences.

More generally, we can show that the reachability problem is decidable if the places can be ordered in such a way that each place has an inhibitor arc to all those transitions having an inhibitor arc from a place with lower order:

Theorem 2.2 For a Petri-net (P, T, W, {(p_{1}, t̂)}, m_{0}, m_{e}) with

∃g ∈ ℕ_{+}^{P} ∀p, p′ ∈ P g(p) ≤ g(p′) → (∀t ∈ T (p′, t) ∈ I → (p, t) ∈ I),

the reachability problem is decidable.

3 The decision algorithm for nested Petri nets

In order to decide the switch-ability problem, we want to establish a normal form T , which corresponds to the condition Θ in [Kos84]:

Definition A set of Transitions T has the property T if ∀t = (K, c, Γ) ∈ T, ∀N_{i} = (P_{T_{i}}^{+}, T_{i}) ∈ K the following conditions hold:

1. In recursive manner, T_{i} has this property T .

2. ∀g ∈ \{c\} ∪ Γ (g(+) − g_{ind}(−) + g_{ind}(+) − g(−))|_{P_{T_{i}}} = \overline{0}, where

g_{ind} := ∑_{t′=(K′,c′,Γ′)∈T_{i},g′∈{c′}∪Γ′}(g(+, p_{g′}) − g(−, p_{g′}))g′

describes the indirect effect of g using the property about the witness places in Condition 3 in the recursion for T_{i}, which says that g(+, p_{g′}) − g(−, p_{g′}) is exactly the number of times that g′ is used.

3. ∀g ∈ {c} ∪ Γ ∃p_{g} ∈ P_{T} g(−, p_{g}) = 1, g(+, p_{g}) = 0,

∀g′ ∈ ⋃_{t′=(K′,c′,Γ′)∈T}{c′} ∪ Γ′ \ {g} g′(−, p_{g}) = g′(+, p_{g}) = 0.

This condition says that the number of times where g is used is exactly the number of tokens which are consumed from the witness place p_{g}. For example, each firing of t′ consumes one token from p_{c′}.

4. Let Q_{i}^{+} := {p ∈ P_{T_{i}} | ∀g ∈ Γ g(+, p) = 0} and Q_{i}^{−} := {p ∈ P_{T_{i}} | ∀g ∈ Γ g(−, p) = 0} be the set of places for which the start marking (end-marking, respectively) is fixed only by c. Then

∃(c(+)|_{P_{T_{i}}} , c(+)|_{P_{T_{i}}} + Δ_{i}) ∈ R_{(Q_{i}^{+},T_{i})} with Δ_{i}|_{Q_{i}^{+}} ∈ (ℕ^{+})^{Q_{i}^{+}} and

∃(c(−)|_{P_{T_{i}}} + Δ′_{i}, c(−)|_{P_{T_{i}}}) ∈ R_{(Q_{i}^{−},T_{i})} with Δ′_{i}|_{Q_{i}^{−}} ∈ (ℕ^{+})^{Q_{i}^{−}} ensure that those places can be raised arbitrarily high by a firing sequence (and vice versa on the other side).

5. c ∈ E_{t}.

Theorem 3.1 For every set of transitions T we can effectively construct a T′ with R_{T} = R_{T′}|_{P_{T} ×P_{T}} such that T′ has property T .

The idea of the algorithm is to reduce T if one of the conditions is not fulfilled. For Condition 2, Presburger arithmetics is used to transfer the implicit quantitative restriction by the witness places to the explicit restriction of the transitions. Condition 3 allows the quantitative control over the firing sequences in the subnet on the outer levels. Condition 4 ensures that all places are unlimited. It can be decided by a covering graph construction, which uses the algorithm recursively (like for Condition 1) for every step, where the current marking is included as a restriction. Limited places are deleted at the cost of a larger structure.

Lemma 3.1 If the conditions 1 - 4 hold for t = (K, c, Γ), then it holds

∀f ∈ ∑_{g∈Γ} g + Γ^{∗}∀e ∈ (Γ ∪ −Γ)^{∗}∃k ≥ 2 {(c + kf), (c + kf + e)} ⊆ E_{t}

This means we can build up firing sequences, which compensate the ’odd’ firing sequences from condition 4, from the constant, and from the ’odd’ indirect firing sequences in order to find the c fulfilling condition 5. From condition 5 it is easy to see that R_{T} = ∅ iff T′ = ∅, thus it immediately follows:

Corollary 3.1 The switch-ability problem for T is decidable

4 Priority-Multicounter-Automata

We define a priority-multicounter-automaton by a restrictive zero-test according to an order of the counters in the following way: the first counter can be tested for zero at any time; the second counter can only be tested for zero simultaneously with the first counter; any further counter can only be tested for zero simultaneously with all preceding counters. Formally, this reads as follows: A priority-multicounter-automaton is a one-way automaton described by the 6-tuple

A = (k, Z, Σ, δ, z_{0}, E)

with the set of states Z, the input alphabet Σ, the transition relation

δ ⊆ (Z × (Σ ∪ {λ}) × {0 … k}) × (Z × {−1, 0, 1}^{k}),

initial state z_{0}, the accepting states E ⊆ Z, the set of configurations C_{A} = Z × Σ^{∗} × ℕ^{k}, the initial configuration σ_{A}(x) = ⟨z_{0}, x, 0^{k}⟩ and configuration transition relation

⟨z, ax, n_{1}, ..., n_{k}⟩ |_{\overline{A}} ⟨z′, x, n_{1} + i_{1}, ..., n_{k} + i_{k}⟩

iff z, z′ ∈ Z, a ∈ Σ ∪ {λ}, ⟨(z, a, j), (z′, i_{1}, ...i_{k})⟩ ∈ δ, ∀i ≤ j n_{i} = 0. The language recognized by an priority-multicounter-automaton A is L(A) = {w | ∃z_{e} ∈ E ∃n_{1}, ..., n_{k} ∈ ℕ ⟨z_{0}, w, 0, ..., 0⟩ |\frac{∗}{A} ⟨z_{e}, λ, n_{1}, ..., n_{k}⟩. A priority-multicounter-automaton can be changed in a way such that it has only one accepting state z_{e} and all counters are empty while accepting thus L(A) = \{w | ⟨z_{0}, w, 0, ..., 0⟩ |\frac{∗}{A} ⟨z_{e}, λ, 0, ..., 0⟩\}. Using Theorem 2.2, we show that the emptiness problem of the accepted language is decidable for priority-multicounter-automata. The same holds for the halting problem by constructing an automaton which contains its input in the states.

Theorem 4.1 The emptiness problem for priority-multicounter-automata is decidable.

Proof: Given A we construct a Petri net (P, T, W, I, m_{0}, m_{1}) with the places P := {1...k}∪Z, the transitions T = δ, the weights W with W (z, ((z′, a, j), (z′′, V))) := 1 if z = z′ else := 0, W (((z′, a, j), (z′′, V)), z) := 1 if z = z′′ else := 0, W (i, ((z′, a, j), (z′′, V))) := 1 if V (i) = −1 else := 0 and W (((z′, a, j), (z′′, V)), i) := 1 if V (i) = 1 else := 0, the inhibitor arcs I := {(i, ((z′, a, j), (z′′, V))) | i ≤ j}, the start marking m_{0} := {z_{0} ↦ 1} and the end marking m_{1} := {z_{e} ↦ 1}, which is reachable from m_{0} iff L(A) ≠ ∅. According to Theorem 2.2 with g(i) = i for i ≤ k and g(z) = k + 1 for z ∈ Z, this is decidable. The classes k-PMC of languages accepted by a priority-multicounter-automaton with k > 0 counters (and also their union) are incomparable to the class LIN of linear languages and it holds (k-1)-PMC⊊k-PMC, since {a^{n_{1}}ba^{n_{2}}...ba^{n_{k+1}}$a^{n_{k+1}}b...a^{n_{2}}ba^{n_{1}} | ∀i ≤ k + 1 n_{i} ∈ ℕ} ∉ k-P MC. This can be shown by constructing T fulfilling property T and then use Lemma 3.1 to find two different words in the language where the automaton has the same configuration reading $. With the same argument, this also holds for the classes k-BLIND and k-PBLIND in [Gre78]. Furthermore {(a^{n}b)^{m} | n, m ∈ ℕ} cannot be accepted by a priority-multicounter-automaton.

5 Restricted Priority-Multipushdown-Automata

We define a priority-multipushdown-automaton by a restrictive treatment of one of the two pushdown symbols according to an order of the pushdown stores in the following way: let the pushdown alphabet be {0, 1}. A 0 can be pushed to and popped from every pushdown store independently but a 1 can only be pushed to or popped from a pushdown store, if all pushdown stores with a lower order are empty. Furthermore, the restriction requires that if a 1 is popped from a pushdown store, then a 1 can not be pushed to this store until it has been empty meanwhile.

Theorem 5.1 The emptiness problem for restricted priority-multipushdown-automata is decidable.

Acknowledgment: I thank Volker Diekert, Henning Fernau and Klaus-Jörn Lange for helpful remarks.

References

[CK86] L. A. Cherkasova and V. E. Kotov. Structured nets. In J. Gruska and M. Chytil, editors, Proc. of 6th MFCS, number 118 in LNCS, pages 242–251. Springer, 1986.

[Dic13] L. E. Dickson. Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Amer. J. Math., 35:413–422, 1913.

[DM79] N. Dershowitz and Z. Manna. Proving Termination with Multiset Orderings. Comm. ACM, 22(8):465–476, 1979.

[ES69] Samuel Eilenberg and M. P. Schützenberger. Rational sets in commutative monoids. Journal of Algebra, 13:173–191, 1969.

[Gre78] S. Greibach. Remarks on blind and partially blind one-way multicounter machines. Theoret. Comput. Sci., 7:311–324, 1978.

[GS65] S. Ginsburg and E. H. Spanier. Semigroups, Presburger formulas, and languages. Pacific J. Math., 16:285–296, 1965.

[HM95] Hendrik Jan Hoogeboom and Anca Muscholl. The code problem for traces – improving the boundaries. Submitted for publication., 1995.

[JKLP90] M. Jantzen, M. Kudlek, K.-J. Lange, and H. Petersen. Dyck_{1}-reductions of context-free languages. In Computers and Artificial Intelligence, volume 9, pages 228–236, 1990.

[KLM89] H. Kleine Büning, T. Lettmann, and E. W. Mayr. Projections of vector addition system reachability sets are semilinear. Theoret. Comput. Sci., 64:343–350, 1989.

[Kos84] S. R. Kosaraju. Decidability of reachability in vector addition systems. In Proceedings 14th Ann. ACM STOC, pages 267–281, 1984.

[May84] E. Mayr. An algorithm for the general Petri net reachability problem. Siam J. Comput., 13:441–459, 1984.

[Rei94] Klaus Reinhardt. Prioritätszählerautomaten und die Synchronisation von Halbspursprachen. Dissertation, Institut für Informatik, Universität Stuttgart, 1994.

Appendix

We use a function Copy (with several indices) which gives new elements on atomic elements and is recursive on tuples, sets and multi-sets, that means for example Copy(M) = {Copy(x) | x ∈ M}, Copy(f) = {Copy(a) ↦ f(a) | f(a) > 0} and Copy(x_{1}, x_{2}, ...) = (Copy(x_{1}), Copy(x_{2}), ...).

A Transformation of a Petri net

Proof: (of Theorem 2.2) Let the Petri-net again have the properties of lemmata 1.1 and 1.2. Let P_{h} = {Copy_{h}(p) | g(p) ≥ h} be the places accessible on level h; this level can only represent markings having no token on a place p with g(p) < h. The innermost net (P_{1}, T_{1}) consists of all transitions

T_{1} := \{(∅, c_{t}, ∅) | \begin{matrix}c_{t}(−, .) = Copy_{1}(W (., t)) ∧ t ∈ T ∧ \\ c_{t}(+, .) = Copy_{1}(W (t, .)) ∧ ∀p ∈ P (p, t) ∉ I \} \end{matrix}

having no inhibitor arc. In general the net on level h > 1 is (P_{h}, T_{h}) having the transitions

T_{h} := \{t_{h}\} ∪ \{ (∅, c_{t}, ∅) | \begin{matrix}c_{t}(−, .) = Copy_{h}(W (., t)) ∧ t ∈ T ∧ \\ c_{t}(+, .) = Copy_{h}(W (t, .)) ∧ \\ ∀p ∈ P g(p) ≥ h → (p, t) ∉ I ∧ \\ ∀p ∈ P g(p) < h → W (p, t) = W (t, p) = 0 \} \end{matrix}

with

t_{h} = (\{(P_{h−1}, T_{h−1})\}, ∅, \{ \begin{matrix}\{(−, Copy_{h}(p)) ↦ 1, (+, Copy_{h−1}(p)) ↦ 1\}, \\ \{(−, Copy_{h−1}(p)) ↦ 1, (+, Copy_{h}(p)) ↦ 1\} | p ∈ P \}) . \end{matrix}

On the top level g = max{g(p) | p ∈ P } + 1 we have T_{g} := {t_{g}} with

t_{g} = ({(P_{g−1}, T_{g−1})}, {(+, Copy_{g−1}(p)) ↦ m_{0}(p), (−, Copy_{g−1}(p)) ↦ m_{e}(p) | p ∈ P }, ∅).

In order to decide the reachability problem using Corollary 3.1, we have to show that ∃w ∈ T^{∗} m_{0}[w⟩m_{e} iff R_{T_{g}} ≠ ∅: The firing sequence w can be decomposed in minimal firing sequences w_{1}...w_{l} having the property m_{0}[w_{1}⟩m_{1}[w_{2}⟩...[w_{l}⟩m_{k} = m_{e} such that m_{i}(p) = 0 for all i ≤ l and p with g(p) < g − 1. For h < g − 1 we can say that a firing sequence m′_{0}[w′⟩m′_{e} starting and ending with a marking without a token on a place p with g(p) ≤ h but always having a token on a place p with g(p) ≤ h in the markings in between, can be decomposed in minimal firing sequences w_{1}...w_{k} having the property m′_{0}[w_{1}⟩m′_{1}[w_{2}⟩...[w_{k}⟩m′_{k} = m′_{e} such that m′_{i}(p) = 0 for all i ≤ k and p with g(p) < h. Thus, for all 1 < i < k, there is a p with g(p) = h and m′_{i}(p) > 0. If w_{i} = t_{i} ∈ T then W (p, t_{i}) = W (t_{i}, p) = 0 for all p with g(p) < h and (p, t_{i}) ∉ I for all p with g(p) ≥ h thus t_{i} = (∅, c_{t_{i}}, ∅) ∈ T_{h} therefore (Copy_{h}(m′_{i−1}), Copy_{h}(m′_{i}), c_{t_{i}}) ∈ ER_{T_{h}} hence Copy_{h}((m′_{i−1}, m′_{i})) ∈ R_{T_{h}}. (For h = 1 this is the only case, which starts the induction.) Else by minimality of w_{i} there is always a token on a place p with g(p) < h in the markings between. Thus, by induction over h it holds Copy_{h−1}((m′_{i−1}, m′_{i})) ∈ R_{(P_{h−1},T_{h−1})} therefore

f := ∑_{p∈P} \begin{matrix}m′_{i−1}(p)\{(−, Copy_{h}(p)) ↦ 1, (+, Copy_{h−1}(p)) ↦ 1\}+ \\ m_{i}(p)\{(−, Copy_{h−1}(p)) ↦ 1, (+, Copy_{h}(p)) ↦ 1\} ∈ E_{t_{h}} \end{matrix}

thus (Copy_{h}(m′_{i−1}), Copy_{h}(m′_{i}), f) ∈ ER_{T_{h}} hence Copy_{h}((m′_{i−1}, m′_{i})) ∈ R_{T_{h}} as well. This means Copy_{h}((m′_{0}, m′_{e})) ∈ R_{(P_{h},T_{h})}, which completes the induction. On the top level by concatenation of all Copy_{g−1}((m_{i−1}, m_{i})) ∈ R_{(P_{g−1},T_{g−1})} for all 1 ≤ i ≤ g we analogously get Copy_{g−1}((m_{0}, m_{e})) ∈ R_{(P_{g−1},T_{g−1})} thus

f′ := ∑_{p∈P}{(+, Copy_{g−1}(p)) ↦ m_{0}(p), (−, Copy_{g−1}(p)) ↦ m_{e}(p)} ∈ E_{t_{g}}

thus (∅, ∅) ∈ ER_{T_{g}} thus (∅, ∅) ∈ R_{T_{g}}. The other direction again follows simply by composing firing sequences.

Example: The start marking {p_{3} ↦ 3, p_{4} ↦ 2} and the end marking {p_{4} ↦ 27} of the Petri net

[figure: p_{3}; t_{1}; p_{4}; t_{2}; t_{4}; p_{1}; p_{2}; t_{3}; 3; 5; 2; 2; 2; •; •; •; 5]

with the function g with g(p_{1}) = 1, g(p_{2}) = 2 and g(p_{3}) = g(p_{4}) = 3 leads to the nested transition

[figure: 2; 3; 27; t_{4}; p′′_{3}; p′′_{4}; 5; t_{3}; p′_{3}; p′_{4}; p′_{2}; 5; 2; p_{3}; t_{1}; p_{4}; t_{2}; p_{1}; p_{2}; 3; 2; 2]

The firing sequence w = t_{1}t_{2}t_{2} from {p_{3} ↦ 1, p_{4} ↦ 3} to {p_{2} ↦ 4, p_{4} ↦ 2} on the innermost level enables one firing (w) from {p′_{3} ↦ 1, p′_{4} ↦ 3} to {p′_{2} ↦ 4, p′_{4} ↦ 2} on the next level, where the firing sequence w′ = (w)(w)t_{3}(w)t_{3}(w)t_{3}(w)t_{3} from {p′_{3} ↦ 2, p′_{4} ↦ 7} to {p′_{3} ↦ 5, p′_{4} ↦ 2} enables one firing (w′) from {p′′_{3} ↦ 2, p′′_{4} ↦ 7} to {p′′_{3} ↦ 5, p′′_{4} ↦ 2} on the following level, where the firing sequence w′′ = t_{4}(w′)t_{4}^{5} from {p′′_{3} ↦ 3, p′′_{4} ↦ 2} to {p′′_{4} ↦ 27} enables the firing of the out-most transition.

B The decision algorithm

In the following we describe a decision algorithm which reduces a nested Petri net not having the property T in every step. To prove its termination, we have to define an ordering on a size S, which is Noetherian and decreasing in every step of the algorithm: A list (tuple, respectively) is smaller than another if the first i elements are equal and the i + 1’th element is smaller or not existing. The smallest size is S(∅). Accordingly, T = ∅ trivially has the property T . The size S(T) of a set of transitions is a descending ordered list of the sizes S(t) of the transitions t ∈ T. The size of a transition is S(t) = S(K, c, Γ) := (S(K), b_{2}, b_{3}, b_{5}, |Γ|), where b_{i} is 0 if Condition T .i is fulfilled and otherwise 1. The size S(K) of a set of nets is a descending ordered list of the sizes S(P_{T}^{+}, T) of the nets (P_{T}^{+}, T) ∈ K. The size of a net is

S(P_{T}^{+}, T) := (Concatenation(J, [|non monotoneP_{T}^{+}|]), S(T), |P_{T} |)

with J := max{J′ | ∃g, f, e, d, c, b (J′, g, f) ∈ S(K′), (S(K′), e, d, c, b) ∈ S(T)} causing it to be greater than the size of its subnets. A place p ∈ P_{T} is called monotone if ∀t′ = (K′, c′, Γ′) ∈ T, g′ ∈ {c′} ∪ Γ′ ⇒ g′(+, p) = 0. Obviously, S(K′) < S(K) for a K′ contained one or more levels deeper in K.

Lemma B.1 The ordering on S defined above is Noetherian

Proof: According to [DM79] the set of descending ordered lists of elements of a Noetherian ordered set is again Noetherian. The first components of the triples S(P, T) are descending lists of natural numbers and thus Noetherian. Assume by contradiction that x is the smallest first component such that there is an infinite descending sequence of triples S(P, T) = (x, y_{1}, n_{1}), (x, y_{2}, n_{2}), .... In all triples appearing in all lists in all 5-tuples appearing in any y_{i}, the first component must always be smaller than x and therefore their order must be Noetherian. Thus, also the lists which are the first components of the 5-tuples, are ordered Noetherian. Since the other components are natural numbers, the 5-tuples and the y_{i}’s are also ordered Noetherian. Since the first component x must remain constant, and the third components are natural numbers, we get a contradiction and thus S(T) is Noetherian. Proof:(of Theorem 3.1) The set of transitions T′ in the Theorem is computed by the following algorithm, where the details are explained in the subsections:

function reacheq(T): begin

repeat i:= 1 while i≤5 and ∀t = (K, c, Γ) ∈ T, ∀N ∈ K Condition T .i fulfilled

do i:=i+1 od if i=6 then return T

else T:=T′ for T′ according to subsection B.i fi

until i=6 end reacheq

in each step S(T) decreases (S(reacheq(T)) < S(T) if T ≠ reacheq(T)); because of Lemma B.1 the algorithm terminates.

B.1 Condition 1

Let Condition 1 be not fulfilled by T_{i} where (P_{T_{i}}^{+}, T_{i}) ∈ K and t = (K, c, Γ) ∈ T. Let T′_{i} := reacheq(T_{i}), which terminates by induction since S(T_{i}) < S(T). Now we set t′ := ({(P_{T_{i}}^{+}, T′_{i})} ∪ K \ (P_{T_{i}}^{+}, T_{i}), c, Γ′) with Γ′ := Γ ∪ {{(+, p) ↦ 1}, {(−, p) ↦ 1} | p ∈ P_{T′_{i}} \ P_{T_{i}}} and T′ := {t′}∪T \{t}. Since R_{T_{i}} = R_{T′_{i}}|_{P_{T_{i}}×P_{T_{i}}}, we have R_{(P_{T_{i}}^{+},T_{i})} = R_{(P_{T′_{i}}^{+},T′_{i})}|_{P_{T_{i}}×P_{T_{i}}} thus

E_{t} = E_{t′}|\overline{(+,−)×(P_{T′_{i}}\P_{T_{i}})} thus R_{T} = R_{T′}. From S(T′_{i}) < S(T_{i}) it follows that S(T′) < S(T).

B.2 Condition 2

Let Condition 2 be not fulfilled by T_{i} where (P_{T_{i}}^{+}, T_{i}) ∈ K and t = (K, c, Γ) ∈ T. The set L :=

\{g ∈ ℤ^{\{+,−\}×(P_{T} ˙∪ ˙⋃_{(P{+ \atop T_{j}} ,T_{j})∈K} P_{T_{j}}} \begin{matrix}(g(+) − g_{ind}(−) + g_{ind}(+) − g(−))|_{P_{T_{i}}} = \overline{0} \\ g_{ind} = ∑_{{t′=(K′,c′,Γ′)∈T_{i}, \atop g′∈\{c′\}∪Γ′}}(g(+, p_{g′}) − g(−, p_{g′}))g′\} \end{matrix}

is a Presburger set. Using Presburger arithmetics [GS65],[ES69], we can calculate the semi-linear set

L ∩ (c + Γ^{∗}) =: ⋃_{j=1}^{l} c_{j} + Γ_{j}^{∗}

for some c_{j} and Γ_{j} and replace t by the l transitions t_{j} = (K, c_{j}, Γ_{j}) that means T′ := T \ {t} ∪ {t_{j} | j ≤ l}.

It is easy to see that E_{t} ⊆ ⋃_{j=1}^{l} E_{t_{j}} since E_{t} ⊆ L follows from the definition of E_{t} and

E_{t} ⊇ ⋃_{j=1}^{l} E_{t_{j}} because of the cut; thus E_{t} = ⋃_{j=1}^{l} E_{t_{j}} and therefore ER_{T′} = ER_{T}.

Since b_{2} is now 0 for each S(t_{j}) and S(K) remains the same, S(t_{j}) < S(t) holds for every j ≤ l and thus S(T′) < S(T).

B.3 Condition 3

Let G be the set of all g ∈ {c} ∪ Γ not fulfilling Condition 3. Add {p_{g′} | g ∈ G} to P_{T′} = P_{T} ∪ {p_{g′} | g ∈ G} by replacing the g’s in G by g′ := g + {(−, p_{g′}) ↦ 1} in T′ := T \ {t} ∪ {(K, c′, Γ′)} with Γ′ = Γ \ G ∪ {g′ | g ∈ G \ {c}} and c′ := c if c ∉ G. The new places are monotone and do not increase the size of K, Condition 2 is not affected, thus b_{2} stays 0; since b_{3} is now 0, it holds S(T′) < S(T).

B.4 Condition 4

Condition 4 is decidable by two covering graph constructions for every i working as follows: Every node in the covering graphs has a marking from (ℕ∪{ω})^{P_{T_{i}}}. The root of the covering graph CG_{(i,+)} (CG_{(i,−)}, respectively ) has the marking c(+)|_{Q_{i}^{+}} + ω^{P_{T_{i}}\Q_{i}^{+}} (c(−)|_{Q_{i}^{−}} +

ω^{P_{T_{i}}\Q_{i}^{−}}, respectively ).

For a node in CG_{(i,+)} marked with m we construct

T′_{i} := \{(K′, c_{1}, Γ_{1}), ..., (K′, c_{r}, Γ_{r}) | \begin{matrix}(K′, c′, Γ′) ∈ T_{i}, \\ (c′ + Γ^{′∗}) ∩ \{g | g(−)|_{P_{T_{i}}} ≤ m\} =: ⋃_{j=1}^{r} c_{j} + Γ_{j}^{∗}\} \end{matrix}

using Presburger arithmetics, which restricts the allowed firing sequences to those, which are possible starting with the limited marking m. Recursively we can compute T′′_{i} := reacheq(T′_{i}) since S(T′_{i}) < S(T) since S(K′) < S(K) because S(K′) is contained in S(K) and therefore max{J | ∃g, f (J, g, f) ∈ S(K)} is a concatenation of a number to a list J′′ ≥ max{J′ | ∃g, f (J′, g, f) ∈ S(K′)} and hence greater. For every (K′′, c′′, Γ′′) ∈ T′′_{i}, add a new node

m′ := m − c′′(−) + c′′(+) + ω Σ_{g∈Γ′′} g(+)|_{P_{T_{i}}}

to the covering graph CG_{(i,+)}. According to Lemma 3.1, there is no limit for the number of appearances of the multi-sets in Γ′′ in firing sequences, which allows to label those places p with ω, where g(+, p) > 0 for a g ∈ Γ′′. If m′ > m′′ for an m′′ on the path from the root to m, then we set m′ := m′ + ω(m′ − m′′), since we can lift the marking of those places p with (m′ − m′′)(p) > 0 by repeating the firing sequence corresponding to the path from m′′ to m′ arbitrarily many times. If m′ ≤ m′′ ∈ P ath(m′), then we need not calculate the successors of m′, since we already had better chances at m′′. Since according to [Dic13], there are only finite sets of incomparable multi-sets over a finite set P_{T_{i}}, every path must terminate. If for all i a node marked with ω^{P_{T_{i}}} is in CG_{(i,+)} and in CG_{(i,−)}, then the Condition 4 is fulfilled. Otherwise we can calculate w.l.o.g.

k := max_{path⊆CG_{(i,+)}} min_{p∈P_{T_{i}}} max_{m∈path} m(p)

This means that in every path in CG_{(i,+)} there is a place p such that on this path there are never more than k tokens on p. Now, we can replace in T′ := T \ {t} ∪ ⋃_{p∈P_{T_{i}}} U(p) the transition t by all those sets of

transitions U(p) which are generated by restricting t in such a way that, in the subnet (P_{T_{i}}^{+}, T_{i}), there can never be more than k tokens on p. In order to show that S(T′) < S(T) we have to show that each S(t′) < S(t) for every t′ in every U(p). Here, we consider two cases:

B.4.1 Elimination of monotone places

We have ∀t′′ = (K′′, c′′, Γ′′) ∈ T_{i} ∀g′′ ∈ {c′′} ∪ Γ′′ g′′(+, p) = 0 from the monotonicity of p. The set U(p) contains a new transition for every possible combination (including the or-

der of the summands) of g(+, p) = g(−, p) + ∑_{m=1}^{l} g_{m}(−, p) ≤ k with g ∈ c + {ĝ ∈ Γ |

ĝ(+, p) > 0 ∨ ĝ(−, p) > 0}^{∗}, g_{m} ∈ c_{i_{m}} + {g ∈ Γ_{i_{m}} | g(−, p) > 0}^{∗}, g_{m}(−, p) > 0 and t_{i_{m}} = (K_{i_{m}}, c_{i_{m}}, Γ_{i_{m}}) ∈ T_{i}.

In T′_{i} := {(K′′, c′′, Γ′′′) | (K′′, c′′, Γ′′) ∈ T_{i}, c′′(−, p) = 0, Γ′′′ = {g ∈ Γ′′ | g(−, p) = 0}} we filter out everything which affects p; thus P_{T′_{i}} = P_{T_{i}} \ {p} and P_{T′_{i}}^{+} = P_{T_{i}}^{+} \ {p}. Now we define the new transition t′ = (K′, c′, Γ′) ∈ U(p) with

K′ := K \ {(P_{T_{i}}^{+}, T_{i})} ∪ {Copy_{j}(P_{T′_{i}}^{+}, T′_{i}) | 0 ≤ j ≤ l} ∪ ⋃_{m=1}^{l} Copy′_{m}(K_{i_{m}})

where the subnets of the transitions causing the l affections of p are lifted to the level K′ and the net (P_{T′_{i}}^{+}, T′_{i}) is needed in l + 1 copies for the phases before, between and after the l affections of p. The constant multi-set of t is changed to c′ := g|\overline{\{+,−\}×P_{T_{i}}} +

Copy_{0}(g|_{\{+\}×P_{T_{i}}})+Copy_{l}(g|_{\{−\}×P_{T_{i}}})+ ∑_{m=1}^{l} Copy′_{m}(g_{m}|\overline{\{+,−\}×P_{T_{i}}})+Copy_{m−1}(g_{m}|_{\{+\}×P_{T_{i}}})+

Copy_{m}(g_{m}|_{{−}×P_{T_{i}}}) and

Γ′ := \begin{matrix}\{g′|\overline{\{+,−\}×P_{T_{i}}} + Copy_{0}(g′_{\{+\}×P_{T_{i}}}) + Copy_{l}(g′_{\{−\}×P_{T_{i}}}) | g′ ∈ Γ\} ∪ \\ \{\{(−, Copy_{j}(p)) ↦ 1, (+, Copy_{j+1}(p)) ↦ 1\} | p ∈ P_{T′_{i}}, 0 ≤ j < l\} ∪ \\ \{ \begin{matrix}Copy′_{m}(g′|\overline{\{+,−\}×P_{T_{i}}}) + Copy_{m−1}(g′|_{\{+\}×P_{T_{i}}}) + Copy_{m}(g′|_{\{−\}×P_{T_{i}}}) | \\ g′ ∈ Γ_{i_{m}}, g′(−, p) = 0, 1 ≤ m ≤ l\}. \end{matrix} \end{matrix}

It holds S(K′) < S(K) because of S(Copy_{j}(P_{T′_{i}}^{+}, T′_{i})) < S((P_{T_{i}}^{+}, T_{i})) for all 0 ≤ j ≤ l since |P_{T′_{i}}| = |P_{T_{i}}| − 1 and S(N) < S((P_{T_{i}}^{+}, T_{i})) for all N ∈ Copy′_{m}(K_{i_{m}}) and i ≤ l.

Example: Let t = ({({q}, {v, t_{j}})}, c, Γ) with t_{j} = ({({r}, {u})}, c_{j}, Γ_{j}) looking like

[figure: p; q; r; v; u; 2; 4; 5; 6; 7; 8; 9]

and c(+, p) = 2 = k means that the transition t_{j} can only fire twice (p = p_{c_{j}}). So there is only one possible combination g = c, l = 2, g_{1} = g_{2} = c_{j} and we get only one new transition t′ = ({Copy_{1}({r}, {v}), Copy′_{1}({q}, {u}), Copy_{2}({r}, {v}), Copy′_{2}({q}, {u}), Copy_{3}({r}, {v})}, c′, Γ′) looking like

[figure: q_{1}; r_{1}; q_{2}; r_{2}; q_{3}; v_{1}; v_{2}; v_{3}; u_{1}; u_{2}; 4; 5; 6+x; 6+y; 8; 8; 9; 9; 7+x; 7+y]

B.4.2 Elimination of non-monotone places

Like in the construction of a regular expression from a finite automaton having the states 0, ...k, we define for all l, j, h ≤ k the set T_{j,h}^{l−1} of transitions corresponding to firing sequences starting with a marking m_{0} with m_{0}(p) = j, ending with a marking m_{1} with m_{1}(p) = h and meanwhile always having less than l tokens on p. This means T_{j,h}^{−1} is constructed by calculating for every (K′, c′, Γ′) ∈ T_{i} the representation of the set

⋃_{l=1}^{r} c_{l} + Γ_{l}^{∗} := (c′ + Γ^{′∗}) ∩ {g | j − g(−, p) = h − g(+, p) ∈ ℕ}

using Presburger arithmetics and define

T_{j,h}^{−1} := Copy_{j,h}^{−1}(\{(K′, c_{l}|\overline{p}, Γ_{l}|\overline{p}) | (K′, c′, Γ′) ∈ T_{i}, l ≤ r\})

thus P_{T_{j,h}^{−1}} = Copy_{j,h}^{−1}(P′_{T_{i}}) with P′_{T_{i}} := P_{T_{i}} \ {p}).

Recursively we define T_{l,l}^{l} := {({(P_{T_{l,l}^{l−1}}, T_{l,l}^{l−1})}, ∅, Γ′′)} with Γ′′ :=

\{ \begin{matrix}\{(−, Copy_{l,l}^{l}(p)) ↦ 1, (+, Copy_{l,l}^{l−1}(p)) ↦ 1\}, \\ \{(−, Copy_{l,l}^{l−1}(p)) ↦ 1, (+, Copy_{l,l}^{l}(p)) ↦ 1\} | p ∈ P′_{T_{i}}\}, \end{matrix}

otherwise, for h ≠ l we define

T_{l,h}^{l} := {({(P_{T_{l,l}^{l−1}}, T_{l,l}^{l−1})} ∪ K_{2}, c′′, Γ′′) | (K_{2}, | Copy_{l,h}^{l−1}(ĉ), Γ̂) ∈ T_{l,h}^{l−1}}

with c′′ = Copy_{l,l}^{l−1}(ĉ|_{\{−\}×P_{T′_{i}}}) + Copy_{l,h}^{l−1}(ĉ|\overline{\{+,−\}×P_{T′_{i}}}) + Copy_{l,h}^{l}(ĉ|_{\{+\}×P_{T′_{i}}}) and Γ′′ =

\begin{matrix}\{\{(−, Copy_{l,h}^{l}(p)) ↦ 1), (+, Copy_{l,l}^{l−1}(p)) ↦ 1\} | p ∈ P′_{T_{i}}\}∪ \\ \{Copy_{l,l}^{l−1}(g′|_{\{−\}×P_{T′_{i}}}) + Copy_{l,h}^{l−1}(g′|\overline{\{+,−\}×P_{T′_{i}}}) + Copy_{l,h}^{l}(g′|_{\{+\}×P_{T′_{i}}}) | Copy_{l,h}^{l−1}(g′) ∈ Γ̂\} \end{matrix}

and analogously

\begin{matrix}T_{j,l}^{l} := \{(\{(P_{T_{l,l}^{l−1}}, T_{l,l}^{l−1})\} ∪ K_{1}, ..., ...) | (K_{1}, ..., ...) ∈ T_{j,l}^{l−1}\} for j ≠ l, else \\ T_{j,h}^{l} := T_{j,h}^{l−1} ∪ \{(\{(P_{T_{l,l}^{l−1}}, T_{l,l}^{l−1})\} ∪ K_{1} ∪ K_{2}, ..., ...) | (K_{1}, ..., ...) ∈ T_{j,l}^{l−1}, (K_{2}, ..., ...) ∈ T_{l,h}^{l−1}\}. \end{matrix}

Now we define U(p) :=

\{(K̂, ĉ, Γ̂) | \begin{matrix}K̂ = K \ \{(P_{T_{i}}^{+}, T_{i})\} ∪ K′′, \\ ĉ = c|\overline{\{+,−\}×P_{T_{i}}} + g′′|\overline{\{+,−\}×Copy_{c(+,p),c(−,p)}^{k}(P_{T_{i}})}, g′′ ∈ Γ′′, \\ Copy_{c(+,p),c(−,p)}^{k}(c(+)|_{P_{T_{i}}}) = g′′(−)|_{Copy_{c(+,p),c(−,p)}^{k}(P_{T_{i}})}, \\ Copy_{c(+,p),c(−,p)}^{k}(c(−)|_{P_{T_{i}}}) = g′′(+)|_{Copy_{c(+,p),c(−,p)}^{k}(P_{T_{i}})}, \\ Γ̂ = \{ \begin{matrix}g|\overline{\{+,−\}×P_{T_{i}}} + g′|\overline{\{+,−\}×Copy_{c(+,p),c(−,p)}^{k}(P_{T_{i}})} | g ∈ Γ, g′ ∈ Γ′′, \\ Copy_{c(+,p),c(−,p)}^{k}(g(+)|_{P_{T_{i}}}) = g′(−)|_{Copy_{c(+,p),c(−,p)}^{k}(P_{T_{i}})}, \\ Copy_{c(+,p),c(−,p)}^{k}(g(−)|_{P_{T_{i}}}) = g′(+)|_{Copy_{c(+,p),c(−,p)}^{k}(P_{T_{i}})}\} \end{matrix} \\ (K′′, ∅, Γ′′) ∈ T_{c(+,p),c(−,p)}^{k}\} . \end{matrix}

Since |nonmonotoneP_{T_{c(+,p),c(−,p)}^{k}}| = ... = |nonmonotoneP_{T_{j,h}^{−1}}| = |nonmonotoneP_{T_{i}}| − 1 we

have S(K′′) < S({(P_{T_{i}}^{+}, T_{i})}) because the first components of the 5-tuples in S(K′′) became longer but have smaller elements at the end. Thus S(K′, c′, Γ′) < S(t).

Example: Let t = ({({p} ∪ P^{+}, {v, w, t_{j}})}, c, Γ) with t_{j} = ({({p′} ∪ Q^{+}, {u})}, c, Γ) look like

[figure: p; p′; v; u; w; 8; 9]

and k = 1. This means that firing sequences are restricted to the regular expression ((wv^{∗}t_{j}) + v)^{∗}wv^{∗}. The new transition

t′ = (K′, c′, Γ′) with K′ = {(P_{1,1}^{+,0}, {v_{1,1}^{−1}, t̂}), (P_{0,0}^{+,0}, {v_{0,0}^{−1}})} ∪ K_{1,0}^{w,−1} with
t̂= (K̂, ĉ, Γ̂) with K̂ = K_{1,0}^{w,−1} ∪ {(P_{0,0}^{+,0}, {v_{0,0}^{−1}}), ({p′_{0,1}^{−1}} ∪ Q_{0,1}^{+,−1}, {u_{0,1}^{−1}})}

now looks like

[figure: v_{1,1}^{−1}; w_{1,0}^{−1}; w_{1,0}^{−1}; v_{0,0}^{−1}; v_{0,0}^{−1}; p′_{0,1}^{−1}; u_{0,1}^{−1}; 8; 9]

B.5 Condition 5

If Condition 5 is not fulfilled for = (K, c, Γ) then, according to Lemma 3.1 for e = ∅ and f = ∑_{g∈Γ} g, there exists a k such that (c + kf) ∈ E_{t}. Set T′ := T \ {t} ∪ {(K, c + kf, Γ)} ∪

{(K, c + jg, Γ \ {g}) | j ≤ k, g ∈ Γ}. Conditions 2 and 3 are not affected, thus, b_{2} and b_{3} stay 0. The size S((K, c + kf, Γ)) is smaller than S(t) since b_{5} is now zero and the other new transitions also have a smaller size because of |Γ \ {g}| < |Γ|; thus, it holds S(T′) < S(T).

C Building up compensating firing sequences

Proof:(of Lemma 3.1) For K = ∅, we have E_{t} = c+Γ^{∗} and the statement is easily fulfilled by choosing a sufficiently huge k. For every (P_{T_{i}}^{+}, T_{i}) ∈ K and for every t_{j} = (K_{j}, c_{j}, Γ_{j}) ∈ T_{i}, let

f_{j} := ∑_{g∈Γ_{j}} f(+, p_{g})g, e_{j} := ∑_{g∈Γ_{j}} e(+, p_{g})g and h_{j} := ∑_{g∈Γ_{j}} c(+, p_{g})g.

Let (c(+)|_{P_{T_{i}}} , c(+)|_{P_{T_{i}}} + Δ_{i}, α_{i}) ∈ ER_{(Q_{i}^{+},T_{i})} and (c(+)|_{P_{T_{i}}} + Δ′_{i}, c(+)|_{P_{T_{i}}} , α′_{i}) ∈ ER_{(Q_{i}^{−},T_{i})} according to Condition 4. Thus α_{i} ∈ E_{(Q_{i}^{+},T_{i})} = E_{T_{i}}^{∗} and α′_{i} ∈ E_{(Q_{i}^{−},T_{i})} = E_{T_{i}}^{∗}. We decompose α_{i} + α′_{i} =: ∑_{t_{j}∈T_{i}} −d_{j} such that −d_{j} ∈ E_{t_{j}}^{∗} for every j.

By Condition 1 and by applying the induction over the structure of nestedness three times for e as e_{j}, h_{j} or d_{j} there exist k_{j}, k′_{j}, k′′_{j} ≥ 2 with

(c_{j} + k_{j}f_{j}), (c_{j} + k′_{j}f_{j}), (c_{j} + k′_{j}f_{j}), (c_{j} + k_{j}f_{j} + e_{j}), (c_{j} + k′_{j}f_{j} + h_{j}), (c_{j} + k′′_{j}f_{j} + d_{j}) ∈ E_{t_{j}}.

Let Δ_{f,i} := f(+)|_{P_{T_{i}}} and Δ′_{f,i} := f(−)|_{P_{T_{i}}}. There exists a sufficiently large h ≥ 1 with hf + e ∈ ∑_{g∈Γ} g + Γ^{∗}, such that for all i and j

∀p ∈ P_{T_{i}}^{+}(hΔ_{f,i} + Δ_{i})(p) ≥ 1 ∧ (hΔ′_{f,i} + Δ′_{i})(s) ≥ 1,

h = n_{j}k_{j} = n′_{j}k′_{j} = n′′_{j}k′′_{j} for some n_{j}, n′_{j}, n′′_{j},

l_{j} := n_{j}(k_{j}f(+, p_{c_{j}}) − 1) + e(+, p_{c_{j}}) > 0,
n′_{j}(k′_{j}f(+, p_{c_{j}}) − 1) + c(+, p_{c_{j}}) > 0 and
n′′_{j}(k′′_{j}f(+, p_{c_{j}}) − 1) + (−α_{i} − α′_{i})(−, p_{c_{j}}) > 0.

Now we have ∑_{g∈{c_{j}}∪Γ_{j}} hf(+, p_{g})g = n_{j}((k_{j}f(+, p_{c_{j}}) − 1)c_{j} + (c_{j} + k_{j}f_{j})) ∈ E_{t_{j}}^{∗} according

to Condition 1 and 5. The same holds for

∑_{g∈{c_{j}}∪Γ_{j}}(hf + e)(+, p_{g})g =

n_{j}((k_{j}f(+, p_{c_{j}}) − 1)c_{j} + (c_{j} + k_{j}f_{j})) + e(+, p_{c_{j}})c_{j} + e_{j} =
l_{j}c_{j} + (n_{j} − 1)(c_{j} + k_{j}f_{j}) + (c_{j} + k_{j}f_{j} + e_{j}) ∈ E_{t_{j}}^{∗}.

Analogously we have

∑_{g∈{c_{j}}∪Γ_{j}}(hf + c)(+, p_{g})g ∈ E_{t_{j}}^{∗} and ∑_{g∈{c_{j}}∪Γ_{j}} hf(+, p_{g})g + d_{j} ∈ E_{t_{j}}^{∗}

and by combination of them we get ( ∑_{t_{j}∈T_{i},g∈{c_{j}}∪Γ_{j}}(2hf +c)(+, p_{g})g) = (2hf +c)_{ind} ∈ E_{T_{i}}^{∗} =

E_{(P_{T_{i}}^{+},T_{i})} and analogously (2hf + c + e)_{ind}, (hf_{ind} − α_{i} − α′_{i}) ∈ E_{T_{i}}^{∗} = E_{(P_{T_{i}}^{+},T_{i})}. According to Condition 2 and the definition of ER_{(P_{T_{i}}^{+},T_{i})}, there exists a sufficiently large l ≥ 0 such that for β = 2hf + c as well as for β = 2hf + c + e we have

(β(+)|_{P_{T_{i}}^{+}} + lhΔ_{f,i}, β(+)|_{P_{T_{i}}^{+}} + lhΔ_{f,i} + Δ_{i}, α_{i}),

(β(+)|_{P_{T_{i}}^{+}} + lhΔ_{f,i} + (l − 1)Δ_{i}, β(+)|_{P_{T_{i}}^{+}} + lhΔ_{f,i} + lΔ_{i}, α_{i}), (β(+)|_{P_{T_{i}}^{+}} + lhΔ_{f,i} + lΔ_{i}, β(−)|_{P_{T_{i}}^{+}} + lhΔ_{f,i} + lΔ_{i}, β_{ind}),

(β(−)|_{P_{T_{i}}^{+}} + l(hΔ_{f,i} + Δ_{i}), β(−)|_{P_{T_{i}}^{+}} + (l − 1)(hΔ_{f,i} + Δ_{i}) + hΔ′_{f,i} + Δ′_{i}, hf_{ind} − α_{i} − α′_{i}), (β(−)|_{P_{T_{i}}^{+}} + hΔ_{f,i} + Δ_{i} + (l − 1)(hΔ′_{f,i} + Δ′_{i}), β(−)|_{P_{T_{i}}^{+}} + l(hΔ′_{f,i} + Δ′_{i}), hf_{ind} − α_{i} − α′_{i}),

(β(−)|_{P_{T_{i}}^{+}} + lhΔ′_{f,i} + lΔ′_{i}, β(−)|_{P_{T_{i}}^{+}} + lhΔ′_{f,i} + (l − 1)Δ′_{i}, α′_{i}), (β(−)|_{P_{T_{i}}^{+}} + lhΔ′_{f,i} + Δ′_{i}, β(−)|_{P_{T_{i}}^{+}} + lhΔ′_{f,i}, α′_{i})

∈ ER_{(P_{T_{i}}^{+},T_{i})}, where the first two (and the last two, respectively) have the same fixed firing sequence from Condition 4, described by α_{i} (α′_{i}, respectively) and hf_{ind} − α_{i} − α′_{i} describes a fixed firing sequence from β(−)|_{P_{T_{i}}^{+}} + (l − 1)1^{P_{T_{i}}^{+}} + Δ_{i} to β(−)|_{P_{T_{i}}^{+}} + (l − 1)1^{P_{T_{i}}^{+}} + Δ′_{i}. With Lemma C.1 we get

(β(+)|_{P_{T_{i}}^{+}} + lhΔ_{f,i}, β(+)|_{P_{T_{i}}^{+}} + lhΔ_{f,i} + lΔ_{i}, lα_{i}), (β(+)|_{P_{T_{i}}^{+}} + lhΔ_{f,i} + lΔ_{i}, β(−)|_{P_{T_{i}}^{+}} + lhΔ_{f,i} + lΔ_{i}, β_{ind}), (β(−)|_{P_{T_{i}}^{+}} + l(hΔ_{f,i} + Δ_{i}), β(−)|_{P_{T_{i}}^{+}} + l(hΔ′_{f,i} + Δ′_{i}), l(hf_{ind} − α_{i} − α′_{i}) ), (β(−)|_{P_{T_{i}}^{+}} + lhΔ′_{f,i} + lΔ′_{i}, β(−)|_{P_{T_{i}}^{+}} + lhΔ′_{f,i}, lα′_{i}) ∈ ER_{(P_{T_{i}}^{+},T_{i})}.

Catenating them, we get

(β(+)|_{P_{T_{i}}^{+}} + lhΔ_{f,i}, β(−)|_{P_{T_{i}}^{+}} + lhΔ′_{f,i}, β_{ind} + lhf_{ind}) ∈ ER_{(P_{T_{i}}^{+},T_{i})}.

Let k := 2h + lh. Now we have ((c + kf)(+)|_{P_{T_{i}}^{+}} ), ((c + kf)(−)|_{P_{T_{i}}^{+}} ), (c + kf)_{ind}) ∈ ER_{(P_{T_{i}}^{+},T_{i})} and ((c + kf + e)(+)|_{P_{T_{i}}^{+}} ), ((c + kf + e)(−)|_{P_{T_{i}}^{+}} ), (c + kf + e)_{ind}) ∈ ER_{(P_{T_{i}}^{+},T_{i})} for all (P_{T_{i}}^{+}, T_{i}) ∈ K and thus (c + kf), (c + kf + e) ∈ E_{t}.

Lemma C.1 If (lm, (l − 1)m + m′, f), (m + (l − 1)m′, lm′, f) ∈ ER_{(P_{T}^{+},T)} having both the same fixed firing sequence, then (lm, lm′, lf) ∈ ER_{(P_{T}^{+},T)}.

Proof: Let min(m, m′) := {{p ↦ min(m(p), m′(p))} | p ∈ P_{T} } then, with the same fixed firing sequence, we have (min(lm, m + (l − 1)m′), min((l − 1)m + m′, lm′), f) ∈ ER_{(P_{T}^{+},T)}, by monotonicity, for all 0 ≤ j < l, we have

((l − j)m + jm′, (l − j − 1)m + (j + 1)m′, f) ∈ ER_{(P_{T}^{+},T)}

Catenating them, we get (lm, lm′, lf) ∈ ER_{(P_{T}^{+},T)}.

D Folding pushdown-stores into a nested Petri net

Formally, a restricted priority-multipushdown-automaton is a one-way automaton described by the 6-tuple

A = (k, Z, Σ, δ, z_{0}, E)

with the set of states Z = Z′ × {↑, ↓}^{k}, the input alphabet Σ, the transition relation

δ ⊆ (Z × (Σ ∪ {λ}) × {0 … k} × {λ, 0, 1}^{k}) × (Z × {λ, 0, 1}^{k}),

initial state z_{0}, the accepting states E ⊆ Z, the set of configurations C_{A} = Z × Σ^{∗} × ({0, 1}^{∗})^{k}, the initial configuration σ_{A}(x) = ⟨z_{0}, x, 0^{k}⟩ and configuration transition relation

⟨z, ax, g_{1}d_{1}, ..., g_{k}d_{k}⟩ |_{\overline{A}} ⟨z′, x, g_{1}i_{1}, ..., g_{k}i_{k}⟩

iff z, z′ ∈ Z, a ∈ Σ ∪ {λ}, ⟨(z, a, j, d_{1}, ..., d_{k}), (z′, i_{1}, ...i_{k})⟩ ∈ δ, z = (z′′, a_{1}, ..., a_{k}), z′ = (z′′′, a′_{1}, ..., a′_{k}), a_{j} =↑ ∨a′_{j} =↓ and

∀i < j g_{i} = λ ∧
∀i > j d_{i} ≠ 1 ∧ i_{i} ≠ 1 ∧ a_{i} = a′_{i} ∧
∀i ≤ k(a_{i} =↓ ∨d_{i} ≠ 1) ∧ (a′_{i} =↑ ∨i_{i} ≠ 1).

Furthermore, the condition d_{j} ≠ 0 ∧ i_{j} ≠ 0 can be established by creating an intermediate state and a smaller j in the second transition. Proof:(of Theorem 5.1) Given A, which has w.l.o.g. only one accepting configuration with all push-down stores empty and Σ = ∅, we add |Z′| push-down stores playing the role of the states (Only one of them has a zero and the others are empty.). This allows us to set Z = {↑, ↓}^{k}. Here the end state becomes the last push-down store and the start state the second last, thus w.l.o.g. the last 3 push-down stores never have a 1. Then, we construct a nested Petri net on 2k − 3 levels as follows: The innermost net (P_{T_{0}}, T_{0}) consists of all transitions

T_{0} := \{(∅, c_{t}, ∅) | \begin{matrix}t = ⟨(z, λ, 0, d_{1}, ..., d_{k}), (z, i_{1}, ...i_{k})⟩ ∈ δ ∧ \\ ∀i ≤ k (c_{t}(−, p_{i}^{0}) = 1 ↔ d_{i} = 0) ∧ (c_{t}(+, p_{i}^{0}) = 1 ↔ i_{i} = 0) \} \end{matrix}

pushing and popping only zeros. The net (P_{T′_{0}}, T′_{0}) is defined analogously with p′ instead of p. In general, the net on level 2h − 1 with 1 ≤ h ≤ k − 2 is (P_{T_{2h−1}}, T_{2h−1}) having the transitions T_{2h−1} := {t_{2h−1}} ∪

\{ (∅, c_{t,s}, ∅) | \begin{matrix}t = ⟨(z, λ, h, d_{1}, ..., d_{k}), (z, i_{1}, ...i_{k})⟩ ∈ δ ∧ \\ s = ⟨(z′, λ, h, d′_{1}, ..., d′_{k}), (z′, i′_{1}, ...i′_{k})⟩ ∈ δ ∧ \\ i_{h} = d′_{h} = 1 ∧ i′_{h} = d_{h} = λ ∧ \\ ∀h < i ≤ k (c_{t}(−, p_{i}^{2h−1}) = 1 ↔ d_{i} = 0) ∧ (c_{t}(+, p_{i}^{2h−1}) = 1 ↔ i_{i} = 0) ∧ \\ ∀h < i ≤ k (c_{t}(+, p_{i}^{2h−1}′) = 1 ↔ d_{i} = 0) ∧ (c_{t}(−, p_{i}^{2h−1}′) = 1 ↔ i_{i} = 0) \} \end{matrix}

with t_{2h−1} = ({(P_{T_{2h−2}}, T_{2h−2}), (P_{T′_{2h−2}}, T′_{2h−2})}, ∅, Γ_{2h−1}) with

Γ_{2h−1} = \{ \begin{matrix}\{(−, p_{h}^{2h−2}) ↦ 1, (+, p_{h}^{2h−2}) ↦ 1\}, \\ \{(−, p_{i}^{2h−1}) ↦ 1, (+, p_{i}^{2h−2}) ↦ 1\}, \\ \{(−, p_{i}^{2h−2}) ↦ 1, (+, p_{i}^{2h−1}) ↦ 1\}, \\ \{(−, p_{i}^{2h−1}′) ↦ 1, (−, p_{i}^{2h−2}′) ↦ 1\}, \\ \{(+, p_{i}^{2h−2}′) ↦ 1, (+, p_{i}^{2h−1}′) ↦ 1\} | h < i ≤ k \} \end{matrix}

and the net on level 2h with 1 ≤ h ≤ k−2 is (P_{T_{2h}}, T_{2h}) having the transitions T_{2h} := {t_{2h}} ∪

\{ (∅, c_{t}, ∅) | \begin{matrix}t = ⟨(z, λ, h + 1, d_{1}, ..., d_{k}), (z′, i_{1}, ...i_{k})⟩ ∈ δ ∧ \\ z = (a_{1}, ..., a_{h−1}, ↓, a_{h+1}, ..., a_{k}), z′ = (a′_{1}, ..., a′_{h−1}, ↑, a_{h+1}, ..., a_{k}), ∧ \\ ∀h < i ≤ k (c_{t}(−, p_{i}^{2h}) = 1 ↔ d_{i} = 0) ∧ (c_{t}(+, p_{i}^{2h}) = 1 ↔ i_{i} = 0) ∧ \\ ∀h < i ≤ k (c_{t}(+, p_{i}^{2h}′) = 1 ↔ d_{i} = 0) ∧ (c_{t}(−, p_{i}^{2h}′) = 1 ↔ i_{i} = 0) \} \end{matrix}

with t_{2h} = ({(P_{T_{2h−1}}, T_{2h−1})}, ∅, Γ_{2h}) with

Γ_{2h} = \{ \begin{matrix}\{(−, p_{i}^{2h}) ↦ 1, (+, p_{i}^{2h−1}) ↦ 1\}, \\ \{(−, p_{i}^{2h−1}) ↦ 1, (−, p_{i}^{2h−1}′) ↦ 1\}, \\ \{(+, p_{i}^{2h−1}′) ↦ 1, (+, p_{i}^{2h}) ↦ 1\} | h < i ≤ k \} \end{matrix}

The net (P_{T′_{2h}}, T′_{2h}) is defined analogously with p′ instead of p. On the top level 2k − 4 we have T_{2k−4} := {t_{2k−4}} with

t_{2k−5} = ({(P_{2k−5}, T_{2k−5})}, {(+, p_{k−1}^{2k−5}) ↦ 1, (+, p_{k}^{2k−5}′) ↦ 1}, Γ_{2k−4})

with Γ_{2k−4} = { {(−, p_{i}^{2k−5}) ↦ 1, (0, p_{i}^{2k−5}′) ↦ 1} | k − 3 < i ≤ k }. Now, if we have a sequence w ∈ δ^{∗} of transitions of A leading from the start- to an end configuration, then 1’s are only pushed or popped from the first k − 3 push-down stores and we have to show that there is an η ∈ Γ_{2k−4}^{∗} such that ({(+, p_{k−1}^{2k−5}) ↦ 1, (+, p_{k}^{2k−5}′ ↦ 1}, η) ∈ R_{(P_{2k−5},T_{2k−5})} and thus (∅, ∅) ∈ R_{T_{2k−4}}. By induction over h, we consider w ∈ {⟨(z, λ, j, d_{1}, ..., d_{k}), (z′, i_{1}, ...i_{k})⟩ ∈ δ | j ≤ h}^{∗} be a sequence of transitions of A such that in the corresponding sequence of configurations 1’s are only pushed or popped from the first h push-down stores and that they are empty in the first and the last configuration. Then, the direction of a_{h} cannot be changed from ↓ to ↑ according to the definition. Thus w can be decomposed in v_{1}t_{1}v_{2}t_{2}...v_{n}w_{n}...s_{2}w_{2}s_{1}w_{1} = w such that t_{1} (s_{1}, respectively) with i < n is a transition in δ with j = h and i_{j} = 1 (d_{j} = 1, respectively) and the v_{i} and w_{i} are sequences of transitions in δ^{∗} where no 1 is pushed or popped to the h’th push-down store. Each of the v_{i} or w_{i} can be decomposed into minimal sequences w′_{1}t′_{1}w′_{2}t′_{2}...w′_{m} each starting and ending with the first h − 1 push-down stores empty and the t′_{i} are those transitions where the push-down store number h − 1 is switched from popping to pushing, that means a_{j} =↑ ∧a′_{j} =↓. The w′_{i} now have the same property as w with h := h − 1. For h = 0 a sequence w ∈ {⟨(z, λ, 0, d_{1}, ..., d_{k}), (z′, i_{1}, ...i_{k})⟩ ∈ δ}^{∗} corresponds to a path in R_{(P_{T_{0}},T_{0})}. By induction we assume that for every w′_{i} we have a corresponding path in R_{(P_{T_{2h−1}},T_{2h−1})} and thus a corresponding firing of t_{2h}. Furthermore, for every t′_{i}, we have a corresponding firing of (∅, c_{t′_{i}}, ∅). Thus for every v_{i} and w_{i}, respectively, we have a corresponding path in R_{(P_{T_{2h}},T_{2h})} and R_{(P_{T{′ \atop 2h}},T′_{2h})}, respectively, together they enable a corresponding firing of t_{2h+1}. Furthermore, for every pair t_{i}, s_{i} we have a corresponding firing of (∅, c_{t_{i},s_{i}}, ∅). Thus for w we have a corresponding path in R_{(P_{T_{2h+1}},T_{2h+1})}, which completes the induction. For the other direction, if (∅, ∅) ∈ R_{T_{2k−4}}, the composing the corresponding transitions in the appropriate way leads from the start to the end configuration.