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