On the Complexity of Safe, Elementary Hornets Michael Köhler-Bußmeier University of Hamburg, Department of Informatics Vogt-Kölln-Str. 30, D-22527 Hamburg koehler@informatik.uni-hamburg.de Abstract. In this paper we study the complexity of Hornets, an alge- braic extension of object nets. We define a restricted class: safe, elemen- tary Hornets, to guarantee finite state spaces. It will turn out, that the reachability problem for this class requires exponential space, which is a major increase when compared to safe, elementary object nets, which require polynomial space. Keywords: Hornets, nets-within-nets, object nets, reachability, safeness 1 Hornets: Higher-Order Object Nets In this paper we study the algebraic extension of object nets, called Hornets. Hornets are a generalisation of object nets [KR03,KR04,KBH09], which follow the nets-within-nets paradigm as proposed by Valk [Val91,Val03]. With object nets we study Petri nets where the tokens are nets again, i.e. we have a nested marking. Events are also nested. We have three different kinds of events – as illustrated by the following example: 1. System-autonomous: The system net transition b t fires autonomously, which moves the net-token from pb1 to pb2 without changing its marking. 2. Object-autonomous: The object net fires transition t1 “moving” the black token from q1 to q2 . The object net remains at its location pb1 . 3. Synchronisation: Whenever we add matching synchronisation inscriptions at the system net transition b t and the object net transition t1 , then both must fire synchronously: The object net is moved to pb2 and the black token moves from q1 to q2 inside. Whenever synchronisation is specified, autonomous actions are forbidden. For Hornets we extend object-nets with algebraic concepts that allow to modify the structure of the net-tokens as a result of a firing transition. This is a generalisation of the approach of algebraic nets [Rei91], where algebraic data types replace the anonymous black tokens. Example 1. We consider a Hornet with two workflow nets N1 and N2 as tokens – cf. Figure 1. To model a run-time adaption, we combine N1 and N2 resulting in the net N3 = (N1 kN2 ). This modification is modelled by transition t of the Hornets in Fig. 1. In a binding α with x 7→ N1 and y 7→ N2 the transition t is enabled. Assume that (xky) evaluates to N3 for α. If t fires it removes the two net-tokens from p and q and generates one new net-token on place r. The net-token on r has the structure of N3 and its marking is obtained as a transfer from the token on v in N1 and the token on s in N2 into N3 . This transfer is possible since all the places of N1 and N2 are also places in N3 and tokens can be transferred in the obvious way. N2 i s f net-token produced on r by t i2- d - ri - e - i2 i- u v f1 a- h - b- h r- c- h 1 N3 h } ZZ q Zl s y i- 3  @R - h f3 Hj H (xky) r h - l @ Rh f p*  t i2 - d - h rs - e - h 2 s x l   = N1 i u v f i1- a - i - b - ri - c - i1 Fig. 1. Modification of the net-token’s structure The use of algebraic operations in Hornets relates them to algebraic higher- order (AHO) systems [HEM05], which are restricted to two-levelled systems but have a greater flexibility for the operations on net-tokens, since each net transformation is allowed. There is also a relationship to Nested Nets [Lom08], which are used for adaptive systems. It is not hard to prove that the general Hornet formalism is Turing-complete. In [KB09] we have proven that there are several possibilities to simulate counter programs: One could use the nesting to encode counters. Another possibility is to encode counters in the algebraic structure of the net operators. In this paper we like to study the complexity that arises due the algebraic structure. Therefore, we restrict Hornets to guarantee that the system has a finite state space. First, we allow at most one token on each place, which results in the class of safe Hornets. However this restriction does not guarantee finite state spaces, since we have the nesting depth as a second source of undecidability [KBH09]. Second, we restrict the universe of object nets to finite sets. Finally, we restrict the nesting depth and introduce the class of elementary Hornets, which have a two-levelled nesting structure. This is done in analogy to the class of elemtary object net systems ( Eos) [KR04], which are the two-level specialisation of general object nets [KR04,KBH09]. If we rule out these sources of complexity the main origin of complexity is the use of algebraic transformations, which are still allowed for safe, elementary Hornets. As a result we obtain the class of safe, elementary Hornets – in analogy to the class of safe Eos [KBH10]. We have shown in [KBH10,KBH11] that most problems for safe Eos are PSpace-complete. More precisely: All problems that are expressible in LTL or CTL, which includes reachability and liveness, are PSpace-complete. This means that with respect to these problems safe Eos are no more complex than p/t nets. In this presentation we will show that safe, elementary Hornets are beyond PSpace. It is well known that “the reachability problem requires exponential space” in the case of bounded p/t nets [Lip76]. We obtain that the reachability problem for safe, elementary Hornets requires exponential space, too. We step from polynomial space (as in the case of safe Eos) to exponential space in the case of safe elementary Hornets. 2 Elementary Hornets A multiset m on the set D is a mapping m P : D → N. Multisets can also be n represented as a formal sum in the form m = i=1 xi , where xi ∈ D. Multiset addition is defined component-wise: (m1 +m2 )(d) := m1 (d)+m2 (d). The empty multiset 0 is defined as 0(d) = 0 for all d ∈ D. Multiset-difference m1 − m2 is defined by (m1 − m2 )(d) := max(mP 1 (d) − m2 (d), 0). The cardinality of a multiset is |m| := d∈D m(d). A multiset m is finite if |m| < ∞. The set of all finite multisets over the set D is denoted MS (D). Multiset notations are used for sets as well. The meaning will be apparent from its use. ′ Any mapping Pfn : D → DPextends to a multiset-homomorphism f ♯ : MS (D) → ′ ♯ n MS (D ) by f ( i=1 xi ) = i=1 f (xi ). Net-Algebras We define the algebraic structure of object nets. For a general introduction of algebraic specifications cf. [EM85]. Let K be a set of net-types (kinds). A (many-sorted) specification (Σ, X, E) consists of a signature Σ, a family of variables X = (Xk )k∈K , and a family of axioms E = (Ek )k∈K . A signature is a disjoint family Σ = (Σk1 ···kn ,k )k1 ,··· ,kn ,k∈K of operators. The set of terms of type k over a signature Σ and variables X is denoted TkΣ (X). We use (many-sorted) predicate logic, where the terms are generated by a signature Σ and formulae are defined by a family of predicates Ψ = (Ψn )n∈N . The set of formulae is denoted PLΓ , where Γ = (Σ, X, E, Ψ ) is the logic structure. Let Σ be a signature over K. A net-algebra assigns to each type k ∈ K a set Nk of object nets. Each object N ∈ N Sk , k ∈ K net is a p/t net N = (PN , TN , preN , postN ). We identify N with k∈K Nk in the following. We as- sume the family N = (Nk )k∈K to be disjoint. The nodes of the object nets in Nk are not disjoint, since the firing rule allows to transfer tokens between net tokens within the same set Nk . Such a transfer is possible, if we assume that all nets N ∈ Nk have the same set of places Pk . In the example of Fig. 1 the object nets N1 , N2 , and N3 must belong to the same type since otherwise it would be impossible to transfer the markings in N1 and N2 to the generated N3 . In general, Pk is not finite. Since we like each object net to be finite in some sense, we require that the transitions TN of each N ∈ Nk use only a finite subset of Pk , i.e. ∀N ∈ N : |• TN ∪ TN • | < ∞. The family of object nets N is the universe of the algebra. A net-algebra (N , I) assigns to each constant σ ∈ Σλ,k an object net σ I ∈ Nk and to each operator σ ∈ Σk1 ···kn ,k with n > 0 a mapping σ I : (Nk1 × · · · × Nkn ) → Nk . A net-algebra is called finite if Pk is a finite set for each k ∈ K. A variable assignment α = (αk : Xk → Nk )k∈K maps each variable onto an element of the algebra. For a variable assignment α the evaluation of a term t ∈ TkΣ (X) is uniquely defined and will be denoted as α(t). A net-algebra, such that all axioms of (Σ, X, E) are valid, is called net-theory. System Net Assume we have a fixed logic Γ = (Σ, X, E, Ψ ) and a net-theory (N , I). An elementary higher-order object net (Hornet) is composed of a sys- tem net N b and the set of object nets N . W.l.o.g. we assume N b 6∈ N . To guaran- tee finite state spaces for elementary Hornets, we require that the net-theory (N , I) is finite, i.e. each place universe Pk is finite. The system net is a net N b = (Pb, Tb, pre, post, G), b where each arc is labelled with a multiset of terms: pre, post : Tb → (Pb → MS (TΣ (X))). Each transition is labelled by a guard predicate G b : Tb → PLΓ . The places of the system net are b typed by the function d : P → K. As a typing constraint we have that each arc inscription has to be a multiset of term of kind assigned to the arc’s place: p) d(b pre(b t)(b p), post(b p) ∈ MS (TΣ (X)) t)(b (1) For each variable binding α we obtain the evaluated functions preα , postα : Tb → (Pb → MS (N )) in the obvious way. Nested Markings Since the tokens of an elementary Hornets are instances of object nets a marking is a nested multiset of the form: n X µ= pbi [Ni , Mi ] where pbi ∈ Pb, Ni ∈ Nd(pbi ) , Mi ∈ MS (PNi ), n ∈ N i=1 Each addend pbi [Ni , Mi ] denotes a net-token on the place pbi that has the structure of the object net Ni and the marking Mi ∈ MS (PNi ).1 The set of all nested multisets is denoted as M. We define the partial order ⊑ on nested multisets by setting µ1 ⊑ µ2 iff ∃µ : µ2 = µ1 + µ. 1 For Eos the net structure of a net-token is uniquely determined by the place. So, we do not include the object net Ni in µ for Eos. The projection Π 1 abstracts from the substructure of all net-tokens: X n  Xn 1 ΠN pbi [Ni , Mi ] := 1N (Ni ) · pbi (2) i=1 i=1 where the indicator function 1N is defined as: 1N (Ni ) = 1 iff Ni = N . 2 The projection ΠN (µ) is the multiset of all object nets in the marking: X n  Xn 2 ΠN pbi [Ni , Mi ] := Ni (3) i=1 i=1 The projection Πk2 is the sum of all net-tokens’ markings (of the same type k ∈ K) ignoring their local distribution within the system net: X n  Xn Πk2 pbi [Ni , Mi ] := pi ) · M i 1k (b (4) i=1 i=1 where the indicator function 1k is defined as: 1k (b pi ) = 1 iff d(b p) = k. Synchronisation The transitions in an Hornet are labelled with synchronisation inscriptions. We assume a fixed set of channels C = (Ck )k∈K . – The function family b lα = (b lαk )k∈K defines the synchronisation constraints. Each transition of the system net is labelled with a multiset b lk (b t) = (e1 , c1 )+ k · · · + (en , cn ), where the expression ei ∈ TΣ (X) describes the called object net and ci ∈ Ck is a channel. Each variable assignment α generates the function b lαk (b t)(N ): X X b lαk (b t)(N ) := ci for b lk (b t) = (ei , ci ) (5) 1≤i≤n α(ei )=N 1≤i≤n Each function blαk (b t)(N ) assigns for each object net N a multiset of channels. The intention is that b t fires synchronously with a multiset ϑ(N ) of object net transitions with matching multiset of labels. – For each N ∈ Nk the function lN assigns to each transition t ∈ TN ei- ther a channel c ∈ Ck or ⊥k , whenever t fires without synchronisation, i.e. autonously. Definition 1 (Elementary Hornet). Assume a fixed many-sorted predicate b , N , I, d, l, µ0 ) logic Γ = (Σ, X, E, Ψ ). An elementary Hornet is a tuple EH = (N such that: 1. Nb is an algebraic net, called the system net. 2. (N , I) is a finite net-theory for the logic Γ . 3. d : Pb → K is the typing of the system net places. 4. l = (bl, lN )N ∈N is the labelling. 5. µ0 ∈ M is the initial marking. Events The synchronisation labelling generates the set of system events Θ: The labelling introduces three cases of events: 1. Synchronised firing: There is at least one object net that has to be synchro- nised, i.e. there is a N such that b l(bt)(N ) is not empty. Such an event is a pair θ = t [ϑ], where b bα t is a system net transition, α is a variable binding, and ϑ is a function that maps each object net to a multiset of its transitions, i.e. ϑ ∈ MS (TN ). It is required that τb and ϑ(N ) have matching multisets of labels, i.e. bl(b t)(N ) = lN ♯ (ϑ(N )) for all N ∈ N . The intended meaning is that τb fires synchronously with all the object net transitions ϑ(N ), N ∈ N . 2. System-autonomous firing: The transition b t of the system net fires autonomously, whenever b l(b t) is the empty multiset 0. We consider system-autonomous firing as a special case of synchronised firing generated by the function ϑid , defined as ϑid (N ) = 0 for all N ∈ N . 3. Object-autonomous firing: An object net transition t in N fires autonomously, whenever lN (t) = ⊥k . Object-autonomous events are denoted as id pb,N [ϑt ], where ϑt (N ′ ) = {t} if N = N ′ and 0 otherwise. The meaning is that in object net N fires t autonomously within the place pb. For the sake of uniformity we define for an arbitrary binding α: ( ′ ′ ′ ′ 1 if pb′ = pb ∧ N ′ = N preα (id pb,N )(b p )(N ) = postα (id pb,N )(b p )(N ) = 0 otherwise. The set of all events generated by the labelling l is Θl := Θ1 ∪ Θ1 : n o Θ1 := τbα [ϑ] | ∀N ∈ N : b lα (b t)(N ) = lN♯ (ϑ(N )) n o (6) Θ2 := id pb,N [ϑt ] | pb ∈ Pb, N ∈ Nd(bp) , t ∈ TN Firing Rule A system event θ = τbα [ϑ] removes net-tokens together with their individual internal markings. Firing the event replaces a nested multiset λ ∈ M that is part of the current marking µ, i.e. λ ⊑ µ, by the nested multiset ρ. The enabling condition is expressed by the enabling predicate φEH (or just φ whenever EH is clear from the context): τ α [ϑ], λ, ρ) ⇐⇒ ∀k ∈ K : φ(b p ∈ d−1 (k) : ∀N ∈ Nk : ΠN ∀b 1 (λ)(b p) = preα (b p)(N ) ∧ τ )(b −1 1 ∀b p ∈ d (k) : ∀N ∈ Nk : ΠN (ρ)(b p) = postα (b p)(N ) ∧ τ )(b (7) P Πk2 (λ) ≥ N ∈Nk pre♯N (ϑ(N )) ∧ P Πk2 (ρ) = Πk2 (λ) + N ∈Nk post♯N (ϑ(N )) − pre♯N (ϑ(N )) The predicate φ has the following meaning: Conjunct (1) states that the removed sub-marking λ contains on pb the right number of net-tokens, that are removed by τb. Conjunct (2) states that generated sub-marking ρ contains on pb the right number of net-tokens, that are generated by τb. Conjunct (3) states that the sub-marking λ enables all synchronised transitions ϑ(N ) in the object N . Conjunct (4) states that the marking of each object net N is changed according to the firing of the synchronised transitions ϑ(N ). Note, that conjunct (1) and (2) assures that only net-tokens relevant for the firing are included in λ and ρ. Conditions (3) and (4) allow for additonal tokens in the net-tokens. For system-autonomous events b tα [ϑid ] the enabling predicate φ can be sim- plified further: Conjunct (3) is always true since preN (ϑid (N )) = 0. Conjunct (4) simplifies to Πk2 (ρ) = Πk2 (λ), which means that no token of the object nets get lost when a system-autonomous events fires. Analogously, for an object-autonomous event τb[ϑt ] we have an idle-transition 1 τb = id pb,N and ϑ = ϑt for some t. Conjunct (1) and (2) simplify to ΠN ′ (λ) = 1 ′ 1 1 pb = ΠN ′ (ρ) for N = N and to ΠN ′ (λ) = 0 = ΠN ′ (ρ) otherwise. This means that λ = pb[M ], M enables t, and ρ = pb[M − preN (b t) + postN (b t)]. Definition 2 (Firing Rule). Let EH be an elementary Hornet and µ, µ′ ∈ M markings. – The event τbα [ϑ] is enabled in µ for the mode (λ, ρ) ∈ M2 iff λ ⊑ µ ∧ b τ [ϑ], λ, ρ) holds and the guard G(t) φ(b holds, i.e. E |=α b τ ). I G(b τbα [ϑ](λ,ρ) – An event τbα [ϑ] that is enabled in µ can fire: µ −−−−−−→ µ′ . EH – The resulting successor marking is defined as µ′ = µ − λ + ρ. Note, that the firing rule has no a-priori decision how to distribute the mark- ing on the generated net-tokens. Therefore we need the mode (λ, ρ) to formulate the firing of τbα [ϑ] in a functional way. 3 Boundedness for Safe Elementary Hornets A Hornet is safe iff each place pb in the system net carries at most one token and each net-token carries at most one token on each place p in all reachable markings µ. Since we are interested in safe Hornets in the following, we do not use arc weights greater than 1. Since all nets N ∈ Nk have the same set of places Pk , there is an upper bound for the cardinality of Nk . 4|Pk | Lemma 1. For each k ∈ K we have |Nk | ≤ 2(2 ). Proof. Note, that each common set of places Pk is finite for elementary Hor- nets. Each possible transition t chooses a subset of Pk for the preset • t and another subset for the postset t• . We identify t with the pair (• t, t• ). A tran- sition is an element from Tk := P(Pk ) × P(Pk ). We have |Tk | = 2|Pk | · 2|Pk | = (2|Pk | )2 = 22|Pk | different transitions. To each transition t ∈ TN , N ∈ Nk the partial function lN assigns either a channel c ∈ Ck or ⊥k . The set of labelled transitions is LTk := Tk × (Ck ∪ {⊥k })) and we have |LTk | = |Tk × (Ck ∪ {⊥k }))| = 22|Pk | · (|Ck | + 1) different labelled transitions. We cannot use more channels than we have transitions in the object net, i.e. we could use at most |Tk | ≤ 22|Pk | different channels from Ck ∪ {⊥k }. Thus, we have: |LTk | = 22|Pk | · (|Ck | + 1) ≤ 22|Pk | · 22|Pk | ≤ 24|Pk | Since each object net N in Nk is characterised by its set of labelled transitions 4|Pk | and there are |P(LTk )| = 2|LTk | subsets of LTk , we have at most 2(2 ) different object nets. qed. In the following we identify an object net with a subset of LTk . Lemma 2. A safe Hornet has a finite reachability set. Pn Proof. Each reachable marking is of the form µ = i=1 pbi [Ni , Mi ]. Since each each object net N ∈ Nk is safe, we know that each net-token has at most 2|Pk | 4|Pk | different markings Mi Furthermore, we know |Nk | ≤ 2(2 ) . Assume that m is 4m the maximum of all |Pk |. Then we have at most 2(2 ) · 2m different net-tokens [N, M ]. Each system net place pb is either unmarked or marked with one of these  4m |Pb| net-tokens. Therefore, we have at most 1 + 2(2 ) · 2m different markings in the safe Hornet. qed. It can be shown that for each elementary Hornet EH there exists an Eos ∗ ∗ OS (EH ) with the simulation property: µ −−→ µ′ ⇐⇒ µ −−−−−→ µ′ . The EH OS (EH ) construction of OS (EH ) results in a quite drastic increase in the size of Eos, since we add new elements for each object net in the Hornet. By Lemma 1 the size of the Eos grows double exponentially in Pk . Therefore, the simulation by OS (EH ) is only good for showing undecidability by giving a reduction from Hornets to Eos (Since we know that the reachability problem for Eos is un- decidable [Köh07], we obtain another undecidability proof for Hornets.), but not for studying complexity bounds. In the following we study the complexity of the reachability problem for safe elementary Hornets. 4 Encoding of Elementary Hornets To encode a p/t net, we encode the pre-and the post-matrix, which can be stored in O(|P | · |T |) bits. The size of an elementary Hornet is more involved, since we have to store the algebra and the net-tokens: Lemma 3. Let EH = (N b , N , I, d, l, µ0 ) an elementary Hornet with µ0 = Pn bi [Ni , Mi ]. Assume that the net algebra can be encoded in s(I) space. Then, i=1 p EH can be encoded in s(EH) := s(N b ) + s(I) + s(µ0 ) space, where:     s(N b ) ∈ O |Pb| · |Tb| and s(µ0 ) ∈ O |Pb| · (mN (µ0 ) · mP + m2P ) 2 with mP := max{|Pk | : k ∈ K} and mN (µ0 ) := max{s(N ) | N ∈ ΠN (µ0 )}. Proof. Note, that it is sufficient to encode the system net N b , the net operators in I, the typing d, the global object net place sets Pk , and the initial marking µ0 . It is not necessary to encode the object nets in N , since the object nets are part of the current marking µ and combinatorially derived from Pk . – The system net can be stored in O(|Pb| · |Tb|) bits: The arc-inscriptions pre(bt), post(b t) and transition-inscriptions G( b b t) are fi- nite and need O(|Pb| · |Tb|) bits. The system net labelling b l (b k t) are finite expressions, too, and need O(|Tb|) bits. – The typing d is stored in O(|Pb|) bits. Pn We encode the initial marking µ0 = i=1 pbi [Ni , Mi ] as a list: – Each pb is marked with at most one net-token: n ≤ |Pb |. – Each object net transition is an element from Tk := P(Pk ) × P(Pk ), which needs O(|Pk |) bits. The label lN (t) of an object net transition t is stored in O(|Pk |) bits, since |Ck ∪ {⊥k }| ≤ |TN |. Therefore, a labelled object net transition t uses s(t) ∈ O(|Pk |) bits. – Each object net is identified with some subset LTN = {(t1 , c1 ), . . . , (tn , cn )} of LTk . We encode each object N as the list code(N ) := (t1 , c1 ) · · · (tn , cn ). All in all, we need s(Ni ) := |LTNi | · O(|Pk |) bits to store code(N ). Since each place Pk in the object net is marked with at most one token, we can store Mi as a list of those places that are marked in Mi . We need at most s(Mi ) := |Pd(bpi ) | log(|Pd(bpi ) |) ≤ |Pd(bpi ) |2 bits for this list. 2 Therefore, each net-token [Ni , Mi ] needs O(|LTP Ni | · |Pk | + |Pk | ) bits. n – The space needed for the initial marking µ0 = i=1 pbi [Ni , Mi ] is: Pn Pn s(µ0 ) = i=1 s(Ni ) + s(Mi ) ∈ O( i=1 |LTNi | · |Pd(bpi ) | + |Pk |2 ) Pn ⊆ O( i=1 mN (µ0 ) · mP + m2P ) ⊆ O(|Pb| · (mN (µ0 ) · mP + m2P )) Then, s(EH) is the sum of all components. qed. Since s(Ni ) ≤ 24mP we have mN (µ0 ) ≤ 24mP , which “simplifies” the estima- tion for |µ0 |:     s(µ0 ) ∈ O |Pb| · (mN (µ0 ) · mP + m2P ) ⊆ O |Pb | · (22(mP +1) · mP + m2P ) But, in general 24mP is a rather rude estimation, e.g. in those cases, when only a small subset of N is reachable. 5 Complexity of the Reachability Problem The size |A| of a Turing machines A is the size needed to store its Turing table. Following the presentation in [Esp98] we consider Turing machines A that start with an empty tape as input. We say that A is exponentially bounded (w.r.t. the size of A) if A uses at most 2|A| cells of the tape during all possible runs starting with the empty tape. It is well known that each TM A can be simulated by a counter program C(A). Moreover, if A is exponentially bounded (w.r.t. the size of A), then each |A| counter of C(A) is bounded by 22 . Theorem 1. The reachability problem for safe elementary Hornets requires exponential space. Proof. Our proof that the reachability problem for safe elementary Hornets re- quires at least exponential space is similar to the heart of Lipton’s famous result. Lipton has proven that acceptance of a counter program C translates into a reachability question for a p/t net N (C). Lipton gives a construction for N (C), which √is of size O(|C|2 ). This proves that the reachability problem requires at least 2 |C| space, i.e. exponential space. Our goal is to simulate a counter program C by a safe, elementary Hornet EH of size O(poly(|C|)). In this case we know that a question about a counter program C translates into a question √ about EH. When C needs 2|A| space for the n counters, we have that EH needs 2 |A| space for the corresponding question, where n is the order of the polynom poly(|C|). The translation of counter program statements into Hornets is quite straight- forward. For each program line l and each counter c we have a place. Places for lines are marked with black tokens, places for counters are marked with the net-type Int. For the type Int we have the constant zero and the unary operator suc. The net zero is interpreted as the object net with no transitions and suc enumerates the next subset of LTInt . The translation of each command into a transition is given as in the figure below. The initial marking puts a black token at l1 for first command and one net-token [zero, 0] on each counter place. Since we cannot use more counters than we have statements in C we have O(|Pb|·|Tb|) ⊆ O(|Tb|2 ) = O(|C|2 ), i.e. the resulting system net N b grows quadratic in the size of the program C. Each net-token [zero, 0] in µ0 needs only O(|PInt |) bits, since zero is encoded by the empty list. The marking 0 is encoded by constantly many bits. Therefore, the initial marking needs only O(|Pb|) ⊆ O(|C|) bits. It remains to estimate the size of a Turing machine that the nets zero and suc(N ) (cf. Fig. 2). It is easy to construct the object net zero: simply return the empty list. For the construction of suc(N ), where N is given as a list X, we do function suc(X: list of bit-vector): list of bit-vector function d-exp(n : int) : int var a, b, c : bit; var x, y, i : int; var i : bit-vector: begin var Y : list of bit-vector: n := 2n + 1; begin x := 1; Y := empty-list; c := 1; for i := 1 to n do x := 2x end 4|PInt | n := d-exp(|PInt |) // n = 22 // x = 22n+1 for i := 0 to n − 1 do y = 1; a := is-in(i, X); for i := 1 to x do y := 2y end 2n+1 (b, c) := (c ∧ a, c XOR a); // y = 22 if b = 1 then Y := append(i, Y ) return y end; end return Y ; end Fig. 2. Listing: Net Operators Fig. 3. Listing: Bound a binary increment: We convert the list X of labelled transitions into a binary 4|P | string a0 · · · an−1 of length n := 22 Int = |NInt |. The digits ai are computed whenever necessary. We iterate through all indices i from 0 to n and compute from a and the current carry c the output digit bi and the next carry bit. We add the labelled transition with index i to the list Y . Finally, Y is the list that encodes the resulting object net suc(N ). 4|P | Note, that we cannot denote n = 22 Int directly as the limite of the for-loop, 4|PInt | since we need at least 2 bits to store the for-command, which is undesired to obtain a small Hornet. Instead, we compute n by the function d-exp(|PInt |), which needs only log(|PInt |) bits to store. With this trick the size of the programs are within O(log(|PInt |)). |A| Each counter of C(A) is bounded by 22 . If we set |PInt | := |A|, then we can 4|A| |A| generate n = 22 ≥ 22 object nets – enough to simulate the counter. With |PInt | := |A| we obtain O(log(|PInt |)) ⊆ O(|PInt |) = O(|A|) = O(|C|). The size of the Hornet is therefore in O(|Pb|·|Tb|)+O(|Pb |)+O(log(|PInt |)) ⊆ O(|C|2 )+O(|C|)+O(log(|C|)) ⊆ O(|C|2 ). √ This shows that EH needs 2 |A| space for the reachability problem. qed. 6 Conclusion In this paper we studied the subclass of safe, elementary Hornets. While all properties expressible in temporal logic are PSpace-complete for safe Eos, we obtain that the reachability problem for safe, elementary Hornets needs at least exponential space, which is also a lower bound for LTL model checking since the reachability problem can be expressed as a LTL property. We like to emphasise that the power of safe, elementary Hornets is only due to the transformations of the net-algebra, since all other sources of complexity (nesting, multiple tokens on a place, etc.) have been ruled out by the restriction of safeness and elementariness. References [EM85] Hartmut Ehrig and Bernd Mahr. Fundamentals of algebraic Specification. EATCS Monographs on TCS. 1985. [Esp98] Javier Esparza. Decidability and complexity of petri net problems – an in- troduction. In Wolfgang Reisig and Grzegorz Rozenberg, editors, Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, volume 1491 of LNCS, pages 374–428. 1998. [HEM05] Kathrin Hoffmann, Hartmut Ehrig, and Till Mossakowski. High-level nets with nets and rules as tokens. In PETRI NETS 2005, volume 3536 of LNCS, pages 268 – 288. 2005. [KB09] Michael Köhler-Bußmeier. Hornets: Nets within nets combined with net al- gebra. In Karsten Wolf and Giuliana Franceschinis, editors, PETRI NETS 2009, volume 5606 of LNCS, pages 243–262. 2009. [KBH09] Michael Köhler-Bußmeier and Frank Heitmann. On the expressiveness of communication channels for object nets. Fundamenta Informaticae, 93(1- 3):205–219, 2009. [KBH10] Michael Köhler-Bußmeier and Frank Heitmann. Safeness for object nets. Fundamenta Informaticae, 101(1-2):29–43, 2010. [KBH11] Michael Köhler-Bußmeier and Frank Heitmann. Liveness of safe object nets. Fundamenta Informaticae, 112(1):73–87, 2011. [Köh07] Michael Köhler. Reachable markings of object Petri nets. Fundamenta In- formaticae, 79(3-4):401 – 413, 2007. [KR03] Michael Köhler and Heiko Rölke. Concurrency for mobile object-net systems. Fundamenta Informaticae, 54(2-3), 2003. [KR04] Michael Köhler and Heiko Rölke. Properties of Object Petri Nets. In J. Cor- tadella and W. Reisig, editors, PETRI NETS 2004, volume 3099 of LNCS, pages 278–297. 2004. [Lip76] Richard J. Lipton. The reachability problem requires exponential space. Re- search Report 62, Dept. of Computer science, 1976. [Lom08] Irina Lomazova. Nested petri nets for adaptive process modeling. In A. Avron, N. Dershowitz, and A. Rabinovich, editors, Pillars of Computer Sci- ence, volume 4800 of LNCS, pages 460–474. Springer, 2008. [Rei91] Wolfgang Reisig. Petri nets and algebraic specifications. Theoretical Com- puter Science, 80:1–34, 1991. [Val91] Rüdiger Valk. Modelling concurrency by task/flow EN systems. In 3rd Work- shop on Concurrency and Compositionality, number 191 in GMD-Studien, St. Augustin, Bonn, 1991. Gesellschaft für Mathematik und Datenverarbeitung. [Val03] Rüdiger Valk. Object Petri nets: Using the nets-within-nets paradigm. In Jörg Desel, Wolfgang Reisig, and Grzegorz Rozenberg, editors, Advanced Course on Petri Nets 2003, volume 3098 of LNCS, pages 819–848. 2003.