Complexity Studies for Safe and Fan-Bounded Elementary Hornets Michael Köhler-Bußmeier and Frank Heitmann michael.koehler-bussmeier@haw-hamburg.de heitmann@informatik.uni-hamburg.de Abstract. H ORNETS are Petri nets that have nets as tokens. There are an alge- braic extension of elementary object nets (E OS) with the possibility to mofify the structure of the net-tokens. In previous contributions we investigated elementary H ORNETS as well as their subclass of safe elementary H ORNETS. We showed that the reachability problem for safe elementary H ORNETS requires at least exponen- tial space. We have also showed that exponential space is sufficient. This shows that safe elementary H ORNETS are much more complicated than safe elemen- tary object nets (safe E OS), where reachability is known to be PS PACE-complete. In this contribution we study structural restrictions of elementary H ORNETS that have a better complexity: fan-bounded H ORNETS. It turns out that reachability is again in PS PACE for this class of H ORNETS. Key words: Hornets, nets-within-nets, object nets, reachability, safeness 1 Hornets: Higher-Order Object Nets In this paper we study self-modifying systems in the formalisms of H ORNETS. H OR - NETS are a generalisation of object nets [1, 2], which follow the nets-within-nets paradigm as proposed by Valk [3]. Fig. 1. An Elementary Object Net System (E OS) 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 example given in Figure 1: 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 . 77 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 syn- chronously: 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 H ORNETS 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 [4], where algebraic data types replace the anonymous black tokens. The use of algebraic operations in H ORNETS relates them to algebraic higher-order (AHO) systems [5], which are restricted to two-levelled systems but have a greater flex- ibility for the operations on net-tokens, since each net transformation is allowed. There is also a relationship to Nested Nets [6], which are used for adaptive systems. It is not hard to prove that the general H ORNET formalism is Turing-complete. In [7] 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 our general research we like to study the complexity that arises due the algebraic structure. Therefore, we restrict H ORNETS 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 H ORNETS. However this restriction does not guarantee finite state spaces, since we have the nesting depth as a second source of undecidability [2]. Second, we restrict the universe of object nets to finite sets. Finally, we restrict the nesting depth and introduce the class of elementary H ORNETS, which have a two-levelled nesting structure. This is done in analogy to the class of elementary object net systems (E OS) [1], which are the two-level specialisation of general object nets [1, 2]. 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 H ORNETS. As a result we obtain the class of safe, elementary H ORNETS – in analogy to the class of safe E OS [8]. We have shown in [8–10] that most problems for safe E OS are PS PACE- complete. More precisely: All problems that are expressible in LTL or CTL, which includes reachability and liveness, are PS PACE-complete. This means that with respect to these problems safe E OS are no more complex than p/t nets. In a previous publication [11] we have shown that safe, elementary H ORNETS are beyond PS PACE. We have shown a lower bound, i.e. that “the reachability problem requires exponential space” for safe, elementary H ORNETS – similarly to well known result of for bounded p/t nets [12]. In [13] we give an algorithm thats needs at most exponential space, which shows that lower and upper bound coincide. In this paper we would like to study restrictions of Elementary H ORNETS to obtain net classes where the reachability requires less than exponential space. From [11] we know that the main source of complexity for E H ORNETS is mainly due to the huge number of different of net-tokens, which is double-exponential for safe E H ORNETS. A closer look reveals that the number of net-token’s marking is rather small – “only” single-exponential, while the number of different object nets is double-exponential. We conclude that restricting the net-tokens’ marking beyond safeness would not improve complexity. Instead, we have to impose structural restrictions on the object-nets. Petri 78 net theory offers several well known candidates for structural restrictions, like state machines, free-choice nets etc. Here, we restrict object-nets to state-machines. The paper has the following structure: Section 2 defines Elementary H ORNETS. Since the reachability problem is known to be undecidable even for E OS, we restrict elementary H ORNETS to safe ones, which have finite state spaces. State Machines have at most one place in the pre- and in the post-set. In Section 3 we generalise this notion in the way that the number of all places in pre- and postset of an object-net is below a given bound. So, we obtain the maximal synchronisation degree of the objects nets (i.e. the maximal pre- and postset size) as a fresh complexity parameter. Section 4 shows that the reachability problem is PS PACE-complete. 2 Definition of Elementary Hornets (E H ORNETS) Pn m : D → N. Multisets can also be represented A multiset m on the set D is a mapping 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(m1 (d) P − 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 mappingPf : D → D Pnextends to a multiset-homomorphism f : MS (D) → ′ ♯ n MS (D ) by f ( i=1 xi ) = i=1 f (xi ). A p/t net N is a tuple N = (P, T, pre, post), such that P is a set of places, T is a set of transitions, with P ∩ T = ∅, and pre, post : T → MS (P ) are the pre- and post-condition functions. A marking of N is a multiset of places: m ∈ MS (P ). We t t denote the enabling of t in marking m by m − → m′ . →. Firing of t is denoted by m − Net-Algebras We define the algebraic structure of object nets. For a general introduc- tion of algebraic specifications cf. [14]. Let K be a set of net-types (kinds). A (many-sorted) specification (Σ, X, E) con- sists 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 Uk of object nets – the net universe. Each object N S ∈ Uk , k ∈ K net is a p/t net N = (PN , TN , preN , postN ). We identify U with k∈K Uk in the following. We assume the family U = (Uk )k∈K to be disjoint. The nodes of the object nets in Uk are not disjoint, since the firing rule allows to transfer tokens between net tokens within the same set Uk . Such a transfer is possible, 79 if we assume that all nets N ∈ Uk have the same set of places Pk . Pk is the place universe for all object nets of kind k. 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 ∈ Uk use only a finite subset of Pk , i.e. ∀N ∈ U : |• TN ∪ TN • | < ∞. The family of object nets U is the universe of the algebra. A net-algebra (U, I) assigns to each constant σ ∈ Σλ,k an object net σ I ∈ Uk and to each operator σ ∈ Σk1 ···kn ,k with n > 0 a mapping σ I : (Uk1 × · · · × Ukn ) → Uk . A net-algebra is called finite if Pk is a finite set for each k ∈ K. Since all nets N ∈ Uk have the same set of places Pk , which is finite for E H ORNETS, there is an upper bound for the cardinality of Uk . Proposition 1 (Lemma 2.1 in [11]). For each k ∈ K the cardinality of each net uni- 4|Pk | verse Uk is bound as follows: |Uk | ≤ 2(2 ). A variable assignment α = (αk : Xk → Uk )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. Nested Markings A marking of an E H ORNET assigns to each system net place one or many net-tokens. The places of the system net are typed by the function k : Pb → K, meaning that a place pb contains net-tokens of kind k (b p). Since the net-tokens are instances of object nets, a marking is a nested multiset of the form: n X µ= pbi [Ni , Mi ] where pbi ∈ Pb, Ni ∈ Uk (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 ). The set of all nested multisets is denoted as MH . We define the partial order ⊑ on nested multisets by setting µ1 ⊑ µ2 iff ∃µ : µ2 = µ1 + µ. 1,H The projection ΠN (µ) is the multiset of all system-net places that contain the object-net N :1 X n  Xn 1,H ΠN pbi [Ni , Mi ] := 1N (Ni ) · pbi (1) i=1 i=1 where the indicator function 1N is defined as: 1N (Ni ) = 1 iff Ni = N . 2,H Analogously, the projection ΠN (µ) is the multiset of all net-tokens’ markings (that belong to the object-net N ): X n  Xn 2,H ΠN pbi [Ni , Mi ] := 1k (Ni ) · Mi (2) i=1 i=1 The projection Πk2,H (µ) is the sum of all net-tokens’ markings belonging to the same type k ∈ K: X Πk2,H (µ) := ΠN 2,H (µ) (3) N ∈Uk 1 The superscript H indicates that the function is used for H ORNETS. 80 Synchronisation The transitions in an H ORNET are labelled with synchronisation in- scriptions. We assume a fixed set of channels C = (Ck )k∈K . – The function family b lα = (b k lα )k∈K defines the synchronisation constraints. Each transition of the system net is labelled with a multiset b lk (b t) = (e1 , c1 ) + · · · + (en , cn ), where the expression ei ∈ TkΣ (X) describes the called object net and ci ∈ Ck is a channel. The intention is that b t fires synchronously with a multiset of object net transitions with the same multiset of labels. Each variable assignment α generates the function b k b lα (t) defined as: X X bk b lα (t)(N ) := ci for b lk (b t) = (ei , ci ) (4) 1≤i≤n α(ei )=N 1≤i≤n Each function bk b lα (t) assigns to each object net N a multiset of channels. – For each N ∈ Uk the function lN assigns to each transition t ∈ TN either a channel c ∈ Ck or ⊥k , whenever t fires without synchronisation, i.e. autonomously. System Net Assume we have a fixed logic Γ = (Σ, X, E, Ψ ) and a net-theory (U, I). An elementary higher-order object net (E H ORNET) is composed of a system net N b and b the set of object nets U. W.l.o.g. we assume N 6∈ U. To guarantee finite algebras for E H ORNETS , we require that the net-theory (U, I) is finite, i.e. each place universe Pk is finite. The system net is a net Nb = (Pb, Tb, pre, post, G),b where each arc is labelled with b b a multiset of terms: pre, post : T → (P → MS (TΣ (X))). Each transition is labelled by a guard predicate G b : Tb → PLΓ . The places of the system net are typed by the function k : Pb → K. As a typing constraint we have that each arc inscription has to be a multiset of terms that are all of the kind that is assigned to the arc’s place: k (b p) pre(b t)(b p), post(b t)(b p) ∈ MS (TΣ (X)) (5) For each variable binding α we obtain the evaluated functions preα , postα : Tb → b (P → MS (U)) in the obvious way. Definition 1 (Elementary Hornet, E H ORNET). Assume a fixed many-sorted predicate logic Γ = (Σ, X, E, Ψ ). b , U, I, k , l, µ0 ) such that: An elementary H ORNET is a tuple EH = (N 1. Nb is an algebraic net, called the system net. 2. (U, I) is a finite net-theory for the logic Γ . 3. k : Pb → K is the typing of the system net places. 4. l = (bl, lN )N ∈U is the labelling. 5. µ0 ∈ MH is the initial marking. Events The synchronisation labelling generates the set of system events Θ. We have three kinds of events: 81 1. Synchronised firing: There is at least one object net that has to be synchronised, i.e. there is a N such that b l(bt)(N ) is not empty. Such an event is a pair θ = b tα [ϑ], where 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. ϑ(N ) ∈ MS (TN ). It is required that b t and ϑ(N ) have matching multisets of ♯ ♯ labels, i.e. b l(b t)(N ) = lN (ϑ(N )) for all N ∈ U. (Remember that lN denotes the multiset extension of lN .) The intended meaning is that b t fires synchronously with all the object net transitions ϑ(N ), N ∈ U. 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 gen- erated by the function ϑid , defined as ϑid (N ) = 0 for all N ∈ U. 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 )(bp′ )(N ′ ) = postα (id pb,N )(bp′ )(N ′ ) = 0 otherwise. The set of all events generated by the labelling l is Θl := Θ1 ∪ Θ2 , where Θ1 contains synchronous events (including system-autonomous events as a special case) and Θ2 contains the object-autonomous events: n o ♯ Θ1 := τbα [ϑ] | ∀N ∈ U : b lα (b t)(N ) = lN (ϑ(N )) n o (6) Θ2 := id pb,N [ϑt ] | pb ∈ Pb, N ∈ Uk (bp) , t ∈ TN Firing Rule A system event θ = τbα [ϑ] removes net-tokens together with their individ- ual internal markings. Firing the event replaces a nested multiset λ ∈ MH 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 : φEH (b 1,H p ∈ k −1 (k) : ∀N ∈ Uk : ΠN ∀b (λ)(b p) = preα (b p)(N ) ∧ τ )(b −1 1,H ∀b p ∈ k (k) : ∀N ∈ Uk : ΠN (ρ)(b p) = postα (b p)(N ) ∧ τ )(b (7) P Πk2,H (λ) ≥ N ∈Uk pre♯N (ϑ(N )) ∧ P Πk2,H (ρ) = Πk2,H (λ) + N ∈Uk post♯N (ϑ(N )) − pre♯N (ϑ(N )) The predicate φEH 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. 82 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 additional tokens in the net-tokens. For system-autonomous events b tα [ϑid ] the enabling predicate φEH can be simpli- fied further: Conjunct (3) is always true since preN (ϑid (N )) = 0. Conjunct (4) sim- plifies to Πk2,H (ρ) = Πk2,H (λ), 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 τb = 1,H id pb,N and ϑ = ϑt for some t. Conjunct (1) and (2) simplify to ΠN ′ (λ) = p b = 1,H ′ 1,H 1,H Π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 (bt)]. Definition 2 (Firing Rule). Let EH be an E H ORNET and µ, µ′ ∈ MH markings. – The event τbα [ϑ] is enabled in µ for the mode (λ, ρ) ∈ M2H iff λ ⊑ µ ∧ φEH (b b b τ [ϑ], λ, ρ) holds and the guard G(t) holds, i.e. E |=α b τ ). I G(b τb α [ϑ](λ,ρ) – An event τbα [ϑ] that is enabled in µ can fire – denoted µ −−−−−−→ µ′ . EH – The resulting successor marking is defined as µ′ = µ − λ + ρ. Note, that the firing rule has no a-priori decision how to distribute the marking on the generated net-tokens. Therefore we need the mode (λ, ρ) to formulate the firing of τbα [ϑ] in a functional way. 3 Fan-Bounded Safe, Elementary H ORNETS We know from [11, Lemma 3.1] that a safe E H ORNET has a finite reachability set. More |Pb | precisely: There are at most 1 + U (m) · 2m different markings, where m is the maximum of all |Pk | and U (m) is the number of object nets. In the general case we 4m have U (m) = 2(2 ) , which dominates the bound. It is double-exponential, while the number of different marking wihin each net-token is 2m , i.e. “only” single-exponential. The huge number of object nets is the source of the exponential space requirement for the reachability problem. Therefore, if one wants to require less than exponential space one has to restrict the structure of possible object nets in Uk . The huge number of object-nets in Uk arises since we allow object nets with any number of places in the preset or postset, i.e. unbounded joins or forks. Therefore it seems promising to restrict the synchronisation degree. In the following we want to restrict the number of object-nets in Uk . We forbid unbounded joins or forks. From a practical point of view this can be considered as a rather unlikely. From a theoretical point of view we can take this into account with an parametrised complexity analysis. The parameter considered here is the maximal 83 number of places in the pre- or postset, i.e. the maximal synchronisation at object-net level. Definition 3. An elementary H ORNET EH = (N b , U, I, k , l, µ0 ) is called β-fan- bounded whenever all transitions of all object-nets have at most β places in the pre- and in the postset: ∀k ∈ K : ∀N ∈ Uk : ∀t ∈ TN : |• t| ≤ β ∧ |t• | ≤ β The fan-bound of EH is defined as: β(EH ) := max {|• t|, |t• | : k ∈ K : N ∈ Uk : t ∈ TN } Note, that an elementary H ORNET is always fan-bounded, since PN ⊆ Pk and Pk is always finite in the elementary case: β(EH ) ≤ |Pk | < ∞. Proposition 2. For a safe, β-fan-bounded E H ORNET the cardinality of each net uni- (4β) verse Uk is bounded for each k ∈ K as follows: |Uk | ≤ 2O(n ) where n := |Pk |. Proof. For a safe, β-fan-bounded E H ORNET the number of possible objects is calcu- lated as follows: Each possible transition t chooses a subset of Pk for the preset • t and another subset for the postset t• with the constraint that these subsets have a cardinality of at most β. The number of these subsets is: β  [  β  X        Pk |Pk | |Pk | |Pk | |Pk | = = + + ··· + i=0 i i=0 i 0 1 β  (Here Ai denote the set of all subsets of A that have cardinality i.) We identify t with the pair (• t, t• ). The number of different transitions is:    2 |Pk | |Tk | = + |P1k | + · · · + |Pβk | 0  2 (n)β ≤ 1 + n + n·(n−1) 2! · · · + β!  β 2 ≤ const · n = const · n(2β)  So, the number of different transitions is in O n2β .2 The set of labelled transitions is LTk := Tk × (Ck ∪ {⊥k }) and we have |LTk | = |Tk × (Ck ∪ {⊥k })| different labelled transitions. We cannot use more channels than we have transitions in the object net, i.e. we could use at most |Tk | different channels from Ck ∪ {⊥k }. Thus, we have: |LTk | = |Tk | · (|Ck | + 1) ≤ |Tk | · |Tk | 2 Note, that while the bound we have given for the general case in Lemma 2.1 in [11] is strict (i.e. there are Hornets that exactly have this number of object-nets) the calculation given here gives us only an upper bound. 84 From |Tk | ≤ const · n(2β) we obtain: 2 |LTk | ≤ const · n2β = const · n(4β)  Thus the set of labelled transitions is in O n(4β) , i.e. a polynomial in the number of places n = |Pk | where the degree of the polynomial is given by the fan-parameter β. Since each object net N in Uk is characterised by its set of labelled transitions and (4β) there are |P(LTk )| = 2|LTk | subsets of LTk , we have at most 2O(n ) different object nets. qed. Thus the of different object nets is only single-exponential for fan-bounded E H OR - NETS – and not double-exponential as in the general case. Note, that the set of transitions is a polynomial in the number of places m where the degree is given by the fan-parameter β = β(m) ≤ m. Of course if we have transitions that use all the places in the pre- or postset, i.e. β = m we have an exponential number as before, since:      2  2 |Pk | |Pk | |Pk | |Tk | = + + ··· + = 2|Pk | = 2(2|Pk |) 0 1 m So, the general analysis is just the special case where the fan-parameter β equals the numer of places m. For safe, β-fan-bounded E H ORNET we can give an upper bound for the number of (4β+1) reachable markings. The number of reachable markings is in 2O(n ) , i.e. exponen- tial, where the exponent is a polynomial in the number of places n where the degree is given by the fan-parameter β. Proposition 3. A safe, β-fan-bounded E H ORNET has a finite reachability set. (4β+1) The number of reachable markings is bounded by 2O(n ) where n is the maxi- b mum of all |Pk | and |P |. b| |P Proof. Analogously Prop. 1 we have at most (1 + U (m) · 2m ) different markings in the safe H ORNET. For a β-fan-bounded E H ORNET we have obtained in Prop. 2 a bound for the number (4β) of possible object-nets: |Uk | ≤ U (m) = 2(const·m ) . Thus the number of different markings in the safe, β-fan-bounded E H ORNET is: b|  (4β) |Pb | ≤ 1 + 2(const·m ) · 2m |P (1 + U (m) · 2m )  (4β) |Pb | ≤ 2(const·m +m)  (4β) |Pb | ≤ 2(const·m ) (4β) b = 2(const·m ·|P |) With n := max(m, |Pb|) the bound simplifies to: (4β) (4β) (4β+1) 2(const·m b |) ·|P ≤ 2(const·n ·n) = 2(const·n ) 85 (4β+1) The number of reachable markings is in 2O(n ) , i.e. exponential, where the expo- nent is a polynomial. qed. The most extreme restriction is to forbid forks and joins at all. In this case we consider elementary H ORNETS that have state-machines as object-nets only, i.e. ∀k ∈ K : ∀N ∈ Uk : ∀t ∈ TN : |• t| ≤ 1 ∧ |t• | ≤ 1 An elementary Hornet with this restriction is called E S M H ORNET (elementary state- machine H ORNET) for short. An E S M H ORNET is 1-fan-bounded E H ORNET by defini- tion. Therefore, we obtain the following corollary of Lemma 3: Corollary 1. A safe E S M H ORNET has a finite reachability set. The number of reach- 5 able markings is bounded by 2O(n ) where n is the maximum of all |Pk | and |Pb|. 4 Complexity of the Reachability Problem As p/t nets are a special subcase of fan-bounded E H ORNETS (we simply restrict the system net to a single place with the p/t net of interest as the unique net-token) the reachability problem for safe, fan-bounded E H ORNETS cannot be simpler than for p/t nets, i.e. it is at least PS PACE-hard, since the reachability problem for safe p/t nets is PS PACE-complete. In the following we show that the reachability problem for lies within PS PACE. Lemma 1. For safe, β-fan-bounded E H ORNETS there exists a non-deterministic algo- rithm that decides the reachability problem  within polynomial space: Reachβ-seH ∈ NSpace O n(4β+1) where n is the maximum of all |Pk | and |Pb|. Proof. Whenever µ∗ is reachable it is reachable by a firing sequence without loops. θ1 θ2 θ The main idea of the algorithm is to guess a firing sequence µ0 −→ µ1 −→ · · · −−max −→ ∗ ∗ µmax = µ , where µ is the marking to be tested for reachability. (4β+1) By Prop. 3 we know we have at most max = 2O(n ) different markings. There- fore, we can safely cut off the computation after max steps. θi For each step µi −→ µi+1 we choose non-deterministically some event θi . For a θi given marking µi we guess an event θi and a marking µi+1 and test whether µi −→ µi+1 holds.  – The markings µi and µi+1 can be stored in O n(4β+1) bits, i.e. polynomial space. – The event θi can be stored in polynomial bits: The choice for the system net tran- sition b t fits in polynomial space. The variable binding α selects for each variable in the arc inscriptions some object net from the universe Uk . Since we have always have a finite number of variables polynomial space is sufficient. For each kind k we have the multiset of channels b k b lα (t) to synchronise with. In the proof of Prop 2 we have seen that we have at most const · n(4β) labelled transitions in the object nets, i.e. polynomial space is sufficient. We guess a mode (λ, ρ). (Since we consider safe H ORNETS the choice for λ is unique, since there is at most one net-token on each 86 place, which implies that whenever an event b tα [ϑ] is enabled, then λ is uniquely determined. For the multiset ρ, we use the fact that for each place in the object net N we have at most one token to distribute over all generated net-tokes. For each net N ∈ Uk we select one of the net-tokens generated in the postset. All these choices need at most polynomial many bits. – To check whether the event is enabled we have to whether test α ⊑ µ. This holds iff ∃µ′′ : µ = α + µ′′ . Since α and µ are known, this can be tested in-place by ‘tagging’ all addends from α in µ. Finally we check whether the successor marking µ′ = µ − λ + ρ is equal to µi+1 . This can be done in-place as µ − λ are those addends, that have not been tagged. θ i After each step µi −→ µi+1 we decrement a counter (which has been initialised with the maximal sequence length max ), forget µi , and repeat the procedure with µi+1 again until either the marking of interested is reached or the counter reaches zero. As each step can be tested in polynomial space, the whole algorithm needs at most polynomial many bits to decide reachability. qed. Now we use the technique of Savitch to construct a deterministic algorithm from the non-deterministic algorithm above. Proposition 4. The reachability problem Reachβ-seH for safe β-fan-bounded E H OR - NETS can be solved within polynomial space.  Proof. We known by Lemma 1 that Reachβ-seH ∈ NSpace(O n(4β+1) ). From Sav- itch’s Theorem we obtain:   2     (4β+1) Reachβ-seH ∈ DSpace O n = DSpace O n2(4β+1) This proves our central result that the reachability problem for safe, fan-bounded E H ORNETS is PS PACE -complete, while it requires exponential space in the general case of safe E H ORNETS. References 1. Köhler, M., Rölke, H.: Properties of Object Petri Nets. In Cortadella, J., Reisig, W., eds.: International Conference on Application and Theory of Petri Nets 2004. Volume 3099 of LNCS, Springer-Verlag (2004) 278–297 2. Köhler-Bußmeier, M., Heitmann, F.: On the expressiveness of communication channels for object nets. Fundamenta Informaticae 93 (2009) 205–219 3. Valk, R.: Object Petri nets: Using the nets-within-nets paradigm. In Desel, J., Reisig, W., Rozenberg, G., eds.: Advanced Course on Petri Nets 2003. Volume 3098 of LNCS, Sprin- ger-Verlag (2003) 819–848 4. Reisig, W.: Petri nets and algebraic specifications. Theoretical Computer Science 80 (1991) 1–34 5. Hoffmann, K., Ehrig, H., Mossakowski, T.: High-level nets with nets and rules as tokens. In: Application and Theory of Petri Nets and Other Models of Concurrency. Volume 3536 of LNCS, Springer-Verlag (2005) 268 – 288 87 6. Lomazova, I.: Nested petri nets for adaptive process modeling. In Avron, A., Dershowitz, N., Rabinovich, A., eds.: Pillars of Computer Science. Volume 4800 of LNCS, Springer-Verlag (2008) 460–474 7. Köhler-Bußmeier, M.: Hornets: Nets within nets combined with net algebra. In Wolf, K., Franceschinis, G., eds.: International Conference on Application and Theory of Petri Nets (ICATPN’2009). Volume 5606 of LNCS, Springer-Verlag (2009) 243–262 8. Köhler-Bußmeier, M., Heitmann, F.: Safeness for object nets. Fundamenta Informaticae 101 (2010) 29–43 9. Köhler-Bußmeier, M., Heitmann, F.: Liveness of safe object nets. Fundamenta Informaticae 112 (2011) 73–87 10. Köhler-Bußmeier, M.: A survey on decidability results for elementary object systems. Fun- damenta Informaticae 130 (2014) 99–123 11. Köhler-Bußmeier, M.: On the complexity of the reachability problem for safe, elementary Hornets. Fundamenta Informaticae 129 (2014) 101–116 12. Lipton, R.J.: The reachability problem requires exponential space. Research Report 62, Dept. of Computer science (1976) 13. Köhler-Bußmeier, M., Heitmann, F.: An upper bound for the reachability problem of safe, elementary hornets. In Popova-Zeugmann, L., ed.: Proceedings of the 23rd International Workshop on Concurrency, Specification and Programming (CS&P). Number 1269 in CEUR Workshop Proceedings (2014) 101–112 14. Ehrig, H., Mahr, B.: Fundamentals of algebraic Specification. EATCS Monographs on TCS. Springer-Verlag (1985)