=Paper=
{{Paper
|id=Vol-2907/paper7
|storemode=property
|title=The Reachability Problem for Acyclic Join-Free Petri nets is NP-complete
|pdfUrl=https://ceur-ws.org/Vol-2907/paper7.pdf
|volume=Vol-2907
|authors=Ronny Tredup,Sophie Wallner
|dblpUrl=https://dblp.org/rec/conf/apn/TredupW21
}}
==The Reachability Problem for Acyclic Join-Free Petri nets is NP-complete==
https://ceur-ws.org/Vol-2907/paper7.pdf
The Reachability Problem for Acyclic Join-Free
Petri nets is NP-complete
Ronny Tredup and Sophie Wallner
Universität Rostock, Institut für Informatik
ronny.tredup@uni-rostock.de
sophie.wallner@uni-rostock.de
Abstract. The reachability problem for Petri nets is the task to decide,
for a given Petri net N and a marking m, whether m can be reached from
the initial configuration of N by firing a valid sequence of transitions.
In this paper, we show that the reachability problem for acyclic join-free
Petri nets is NP-complete.
1 Introduction
The concept of Petri nets goes back to Carl Adam Petri [5, 24] and has been fur-
ther developed in the following years, particularly by the contributions of Anatol
Holt [15] and the group around him. Today, Petri nets are a well-established
language for modeling concurrent processes and distributed systems. Different
dialects of Petri nets and their extensions such as, for example, 1-safe Petri nets,
colored Petri nets or timed Petri nets, have applications in several areas such as,
for example, performance evaluation [27]; communication protocols [3, 26]; mod-
eling and analysis of distributed software systems [19, 25]; synthesis of speed
independent asynchronous cicuits [13]; modeling and verification in hardware
design [2, 7].
Petri net analysis deals, for example, with the task to deduce behavioral
properties of the model like reachability, liveness or deadlock, and is subject of
a dedicated annual contest [1].
In this paper, we deal with a special instance of a central algorithmic problem
of Petri net analysis: The reachability problem for Petri nets is the task to decide,
for a given Petri net N and a marking m, whether m is reachable from the initial
configuration of N by firing a sequence of transitions of N .
In theoretical computer science, this problem has been investigated for many
years from both the computability and the complexity point of view: while the
decidability status of the problem has been open for a long time, it was fi-
nally shown in [21] that a decision algorithm exists, and several works aimed at
improved and less complex decision methods [18, 20]. Unfortunately, the reach-
ability problem for Petri nets is intrinsically hard to solve: while its was already
Copyright © 2021 for this paper by its authors. Use permitted under Creative
Commons License Attribution 4.0 International (CC BY 4.0).
124 Ronny Tredup and Sophie Wallner
proven to be EXPSPACE-hard in [6], a recent work showed that the problem
needs even a tower of exponentials of time and space [8].
However, from the complexity point of view, better results can be obtained for
structural restricted Petri nets: for example, the complexity of the reachability
problem boils down to PSPACE-complete for 1-safe Petri nets; the problem is
NP-complete for acyclic Petri nets [4], for acyclic 1-safe Petri nets [28], and for
conflict-free Petri nets [16] as well. On the other hand, the reachability problem is
solvable in polynomial-time for S-systems and marked graphs [14, 5], and 1-safe
conflict-free Petri nets [4].
Free-choice Petri nets define one of the most important sub-classes of Petri
nets. The reachability problem generally remains EXPSPACE-hard for these
nets, but becomes PSPACE-complete for 1-safe free-choice Petri nets, and it is
NP-complete for live 1-safe free-choice Petri nets [12]. Moreover, the problem
is polynomial for reversible free-choice Petri nets [10], and for cyclic extended
free-choice systems [11], and for sound extended free-choice workflow nets [30].
Join-free Petri nets build a particular yet useful subclass of Petri nets and
allow every transition to have at most one input place [9, 17, 29]. To the best
of our knowledge, the complexity status of the reachability problem has not
yet been characterized for this class. In this paper, we partially close this gap
by showing that the reachability problem for acyclic join-free Petri nets is NP-
complete: On the one hand, the problem inherits NP-membership from the more
general class of acyclic Petri nets [28]. On the other hand, we show by a reduction
of a particular Sat-problem, namely Cubic Monotone 1 in 3 3Sat, that the
reachability problem for acyclic join-free Petri nets is NP-hard, even if the the
net is additionally free-choice, that is, its arc weights are restricted to zero and
one.
The paper is structured as follows: The next Section 2 provides basic defini-
tions and supports them with some examples. After that, Section 3 provides the
announced hardness result. Finally, Section 4 briefly closes the paper.
2 Preliminaires
In this section, we introduce relevant basic notions around Petri nets and show
some examples.
Definition 1 (Petri Nets). A Petri net, also Petri net, N = (P, T, f, m0 )
consists of finite and disjoint sets of places P and transitions T , a (total) flow
f : ((P × T ) ∪ (T × P )) → N and an initial marking m0 : P → N.
Definition 2 (Preset, postset). The nodes of a Petri net N = (P, T, f, m0 )
are P ∪ T . The preset of a node x is defined by •x = {y | f (y, x) > 0}, the
postset of x is defined by x• = {y | f (x, y) > 0}. Notice that •x ∩ x• is not
necessarily empty. For a transition t, the pre-places are all places in •t; the
post-places are all places in t•. Pre-transitions and post-transitions for a place
are defined analogously.
The Reachability Problem for Acyclic Join-Free Petri nets is NP-complete 125
Subclasses of Petri nets. Within the class of Petri nets, we can determine
various subclasses, which differ in their flow relation structure: A Petri net
N = (P, T, f, m0 ) is called acyclic if its underlying directed graph G = (V, E)
with vertices V = P ∪ T and edges E = {(x, y) | x, y ∈ V, f (x, y) > 0} has
no directed circuits. Moreover, N is join-free, if every transition t has at most
one pre-place, that is, | • t| ≤ 1. If the co-domain of the flow f is restricted
to {0, 1}, then N is called plain. Furthermore, N is free-choice, if it is plain
and, additionally, if it holds for two arbitrary distinct transitions t and t0 ∈ T :
•t ∩ •t0 6= ∅ ⇒ •t = •t0 . This means that if two transitions share one pre-place,
then they share all pre-places. Notice that a plain join-free Petri net is free-choice
by triviality, since in this case there is no transition with several pre-places.
Figure 1 shows the net N that is obviously acyclic and join-free and free-
choice as well.
p1
t1
p0 p3
t0
p2
t2
Fig. 1. The acyclic, join-free Petri net N , which is also free-choice.
The behavior of a Petri net is defined by the transition rule.
Definition 3 (Transition Rule). Let N = (P, T, f, m0 ) be a Petri net. Tran-
sition t is enabled in marking m if ∀p : m(p) ≥ f (p, t). Firing a Transition
t leads from marking m to marking m0 if t is enabled in m and ∀p : m0 (p) =
t
− m0 .
m(p) − f (p, t) + f (t, p), denoted as m →
Definition 4 (Firing Sequence, Reachability Set). Let N = (P, T, f, m0 )
be a Petri net and m, m0 some (not necessarily distinct) markings of N . We say
a sequence (of transitions) σ = ω ∈ T ∗ can fire at m and its firing leads to m0 ,
σ
denoted by m − → m0 if and only if either σ = ε and m = m0 or σ = ωa, where
ω
ω ∈ T ∗ and a ∈ T , and there is a marking m00 of N such that m − → m00 and
a σ
m00 −
→ m0 . We call RS(N ) = {m | ∃σ ∈ T ∗ : m0 − → m} the reachability set (of
N ), which contains all of N ’s reachable markings.
Definition 5 (Set of transitions of a sequence). Let N = (P, T, f, m0 ) be
a Petri net and let σ ∈ T ∗ . We define the set Sσ of transitions of σ inductively
as follows: If σ = ε, then Sσ = ∅ and, otherwise, if σ = ωa with ω ∈ T ∗ and
a ∈ T , then Sσ = {a} ∪ Sω .
Using the transition rule, a Petri net induces a labeled transition system,
called the reachability graph.
126 Ronny Tredup and Sophie Wallner
Definition 6 (Labeled Transition System, Reachability Graph). A (de-
terministic) transition system T S = [S, s0 , R, A] is a directed labeled graph with
the set of nodes S (called states), an initial state s0 ∈ S, and a transition re-
lation R ⊆ S × A × S with some set of actions A. The reachability graph of a
Petri net N is a transition system, where the set of states is RS(N ), m0 serves
t
as the initial state and (m, t, m0 ) ∈ R iff m →
− m0 .
In this paper, we consider the following instance of the reachability problem:
Reachability For Acyclic Join-Free Petri Nets
Input: A tuple (N, m) where N = (P, T, f, m0 ) is an acyclic and join-free
Petri net and m is a marking of N .
σ
Question: Does there exist a firing sequence σ ∈ T ∗ such that m0 − → m?
An example shall illustrate this problem.
Example 1. Let N be the given net in Figure 1 with the initial marking m0 =
(1, 0, 0, 0) whereas, with a little abuse of definition, the tuple is an abbreviation of
m0 (pH0 ) = 1, m0 (pH1 ) = m0 (pH2 ) = m0 (pH3 ) = 0. In m0 , only t0 is activated.
Firing t0 leads to marking m1 = (0, 1, 1, 0). The marking m2 = (0, 0, 0, 2) is
reachable, because the firing sequence t0 t1 t2 leads us from m0 to m2 . On the
contrary, marking m3 = (1, 0, 0, 1) is not reachable, as for producing tokens on
pH3 , we need to consume the token from pH0 first to activate the transition t1
and t2 .
3 Hardness Result
The following theorem provides the main result of this paper:
Theorem 1. Reachability for Acyclic Join-free Petri Nets is NP-
complete.
The remainder of this paper is dedicated to the proof of Theorem 1: First
of all, by a result of [23], if N = (P, T, f, m0 ) is an acyclic Petri net and m a
marking, then m is reachable from m0 if and only if the well-known state equa-
tion m = m0 + C · x has a non-negative integer solution x. In other words, the
reachability problem is reducible to the problem Linear Integer Program-
ming, which is well-known to be NP-complete. Hence, the reachability problem
for acyclic join-free Petri nets belongs to NP.
Consequently, in order to complete the proof of Theorem 1, it remains to
show that Reachability for Acyclic Join-free Petri Nets is NP-hard.
The proof of the NP-hardness is based on a polynomial-time reduction of the
following particular Sat-problem, which is known to be NP-complete from [22]:
The Reachability Problem for Acyclic Join-Free Petri nets is NP-complete 127
Cubic Monotone 1 in 3 3Sat (CM 1 in 3 3Sat)
Input: A pair (V, F ) consisting of a set V of boolean variables and a
set F = {C0 , . . . , Cn−1 } consisting of 3-variable-clauses, such
that Ci = {Xi0 , Xi1 , Xi2 } ⊆ V and i0 < i1 < i2 for all
i ∈ {0, . . . , n − 1}. Every variable X ∈ V appears in exactly
three different clauses.
Question: Does there exist a one-in-three model for (V, F ), i.e. a set S ⊆ V
such that |S ∩ Ci | = 1 for all i ∈ {0, . . . , n − 1}?
Example 2. The instance (V, F ) of CM 1 in 3 3Sat with set of variables
V = {X0 , X1 , . . . , X5 } and set of 3-variable-clauses F = {C0 , C1 , . . . , C5 }, where
– C0 = {X0 , X1 , X2 } – C3 = {X2 , X3 , X4 }
– C1 = {X0 , X1 , X3 } – C4 = {X2 , X4 , X5 }
– C2 = {X0 , X1 , X5 } – C5 = {X3 , X4 , X5 }
allows a positive decision, since S = {X0 , X4 } is a one-in-three model for (V, F ).
Notice that the number of variables and the number of clauses are equal for
any arbitrary instance of CM 1 in 3 3Sat. This concludes from the problem
definition of CM 1 in 3 3Sat, as every variable occurs exactly in three different
clauses and each clause consists of three different variables.
In the remainder of this paper, unless explicitly stated otherwise, let (V, F ) be
an arbitrary but fixed input of CM 1 in 3 3Sat, where V = {X0 , X1 , . . . , Xn−1 }
and F = {C0 , C1 , . . . , Cn−1 } such that Ci = {Xi0 , Xi1 , Xi2 } and i0 < i1 < i2 for
all i ∈ {0, . . . , n − 1}.
Our reduction uses the following simple yet crucial fact:
Fact 1. If S ⊆ V is a one-in-three model for F , then |S| = n3 .
Proof. Let S be a one-in-three model for F . Since every variable of V occurs in
exactly three distinct clauses and, moreover, |S ∩Ci | = 1 for all i ∈ {0, . . . , n−1},
we have that |F | = 3|S|. This implies |S| = n3 .
The reduction. In order to prove the hardness part of Theorem 1, we trans-
late the instance (V, F ) into an input (N, m) of Reachability for Acyclic
Join-free Petri Nets such that there is a one-in-three model for (V, F ) if and
only if m is reachable from the initial marking of N .
For the Petri net N , we introduce the following components:
– for every i ∈ {0, . . . , n − 1}, the place pCi that represents the clause Ci and
is initially marked by one token: m0 (pCi ) = 1;
– for every i ∈ {0, . . . , n − 1}, the initially empty place pXi : m(pXi ) = 0;
– for every i ∈ {0, . . . , n − 1}, three transitions t0Xi , t1Xi and t2Xi that represent
the three occurrences of the variable Xi in the clauses of F : if C`0 , C`1 , C`2
with `0 < `1 < `2 ∈ {0, . . . , n − 1} are exactly the clauses that contain Xi ,
then, for all j ∈ {0, 1, 2}, it is pC`j the unique pre-place of the transition tjXi ,
128 Ronny Tredup and Sophie Wallner
where f (pC`j , tjXi ) = 1; moreover, for all j ∈ {0, 1, 2}, the place pXi is the
only post-place of tjXi , where f (tjXi , pXi ) = 1;
– for every i ∈ {0, . . . , n − 1}, three other helper-transitions t0Hi , t1Hi , t2Hi and
two helper-places pHi and qHi , such that
• f (t0Hi , pHi ) = 1 and f (t0Hi , pXi ) = 1,
• f (pHi , t1Hi ) = 1 and f (t1Hi , qHi ) = 1 and f (t1Hi , pXi ) = 1,
• f (qHi , t2Hi ) = 1 and f (t2Hi , pXi ) = 1,
• m(pHi ) = m(qHi ) = 0.
The reduction yields the Petri net N = (P, T, f, m0 ) with places and transitions
as follows:
P = {pC0 , pC1 , . . . , pCn−1 } ∪ {pX0 , pX1 , . . . , pXn−1 } ∪ {pH0 , qH0 , . . . , pHn−1 , qHn−1 },
T = {t0X0 , t1X0 , t2X0 , t0X1 , t1X1 , t2X1 , . . . , t0Xn−1 , t1Xn−1 , t2Xn−1 }
∪ {t0H0 , t1H0 , t2H0 , t0H1 , t1H1 , t2H1 , . . . , t0Hn−1 , t1Hn−1 , t2Hn−1 }.
Notice that the resulting net is plain and thus also free-choice. Let the mark-
ing m, whose reachability is shown to be equivalent to the existence of a one-
in-three model for (V, F ), be defined by m(pX0 ) = · · · = m(pXn−1 ) = 3 and
m(p) = 0 for all p ∈ P \ {pX0 , . . . , pXn−1 }.
The following example will make the reduction technique more clear:
Example 3. For the instance (V, F ) of CM 1 in 3 3Sat presented in Example 2,
we build the Petri net N , illustrated in Figure 2.
pC0 pC1 pC 2 pC3 pC4 pC5
t0X0 t1X0 t2X0 t0X1 t1X1 t2X1 t0X2 t1X2 t2X2 t0X3 t1X3 t2X3 t0X4 t1X4 t2X4 t0X5 t1X5 t2X5
p X0 p X1 p X2 pX3 p X4 p X5
t0H0 t1H0 t2H0 t0H1 t1H1 t2H1 t0H2 t1H2 t2H2 t0H3 t1H3 t2H3 t0H4 t1H4 t2H4 t0H5 t1H5 t2H5
pH 0 qH0 pH 1 q H1 pH 2 qH2 pH3 qH3 pH 4 qH4 pH 5 qH5
Fig. 2. The Petri net N according to the reduction for the CM 1 in 3 3Sat-instance
of Example 2.
In the following, we argue that the reduction actually satisfies the function-
ality introduced. The following lemma proves that if (V, F ) allows a positive
decision, then so does (N, m):
Lemma 1. If there is a one-in-three model for F , then m is a reachable marking
of N .
The Reachability Problem for Acyclic Join-Free Petri nets is NP-complete 129
Proof. Recall that any one-in-three model for F has exactly n3 elements by
Fact 1. Let i0 , . . . , i n3 −1 ∈ {0, . . . , n − 1} be n3 pairwise distinct indices, such
that S = {Xi0 , . . . , Xi n −1 } is a one-in-three model for F , that is, for all i ∈
3
{0, . . . , n − 1}, it holds S ∩ Ci = {Xi` } for some ` ∈ {0, . . . , n3 − 1}. Moreover,
let j0 , . . . , j 2n
3 −1
∈ {0, . . . , n − 1} be the 2n
3 pairwise distinct indices such that
{Xj0 , . . . , Xj 2n −1 } = V \ S. We now show, that the marking m is reachable from
3
the marking m0 of N by a firing sequence, which can be derived from S. Initially,
only the clause places pC0 , . . . , pCn−1 are marked with one token each. Therefore,
for every ` ∈ {0, . . . , n3 − 1}, the transitions t0Xi , t1Xi , t2Xi , which represent the
` ` `
occurrences of the variable Xi` in the clauses of F , are all activated. Since S
is a one-in-three model, for all j, ` ∈ {0, . . . , n3 − 1} and all h, k ∈ {0, 1, 2}, the
following is true: if (j, h) 6= (`, k), then •tXih ∩ •tXik = ∅. Hence, the following
j `
sequence can fire at m0 (and results in the marking m1 , defined below):
σ1 = t0Xi0 t1Xi0 t2Xi0 t0Xi1 t1Xi1 t2Xi1 . . . t0Xi n t1Xi n t2Xi n
−1 −1 −1
| {z } | {z } | 3 {z3 3
}
m1 (pXi )=3 m1 (pXi )=3
0 1 m1 (pXi n )=3
−1
3
For all ` ∈ {0, . . . , n3 − 1} and all j ∈ {0, 1, 2}, firing tjXi consumes the only
`
token from its unique pre-place and produces exactly one token on its unique
post-place pXi` . Consequently, firing the transition sequence σ1 leads from m0 to
the marking m1 , such that m1 (pXi` ) = 3 for all ` ∈ {0, . . . , n3 −1} and m1 (p) = 0
for all other places p ∈ P \ {pXi0 , . . . , pXi n −1 }.
3
In order to obtain m, we extend σ1 by the sequence
σ2 = t0Hj0 t1Hj0 t2Hj0 t0Hj1 t1Hj1 t2Hj1 . . . t0Hj 2n t1Hj 2n t2Hj 2n
−1 −1 −1
| {z } | {z } | 3 {z3 3
}
m(pXj )=3 m(pXj )=3
0 1 m(pXj )=3
2n −1
3
It is easy to see, that σ2 can be fired at m1 , since t0Hj does not have a pre-place
`
for all ` ∈ {0, . . . , 2n 2n
3 − 1}. Moreover, for every ` ∈ {0, . . . , 3 − 1}, the firing
0 1 2
of the subsequence tHj tHj tHj does nothing else than to put three tokens on
` ` `
pXj` : t0Hj puts a token on pHj` and a token on pXj` ; after that t1Hj consumes
` `
the token from pHj` and puts a token on qHj` and another one on pXj` ; finally,
t2Hj consumes the token from qHj` and puts a third token on pXj` . In particular,
`
σ σ
m0 −−1−→
2
m, which proves the lemma.
Conversely, by the following lemma, if (N, m) is a yes-instance, then (V, F )
is a yes-instance as well:
Lemma 2. Let σ ∈ T ∗ be a firing sequence of N that leads to the marking m
and let i ∈ {0, . . . , n − 1} be arbitrary but fixed.
1. If t0Hi ∈ Sσ , then tjXi 6∈ Sσ for all j ∈ {0, 1, 2}.
130 Ronny Tredup and Sophie Wallner
2. If there is j ∈ {0, 1, 2} such that tjXi ∈ Sσ , then t0Xi , t1Xi , t2Xi ∈ Sσ .
3. The set S = {Xi | t0Xi , t1Xi , t2Xi ∈ Sσ } defines a one-in-three model for F .
Proof. (1): The transition t0Hi puts a token on pHi and a token on pXi . Since
m(pHi ) = 0 and pHi • = {t1Hi }, we have that t1Hi ∈ Sσ . Similarly, transition t1Hi
puts a token on qHi and on pXi and as well. Since m(qHi ) = 0 and qHi • = {t2Hi },
the transition t2Hi occurs in σ. Finally, since the firing of t2Hi puts a token on
pXi , and pXi • = ∅, and m(pXi ) = 3, we have that •pXi ∩ Sσ = {t0Hi , t1Hi , t2Hi }.
This implies the claim.
(2): Since tjXi ∈ Sσ , by (1), we have that t0Hi 6∈ Sσ , which certainly implies
tHi 6∈ σ and t2Hi 6∈ σ. Hence, by m(pXi ) = 3, we have that every of the transitions
1
t0Xi , t1Xi and t2Xi has put a token on pXi , which implies the claim.
(3): Recall that the i-th clause is given by Ci = {Xi0 , Xi1 , Xi2 }. Since
m(pCi ) = 0, there are j ∈ {0, 1, 2} and k ∈ {0, 1, 2}, such that tkXi ∈ Sσ .
j
By (2), this implies t0Xi , t1Xi , t2Xi ∈ Sσ and thus Xij ∈ Ci ∩ S. In particular,
j j j
we have that S ∩ Ci 6= ∅.
If |Ci ∩ S| ≥ 2, then there are distinct j, ` ∈ {0, 1, 2} such that Xij , Xi` ∈ C ∩
S. By definition of S, this implies t0Xi , t1Xi , t2Xi ∈ Sσ and t0Xi , t1Xi , t2Xi ∈ Sσ
j j j ` ` `
and, by the construction of N , this implies |pCi • ∩Sσ | ≥ 2 as well. This is a
contradiction, since m0 (pCi ) = 1 and •pCi = ∅ and f (pCi , t) = 1 for all t ∈ pCi •.
Consequently, |Ci ∩ S| = 1.
Finally, by the arbitrariness of i, we have that |Ci ∩ S| = 1 for all i ∈
{0, . . . , n − 1}, which proves the claim.
Since the reduction is obviously polynomial and Reachability for Acyclic
Join-free Petri Nets belongs to NP, by Lemma 1 and Lemma 2, we have
proven Theorem 1.
4 Conclusion
In this paper, we show that the well-known reachability problem of Petri nets
is NP-complete for the class of acyclic join-free Petri nets, which are also free-
choice. The hardness-proof bases on the reduction of a particular SAT-problem.
The membership in NP heavily bases on the fact that the nets addressed are
acyclic. Hence, it remains future work to determine the complexity of the reach-
ability problem for join-free Petri nets that may contain cycles.
Acknowledgements. We would like to thank the anonymous reviewers for
their detailed comments and valuable suggestions. In particular, we thank the
reviewer for the hint that improved the original reduction, which provided an
acyclic join-free Petri net with general arc weights, instead of the current plain
net.
The Reachability Problem for Acyclic Join-Free Petri nets is NP-complete 131
References
1. Amparore, E.G., Berthomieu, B., Ciardo, G., Dal-Zilio, S., Gallà, F., Hillah, L.,
Hulin-Hubard, F., Jensen, P.G., Jezequel, L., Kordon, F., Botlan, D.L., Liebke, T.,
Meijer, J., Miner, A.S., Paviot-Adet, E., Srba, J., Thierry-Mieg, Y., van Dijk, T.,
Wolf, K.: Presentation of the 9th edition of the model checking contest. In: TACAS
(3). Lecture Notes in Computer Science, vol. 11429, pp. 50–68. Springer (2019)
2. Azéma, P., Valette, R., Diaz, M.: Petri nets as a common tool for design verification
and hardware simulation. In: Humcke, D.J., Galey, J.M., Szygenda, S.A., Pistilli,
P.O., Dooner, N.P., Brinsfield, J.G., Olila, J.S. (eds.) Proceedings of the 13th
Design Automation Conference, DAC ’76, San Francisco, California, USA, June
28-30, 1976. pp. 109–116. ACM (1976). https://doi.org/10.1145/800146.804803,
https://doi.org/10.1145/800146.804803
3. Berthelot, G., Terrat, R.: Petri nets theory for the cor-
rectness of protocols. IEEE Trans. Commun. 30(12), 2497–
2505 (1982). https://doi.org/10.1109/TCOM.1982.1095452,
https://doi.org/10.1109/TCOM.1982.1095452
4. Cheng, A., Esparza, J., Palsberg, J.: Complexity results for 1-safe nets. In:
Shyamasundar, R.K. (ed.) Foundations of Software Technology and Theoretical
Computer Science, 13th Conference, Bombay, India, December 15-17, 1993, Pro-
ceedings. Lecture Notes in Computer Science, vol. 761, pp. 326–337. Springer
(1993). https://doi.org/10.1007/3-540-57529-4 66, https://doi.org/10.1007/3-540-
57529-4 66
5. Commoner, F., Holt, A.W., Even, S., Pnueli, A.: Marked directed graphs.
J. Comput. Syst. Sci. 5(5), 511–523 (1971). https://doi.org/10.1016/S0022-
0000(71)80013-2, https://doi.org/10.1016/S0022-0000(71)80013-2
6. of Computer Science, Y.U.D., Lipton, R.: The reachability problem requires
exponential space. Research report (Yale University. Department of Com-
puter Science), Department of Computer Science, Yale University (1976),
https://books.google.de/books?id=7iSbGwAACAAJ
7. Cortadella, J., Kishinevsky, M., Kondratyev, A., Lavagno, L., Yakovlev, A.: Hard-
ware and petri nets: Application to asynchronous circuit design. In: Nielsen,
M., Simpson, D. (eds.) Application and Theory of Petri Nets 2000, 21st In-
ternational Conference, ICATPN 2000, Aarhus, Denmark, June 26-30, 2000,
Proceeding. Lecture Notes in Computer Science, vol. 1825, pp. 1–15. Springer
(2000). https://doi.org/10.1007/3-540-44988-4 1, https://doi.org/10.1007/3-540-
44988-4 1
8. Czerwinski, W., Lasota, S., Lazic, R., Leroux, J., Mazowiecki, F.: The reach-
ability problem for petri nets is not elementary. In: Charikar, M., Co-
hen, E. (eds.) Proceedings of the 51st Annual ACM SIGACT Sympo-
sium on Theory of Computing, STOC 2019, Phoenix, AZ, USA, June 23-
26, 2019. pp. 24–33. ACM (2019). https://doi.org/10.1145/3313276.3316369,
https://doi.org/10.1145/3313276.3316369
9. Delosme, J., Hujsa, T., Kordon, A.M.: Polynomial sufficient conditions of
well-behavedness for weighted join-free and choice-free systems. In: Car-
mona, J., Lazarescu, M.T., Pietkiewicz-Koutny, M. (eds.) 13th International
Conference on Application of Concurrency to System Design, ACSD 2013,
Barcelona, Spain, 8-10 July, 2013. pp. 90–99. IEEE Computer Society (2013).
https://doi.org/10.1109/ACSD.2013.12, https://doi.org/10.1109/ACSD.2013.12
132 Ronny Tredup and Sophie Wallner
10. Desel, J., Esparza, J.: Reachability in reversible free choice systems. In: Chof-
frut, C., Jantzen, M. (eds.) STACS 91, 8th Annual Symposium on Theoretical
Aspects of Computer Science, Hamburg, Germany, February 14-16, 1991, Proceed-
ings. Lecture Notes in Computer Science, vol. 480, pp. 384–397. Springer (1991).
https://doi.org/10.1007/BFb0020814, https://doi.org/10.1007/BFb0020814
11. Desel, J., Esparza, J.: Reachability in cyclic extended free-choice systems. Theor.
Comput. Sci. 114(1), 93–118 (1993)
12. Esparza, J.: Reachability in live and safe free-choice petri nets is np-complete.
Theor. Comput. Sci. 198(1-2), 211–224 (1998). https://doi.org/10.1016/S0304-
3975(97)00235-1, https://doi.org/10.1016/S0304-3975(97)00235-1
13. Gallo, O., Necas, T., Lehocki, F.: A tool for the synthesis of asynchronous speed-
independent circuits. In: Donatelli, S., Kleijn, J., Machado, R.J., Fernandes, J.M.
(eds.) Proceedings of the Workshops of the 31st International Conference on Appli-
cation and Theory of Petri Nets and Other Models of Concurrency (PETRI NETS
2010) and of the 10th International Conference on Application of Concurrency
to System Design (ACSD 2010), Braga, Portugal, June, 2010. CEUR Workshop
Proceedings, vol. 827, pp. 207–211. CEUR-WS.org (2010), http://ceur-ws.org/Vol-
827/16 OndrejGallo article.pdf
14. Genrich, H.J., Lautenbach, K.: Synchronisationsgraphen. Acta Informatica 2, 143–
161 (1973)
15. Holt, A.W.: Coordination technology and petri nets. In: Applications and Theory
in Petri Nets. Lecture Notes in Computer Science, vol. 222, pp. 278–296. Springer
(1985)
16. Howell, R.R., Rosier, L.E.: Completeness results for conflict-free vec-
tor replacement systems. J. Comput. Syst. Sci. 37(3), 349–366 (1988).
https://doi.org/10.1016/0022-0000(88)90013-X, https://doi.org/10.1016/0022-
0000(88)90013-X
17. Hujsa, T., Delosme, J., Kordon, A.M.: On the reversibility of live equal-conflict
petri nets. In: Devillers, R.R., Valmari, A. (eds.) Application and Theory of Petri
Nets and Concurrency - 36th International Conference, PETRI NETS 2015, Brus-
sels, Belgium, June 21-26, 2015, Proceedings. Lecture Notes in Computer Science,
vol. 9115, pp. 234–253. Springer (2015). https://doi.org/10.1007/978-3-319-19488-
2 12, https://doi.org/10.1007/978-3-319-19488-2 12
18. Kosaraju, S.R.: Decidability of reachability in vector addition systems (prelimi-
nary version). In: Lewis, H.R., Simons, B.B., Burkhard, W.A., Landweber, L.H.
(eds.) Proceedings of the 14th Annual ACM Symposium on Theory of Comput-
ing, May 5-7, 1982, San Francisco, California, USA. pp. 267–281. ACM (1982).
https://doi.org/10.1145/800070.802201, https://doi.org/10.1145/800070.802201
19. Krämer, B.J.: Stepwise construction of non-sequential software systems using a
net-based specification language. In: Rozenberg, G., Genrich, H.J., Roucairol, G.
(eds.) Advances in Petri Nets 1984, European Workshop on Applications and The-
ory in Petri Nets, covers the last two years which include the workshop 1983 in
Toulouse and the workshop 1984 in Aarhus, selected papers. Lecture Notes in Com-
puter Science, vol. 188, pp. 307–330. Springer (1984). https://doi.org/10.1007/3-
540-15204-0 18, https://doi.org/10.1007/3-540-15204-0 18
20. Lambert, J.: A structure to decide reachability in petri nets. Theor. Com-
put. Sci. 99(1), 79–104 (1992). https://doi.org/10.1016/0304-3975(92)90173-D,
https://doi.org/10.1016/0304-3975(92)90173-D
21. Mayr, E.W.: An algorithm for the general petri net reachability problem. In:
Proceedings of the 13th Annual ACM Symposium on Theory of Comput-
The Reachability Problem for Acyclic Join-Free Petri nets is NP-complete 133
ing, May 11-13, 1981, Milwaukee, Wisconsin, USA. pp. 238–246. ACM (1981).
https://doi.org/10.1145/800076.802477, https://doi.org/10.1145/800076.802477
22. Moore, C., Robson, J.M.: Hard tiling problems with simple tiles. Discrete & Com-
putational Geometry 26(4), 573–590 (2001). https://doi.org/10.1007/s00454-001-
0047-6
23. Murata, T.: Petri nets: Properties, analysis and applications. Proceedings of the
IEEE 77(4), 541–580 (1989)
24. Petri, C.A.: Concepts of net theory. In: MFCS. pp. 137–146. Mathematical Institute
of the Slovak Academy of Sciences (1973)
25. Richta, T., Janousek, V., Kocı́, R.: Dynamic software architecture for distributed
embedded control systems. In: Moldt, D., Rölke, H., Störrle, H. (eds.) Proceedings
of the International Workshop on Petri Nets and Software Engineering (PNSE’15),
including the International Workshop on Petri Nets for Adaptive Discrete Event
Control Systems (ADECS 2015) A satellite event of the conferences: 36th Inter-
national Conference on Application and Theory of Petri Nets and Concurrency
Petri Nets 2015 and 15th International Conference on Application of Concur-
rency to System Design ACSD 2015, Brussels, Belgium, June 22-23, 2015. CEUR
Workshop Proceedings, vol. 1372, pp. 133–150. CEUR-WS.org (2015), http://ceur-
ws.org/Vol-1372/paper8.pdf
26. Rodrı́guez, A., Kristensen, L.M., Rutle, A.: On modelling and validation of the
MQTT iot protocol for M2M communication. In: Moldt, D., Kindler, E., Rölke, H.
(eds.) Proceedings of the International Workshop on Petri Nets and Software Engi-
neering (PNSE’18), co-located with the39th International Conference on Applica-
tion and Theory of Petri Nets and Concurrency Petri Nets 2018 and the 18th Inter-
national Conference on Application of Concurrency to System Design ACSD 2018,
Bratislava, Slovakia, June 24-29, 2018. CEUR Workshop Proceedings, vol. 2138,
pp. 99–118. CEUR-WS.org (2018), http://ceur-ws.org/Vol-2138/paper5.pdf
27. Sifakis, J.: Use of petri nets for performance evaluation. In: Beilner, H., Gelenbe,
E. (eds.) Measuring, Modelling and Evaluating Computer Systems, Proceedings of
the Third International Symposium, Bonn - Bad Godesberg, Germany, October
3-5, 1977. pp. 75–93. North-Holland (1977)
28. Stewart, I.A.: Reachability in some classes of acyclic petri nets. Fun-
dam. Informaticae 23(1), 91–100 (1995). https://doi.org/10.3233/FI-1995-2314,
https://doi.org/10.3233/FI-1995-2314
29. Teruel, E., Colom, J.M., Suárez, M.S.: Choice-free petri nets: a model for deter-
ministic concurrent systems with bulk services and arrivals. IEEE Trans. Syst.
Man Cybern. Part A 27(1), 73–83 (1997). https://doi.org/10.1109/3468.553226,
https://doi.org/10.1109/3468.553226
30. Yamaguchi, S.: Polynomial time verification of reachability in sound extended free-
choice workflow nets. IEICE Trans. Fundam. Electron. Commun. Comput. Sci.
97-A(2), 468–475 (2014)
134 Ronny Tredup and Sophie Wallner