HORNETS are Petri nets that have nets as tokens. There are an algebraic extension of elementary object nets (EOS) with the possibility to mofify the structure of the net-tokens. In previous contributions we investigated elementary HORNETS as well as their subclass of safe elementary HORNETS. We showed that the reachability problem for safe elementary HORNETS requires at least exponential space. We have also showed that exponential space is sufficient. This shows that safe elementary HORNETS are much more complicated than safe elementary object nets (safe EOS), where reachability is known to be PSPACE-complete. In this contribution we study structural restrictions of elementary HORNETS that have a better complexity: fan-bounded HORNETS. It turns out that reachability is again in PSPACE for this class of HORNETS.
In this paper we study self-modifying systems in the formalisms of HORNETS.
HORNETS are a generalisation of object nets [
Fig. 1. An Elementary Object Net System (EOS) 1. System-autonomous: The system net transition btfires autonomously, which moves the net-token from p1 to p2 without changing its marking.
b b 2. Object-autonomous: The object net fires transition t1 “moving” the black token from q1 to q2. The object net remains at its location p1. b 3. Synchronisation: Whenever we add matching synchronisation inscriptions at the system net transition bt and the object net transition t1, then both must fire synchronously: The object net is moved to p2 and the black token moves from q1 to q2 b 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 [
The use of algebraic operations in HORNETS relates them to algebraic higher-order
(AHO) systems [
It is not hard to prove that the general HORNET formalism is Turing-complete. In
[
In our general research 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 [
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 [
In this paper we would like to study restrictions of Elementary HORNETS to obtain
net classes where the reachability requires less than exponential space. From [
The paper has the following structure: Section 2 defines Elementary HORNETS. Since the reachability problem is known to be undecidable even for EOS, we restrict elementary HORNETS 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 PSPACE-complete. 2
Definition of Elementary Hornets (EHORNETS) A multiset m on the set D is a mapping m : D → N. Multisets can also be represented as a formal sum in the form m = Pn
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) − m2(d), 0).
The cardinality of a multiset is |m| := Pd∈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.
Net-Algebras We define the algebraic structure of object nets. For a general
introduction of algebraic specifications cf. [
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 Uk of object nets – the net universe. Each object N ∈ Uk, k ∈ K net is a p/t net N = (PN , TN , preN , postN ). We identify U with Sk∈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, 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 EHORNETS, there is an upper bound for the cardinality of Uk.
Proposition 1 (Lemma 2.1 in [
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 EHORNET 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 p contains net-tokens of kind k (p). Since the net-tokens are b b instances of object nets, a marking is a nested multiset of the form: μ = n X pi[Ni, Mi]
b i=1 where pi ∈ Pb, Ni ∈ Uk(pi), Mi ∈ MS (PNi ), n ∈ N b b (1) (2) (3) Each addend pi[Ni, Mi] denotes a net-token on the place pi that has the structure of b b 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 + μ.
The projection ΠN1,H (μ) is the multiset of all system-net places that contain the object-net N :1 ΠN1,H
Xn i=1 pbi[Ni, Mi] :=
Xn i=1 1N (Ni) · pi b 1 The superscript H indicates that the function is used for HORNETS. where the indicator function 1N is defined as: 1N (Ni) = 1 iff Ni = N .
Analogously, the projection ΠN2,H (μ) is the multiset of all net-tokens’ markings (that belong to the object-net N ): ΠN2,H
Xn i=1 pbi[Ni, Mi] :=
Xn i=1 1k(Ni) · Mi The projection Π2,H (μ) is the sum of all net-tokens’ markings belonging to the k same type k ∈ K: Π2,H (μ) := X k
N∈Uk ΠN2,H (μ) 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 blα = (blαk)k∈K defines the synchronisation constraints. Each transition of the system net is labelled with a multiset blk(t) = (e1, c1) + · · · + b (en, cn), where the expression ei ∈ TkΣ (X) describes the called object net and ci ∈ Ck is a channel. The intention is that bt fires synchronously with a multiset of object net transitions with the same multiset of labels. Each variable assignment α generates the function blαk(bt) defined as: blαk(bt)(N ) := X 1≤i≤n ci for blk(bt) = X α(ei)=N 1≤i≤n (ei, ci) (4)
Each function blαk(bt) 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 (EHORNET) is composed of a system net Nb and the set of object nets U . W.l.o.g. we assume Nb 6∈ U . To guarantee finite algebras for EHORNETS, 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, Gb), 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 Gb : 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: pre(bt)(p), b post(bt)(pb) ∈
MS (TkΣ(pb)(X)) (5)
For each variable binding α we obtain the evaluated functions preα, postα : Tb → (Pb → MS (U )) in the obvious way.
Definition 1 (Elementary Hornet, EHORNET). Assume a fixed many-sorted predicate logic Γ = (Σ, X, E, Ψ ).
An elementary HORNET is a tuple EH = (Nb , U , I, k , l, μ0) such that: 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: 1. Synchronised firing: There is at least one object net that has to be synchronised, i.e. there is a N such that bl(bt)(N ) is not empty.
Such an event is a pair θ = btα[ϑ], where btis 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 bt and ϑ(N ) have matching multisets of labels, i.e. bl(bt)(N ) = lN♯ (ϑ(N )) for all N ∈ U . (Remember that lN♯ denotes the multiset extension of lN .) The intended meaning is that btfires synchronously with all the object net transitions ϑ(N ), N ∈ U . 2. System-autonomous firing: The transition bt of the system net fires autonomously, whenever bl(bt) 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 ∈ 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 p.
b For the sake of uniformity we define for an arbitrary binding α: preα(id pb,N )(pb′)(N ′) = postα(id pb,N )(pb′)(N ′) = (1 0 if p′ = pb ∧ N ′ = N
b otherwise. (6) (7)
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: Θ1 := nτ α[ϑ]
b Θ2 := nid pb,N [ϑt] | p ∈ Pb, N ∈ Uk(p), t ∈ TN
b b | ∀N ∈ U : blα(bt)(N ) = lN♯ (ϑ(N ))o o Firing Rule A system event θ = τbα[ϑ] removes net-tokens together with their individual 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): φEH (τbα[ϑ], λ, ρ) ↔ ∀k ∈ K : ∀p ∈ k −1(k) : ∀N ∈ Uk : ΠN1,H (λ)(p) = preα(τb)(p)(N ) ∧
b b b ∀p ∈ k −1(k) : ∀N ∈ Uk : ΠN1,H (ρ)(p) = postα(τb)(p)(N ) ∧ Πbk2,H (λ) ≥ PN∈Uk pre♯N (ϑ(N )) ∧b b Πk2,H (ρ) = Πk2,H (λ) + PN∈Uk post♯N (ϑ(N )) − pre♯N (ϑ(N ))
The predicate φEH has the following meaning: Conjunct (1) states that the removed sub-marking λ contains on p the right number of net-tokens, that are removed by τ .
b b Conjunct (2) states that generated sub-marking ρ contains on p the right number of b net-tokens, that are generated by τ . Conjunct (3) states that the sub-marking λ enables b 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 btα[ϑid ] the enabling predicate φEH can be simplified further: Conjunct (3) is always true since preN (ϑid (N )) = 0. Conjunct (4) simplifies to Π2,H (ρ) = Π2,H (λ), which means that no token of the object nets get lost k k when a system-autonomous events fires.
Analogously, for an object-autonomous event τ [ϑt] we have an idle-transition τ = b b iΠd N1pb,,′HN (ρan)dfoϑr N=′ ϑ=t Nforansodmtoe Πt. N1C,′Hon(λju)nc=t (01)=anΠdN1(,2′H)(sρi)moptlhifeyrwtoiseΠ. NT1,h′His(λm) ea=nspth=at b λ = pb[M ], M enables t, and ρ = pb[M − preN (bt) + postN (bt)].
Definition 2 (Firing Rule). Let EH be an EHORNET and μ, μ′ ∈ MH markings. – The event τbα[ϑ] is enabled in μ for the mode (λ, ρ) ∈ M2H iff λ ⊑ μ ∧ φEH (τb[ϑ], λ, ρ) holds and the guard Gb(bt) holds, i.e. E |=Iα Gb(τ ). b – An event τ α[ϑ] that is enabled in μ can fire – denoted μ −τb−α−[ϑ−](−λ−,ρ→) μ′.
b 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 τ α[ϑ] in a functional way. b 3
We know from [11, Lemma 3.1] that a safe EHORNET has a finite reachability set. More precisely: There are at most 1 + U (m) · 2m |Pb| different markings, where m is the maximum of all |Pk| and U (m) is the number of object nets. In the general case we have U (m) = 2(24m), 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 number of places in the pre- or postset, i.e. the maximal synchronisation at object-net level.
Definition 3. An elementary HORNET EH = (Nb , U , I, k , l, μ0) is called β-fanbounded whenever all transitions of all object-nets have at most β places in the preand 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 HORNET 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 EHORNET the cardinality of each net universe Uk is bounded for each k ∈ K as follows: |Uk| ≤ 2O(n(4β)) where n := |Pk|. Proof. For a safe, β-fan-bounded EHORNET the number of possible objects is calculated 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: (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: ≤ const · nβ 2 = 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 [
|LTk| ≤ const · n2β 2 = 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 there are |P(LTk)| = 2|LTk| subsets of LTk, we have at most 2O(n(4β)) different object nets. qed.
Thus the of different object nets is only single-exponential for fan-bounded EHORNETS – 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: So, the general analysis is just the special case where the fan-parameter β equals the numer of places m.
For safe, β-fan-bounded EHORNET we can give an upper bound for the number of reachable markings. The number of reachable markings is in 2O(n(4β+1)), i.e. exponential, 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 EHORNET has a finite reachability set.
The number of reachable markings is bounded by 2O(n(4β+1)) where n is the maximum of all |Pk| and |Pb|.
Proof. Analogously Prop. 1 we have at most (1 + U (m) · 2m)|Pb| different markings in the safe HORNET.
For a β-fan-bounded EHORNET we have obtained in Prop. 2 a bound for the number of possible object-nets: |Uk| ≤ U (m) = 2(const·m(4β)). Thus the number of different markings in the safe, β-fan-bounded EHORNET is: (1 + U (m) · 2m)|Pb| ≤
1 + 2(const·m(4β)) · 2m |Pb| ≤ 2(const·m(4β)+m) |Pb| With n := max(m, |Pb|) the bound simplifies to: 2(const·m(4β)·|Pb|) ≤ 2(const·n(4β)·n) = 2(const·n(4β+1)) The number of reachable markings is in 2O(n(4β+1)), i.e. exponential, where the exponent is a polynomial. qed.
The most extreme restriction is to forbid forks and joins at all. In this case we consider elementary HORNETS 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 ESMHORNET (elementary statemachine HORNET) for short. An ESMHORNET is 1-fan-bounded EHORNET by definition. Therefore, we obtain the following corollary of Lemma 3: Corollary 1. A safe ESMHORNET has a finite reachability set. The number of reachable markings is bounded by 2O(n5) where n is the maximum of all |Pk| and |Pb|. 4
As p/t nets are a special subcase of fan-bounded EHORNETS (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 EHORNETS cannot be simpler than for p/t nets, i.e. it is at least PSPACE-hard, since the reachability problem for safe p/t nets is PSPACE-complete. In the following we show that the reachability problem for lies within PSPACE.
Lemma 1. For safe, β-fan-bounded EHORNETS there exists a non-deterministic algorithm 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. The main idea of the algorithm is to guess a firing sequence μ0 −θ→1 μ1 −θ→2 · · · −θ−m−a→x μmax = μ∗, where μ∗ is the marking to be tested for reachability.
By Prop. 3 we know we have at most max = 2O(n(4β+1)) different markings. Therefore, we can safely cut off the computation after max steps.
For each step μi −θ→i μi+1 we choose non-deterministically some event θi. For a given marking μi we guess an event θi and a marking μi+1 and test whether μi −θ→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 transition bt 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 blαk(bt) 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 HORNETS the choice for λ is unique, since there is at most one net-token on each place, which implies that whenever an event btα[ϑ] 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.
After each step μi −θ→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 EHORNETS can be solved within polynomial space.
Proof. We known by Lemma 1 that Reachβ-seH ∈ NSpace(O n(4β+1) ). From Savitch’s Theorem we obtain:
Reachβ-seH ∈ DSpace
O n(4β+1) 2 = DSpace O n2(4β+1)
This proves our central result that the reachability problem for safe, fan-bounded EHORNETS is PSPACE-complete, while it requires exponential space in the general case of safe EHORNETS.