=Paper=
{{Paper
|id=Vol-1269/paper101
|storemode=property
|title=An Upper Bound for the Reachability Problem of Safe, Elementary Hornets
|pdfUrl=https://ceur-ws.org/Vol-1269/paper101.pdf
|volume=Vol-1269
|dblpUrl=https://dblp.org/rec/conf/csp/Kohler-BussmeierH14
}}
==An Upper Bound for the Reachability Problem of Safe, Elementary Hornets==
https://ceur-ws.org/Vol-1269/paper101.pdf
An Upper Bound for the Reachability
Problem of Safe, Elementary Hornets
Michael Köhler-Bußmeier and Frank Heitmann
University of Applied Science Hamburg and University of Hamburg
michael.koehler-bussmeier@haw-hamburg.de
Abstract. In this paper we study the complexity of the reachability
problem Hornets, an algebraic extension of object nets. Here we con-
sider the restricted class of safe, elementary Hornets.
In previous work we established the lower bound, i.e. reachability re-
quires at least exponential space. In another work we have shown we can
simulate elementary Hornets with elemntary object nets Eos, where
reachability is known to be PSpace-complete. Since this simulation leads
to a double exponetial increase in the size of the simulating Eos, we
obtain that for Hornets the reachability problem is solvable in double
exponetial space.
In this contribution we show that the simulation is rather bad, since
we show that exponential space is sufficient, i.e. upper and lower bound
coincide.
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 [1, 2], which follow the nets-within-
nets paradigm as proposed by Valk [3]. 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
t and the object net transition t1 , then both must
the system net transition b
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.
2
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 [4], 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 - i
r - e - i2
i- u v f1
N3 h 1
a- h - b- h r- c- h
ZZ
} q
Zl
s y hi-
3 f3
R - h
@
r
- l
HHj (xky)
p* t Rh i2 - s f2
d - rh - e - h
@
s
l x
=
N1 i u v f
i1- a - i - b - i
r - 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 [5], 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 [6], which are used for
adaptive systems.
It is not hard to prove that the general Hornet formalism is Turing-complete.
In [7] we have proven that there are several possibilities to simulate counter pro-
grams: 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. Here, 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 [2].
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
3
object net systems ( Eos) [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
Hornets. As a result we obtain the class of safe, elementary Hornets – in
analogy to the class of safe Eos [8].
We have shown in [8, 9] 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 a previous publication [10] we have shown that safe, elementary Hornets
are beyond PSpace. We have shown a lower bound, i.e. that “the reachability
problem requires exponential space” for safe, elementary Hornets – similarily
to well known result of for bounded p/t nets [11]. In [12] we have shown that each
elementary Hornet EH can be simulated by an Eos OS(G(EH )). Therefore,
we can reduce the reachability problem for safe, elementary Hornets to the
one for safe Eos.
Unfortunaltely, the construction of the simulating Eos OS(G(EH )) as given
in Theorem 3 of [12] leads to an Eos that is double-exponentially larger than
the Hornet EH , which establishes the fact that the reachability problem for
safe, elementary Hornets requires at most double-exponential space.
In this paper we give establish an upper bound in a more direct fashion. We
will give an decision procedure which needs at most exponential space, which
shows that lower and upper bound coincide.
The paper has the following structure: Section 2 defines Elementary Hor-
nets. Since the reachability problem is known to be undecidable even for Eos,
we restrict elementary Hornets to safe ones. Safe, elementary Hornets have
finite state spaces. In Section 3 we present a decision procedure for reachability
that operates within exponential space. Since we know that exponential space
is also a lower bound for the problem, the algorithm is optimal. The work ends
with a conclusion.
2 Definition of 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.
0
Any mapping Pfn : D → DPextends to a multiset-homomorphism f ] : MS (D) →
0 ] n
MS (D ) by f ( i=1 xi ) = i=1 f (xi ).
4
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:
t
m ∈ MS (P ). We denote the enabling of t in marking m by m → − . Firing of t is
t
denoted by m → − m0 .
2.1 Elementary Hornets (eHornets)
Net-Algebras We define the algebraic structure of object nets. For a general
introduction of algebraic specifications cf. [13].
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. Each object N ∈ USk , k ∈ K net is a p/t net N =
(PN , TN , preN , postN ). We identify U with k∈K Uk in the following. We as-
sume 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 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 ∈ 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 .
4|Pk |
Proposition 1 (Lemma 2.1 in [10]). For each k ∈ K we have |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.
5
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 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 v on nested multisets
by setting µ1 v µ2 iff ∃µ : µ2 = µ1 + µ.
1,H
The projection ΠN (µ) is the multiset of all system-net places that contain
the object-net N :1
Xn 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’ mark-
ings (that belong to the object-net N ):
Xn 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 (µ) := 2,H
ΠN (µ) (3)
N ∈Uk
Synchronisation The transitions in an Hornet are labelled with synchronisation
inscriptions. We assume a fixed set of channels C = (Ck )k∈K .
k
– The function family b lα = (b
lα )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. The intention is that b t fires synchronously with
a multiset of object net transitions with the same multiset of labels. Each
k b
variable assignment α generates the function b lα (t) defined as:
X X
k b
lα
b (t)(N ) := 1≤i≤n
ci for b lk (b
t) = (ei , ci ) (4)
α(ei )=N 1≤i≤n
k b
lα
Each function b (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. au-
tonously.
1
The superscript H indicates that the function is used for Hornets.
6
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 sys-
tem net N b 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 N b = (Pb, Tb, pre, post, G),
b where each arc is labelled
with a multiset of terms: pre, post : T → (P → MS (TΣ (X))). Each transition
b b
is labelled by a guard predicate G b : Tb → PLΓ . The places of the system net are
typed by the function k : P → K. As a typing constraint we have that each arc
b
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α :
T → (Pb → MS (U)) in the obvious way.
b
Definition 1 (Elementary Hornet, eHornet). Assume a fixed many-sorted
predicate logic Γ = (Σ, X, E, Ψ ).
b , U, I, k , l, µ0 ) such that:
An elementary Hornet 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.
2.2 Events and Firing Rule
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(b
t)(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.
]
(Remeber 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
generated by the function ϑid , defined as ϑid (N ) = 0 for all N ∈ U.
7
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 0 ) = {t}
if N = N 0 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 pb0 = pb ∧ N 0 = N
p0 )(N 0 ) = postα (id pb,N )(b
preα (id pb,N )(b p0 )(N 0 ) =
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
individual internal markings. Firing the event replaces a nested multiset λ ∈ MH
that is part of the current marking µ, i.e. λ v µ, 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)
Πk2,H (λ) ≥ N ∈Uk pre]N (ϑ(N )) ∧
P
Πk2,H (ρ) = Πk2,H (λ) + N ∈Uk post]N (ϑ(N )) − pre]N (ϑ(N ))
P
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. 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 φEH can be
simplified further: Conjunct (3) is always true since preN (ϑid (N )) = 0. Conjunct
(4) simplifies 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
1,H
τb = id pb,N and ϑ = ϑt for some t. Conjunct (1) and (2) simplify to ΠN 0 (λ) =
8
1,H 0 1,H 1,H
pb = ΠN 0 (ρ) for N = N and to ΠN 0 (λ) = 0 = ΠN 0 (ρ) 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 eHornet and µ, µ0 ∈ MH mark-
ings.
– The event τbα [ϑ] is enabled in µ for the mode (λ, ρ) ∈ M2H iff λ v µ ∧
φEH (b
τ [ϑ], λ, ρ) holds and the guard G(
b bt) holds, i.e. E |=α
I G(b
b τ ).
τbα [ϑ](λ,ρ)
– An event τbα [ϑ] that is enabled in µ can fire – denoted µ −−−−−−→ µ0 .
EH
– The resulting successor marking is defined as µ0 = µ − λ + ρ.
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 Reachability for Hornets
In the following we study the complexity of the reachability problem for safe
eHornets.
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.
Proposition 2 (Lemma 3.1 [10]). A safe eHornet has a finite reachability
4m
|Pb|
set. There are at most 1 + 2(2 ) · 2m different markings, where m is the
maximum of all |Pk |.
The huge number of object nets in the set Uk of object nets and reachable
markings (cf. Prop. 2) leads to the following result.
Proposition 3 (Theorem 5.1 in [10]). The reachability problem for safe
eHornets requires at least exponential space.
The proof we have given in [10] is similar to the heart of Lipton’s famous
result. In [10] we simulate a counter program C by a safe eHornet EH of
size O(poly(|C|)). Thus we know that a question about a counter program C
translates into a question about
√ EH. When C needs 2|A| space for the counters,
n
|A|
we have that EH needs 2 space for the corresponding question, where n is
the order of the polynom poly(|C|).
In [12] we have given a reduction of the reachability problem for safe eHor-
nets to that of safe Eos. We have shown, that for a safe eHornet EH the
simulating Eos OS(EH) is safe, too. Since we know that the reachability prob-
lem for safe Eos is PSpace-complete [8], we can use the simulating Eos to
decide the reachability problem for EH. We have shown that the simulating
9
Eos OS(G(EH )) increases double-exponentially in size. Let m be the maximum
of all |Pk |. Then, we obtain a space complexity of:
4m
4m O(m)
POLY 2O(2 ) = 2POLY ·O(2 ) = 22
Proposition 4 (Theorem 3 in [12]). The reachability problem ReachseH for
O(m)
safe eHornets is in DSpace 22 .
This implies quite a big gap between the lower bound (exponential space)
and the upper bound resulting from the simulation (double-exponential space).2
Fortunately, simulation is not the only way to obtain an upper complexity bound.
In the following we give a more direct approach with a better complexity. As a
first step we give a non-deterministic algorithm to decide reachability of µ1 .
In the following, we assume that all evaluations of terms and predicates need
at most 2O(m) bits.
Lemma 1. There exists a non-determistic algorithm that decides the reachabil-
ity problem ReachseH for safe eHornets within exponential space: ReachseH ∈
NSpace(2O(m) ), where m is the maximum of all |Pk |.
Proof. The main idea of the following algorithm is to guess a firing sequence
θ1 θ2 θn
µ0 −→ µ1 −→ · · · −→ µn = µ∗ , where µ∗ is the marking to be tested for
reachability.
m
By Prop. 2 we know we have at most 2O(2 ) different markings in the safe
O(m)
Hornet. Therefore, we can safely cut off the computation after 22 steps –
whenever µ∗ is reachable it is reachable by a firing sequence without loops.
function reach(EH : eHornet, µ∗ : Marking): boolean is
O(m)
c := 22
µ := µ0
found := (µ = µ∗ )
while ¬found ∧ c > 0 do
choose non-deterministically an event btα [ϑ](λ, ρ)
tα (λ,ρ)
b
if µ −−−−→ then
EH
µ := µ − λ + ρ // the resulting successor marking
c := c − 1
found := (µ = µ∗ )
else
return false
end while
return found
2
This was to expect, since we have a long ‘chain’ of “recycled” techniques: the simu-
lating Eos OS(G(EH )) and the PSpace algorithm for Eos.
10
θ i
In each step µi −→ µi+1 we choose non-deterministically some event θi .
How much space is needed to store an event? Note, that each common set
of places Pk is finite for eHornets. 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 transition 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 ∈ Uk 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 |
Now we can quantify the amount of space needed for the event θ:
1. We select some system net transition b t.
2. We guess a variable binding α. For each variable in var (b t) of kind k we select
t)|·24m )
some object net from the universe Uk . We have Uk | |var (b
t)|
≤ 2(|var
(b
candidates for the obejct net. Each choice needs log |var (b t)| · 24m ∈ 2O(m)
bits of space. (Compared to the other aspects, the variable binding α uses a
major part of the space needed.)
k b
3. For each kind k we have the multiset of channels b lα (t) to synchronise with.
k b
Whenever lα (t)(N ) is not the empty multiset 0, then we have to select a
b
multiset of transitions from TN ) (with corresponding channel inscriptions).
k b k b
The number of channels used is |b lα (t)|. For each of these |b lα (t)| channels we
have non-deteministically select one labelled object net transition from the
set LTk . We have at most
|blαk (bt)| bk b
bk b
= 2( k∈K |lα (t)|·4·|Pk |) ∈ 2O(m)
Y P
|LTk ||lα (t)| ≤ 24·|Pk |
k∈K
different choices for the synchronisation partner and therefore at most 2O(m)
different synchronisation functions ϑ.
4. We check whether b t and ϑ(N ) have matching multisets of labels, i.e. b
l(b
t)(N ) =
]
lN (ϑ(N )) for all N ∈ U.
5. 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 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 we select one of the net-tokens generated in the postset, i.e. on the
places t• ∩ d−1 (N ).
Since |t• ∩d−1 (N )| =: c is constant, we have at most c|PN | ∈ 2O(|PN |) = 2O(m)
different modes.
11
All these choices need at most 2O(m) bits of space.
tα (λ,ρ)
b
We then check whether the event is enable, i.e. whether µ −−−−→ holds.
1. We test α v µ. This holds iff ∃µ00 : µ = α + µ00 . Since α and µ are known,
this can be tested by ‘tagging’ all addends from α in µ, which needs at most
2O(m) bits.
2. We evaluate the guard predicate G( t).
b b
3. The resulting successor marking is defined as µ0 = µ − λ + ρ. Here, µ − λ are
those addends, that have not been tagged. Adding ρ needs at most 2O(m)
bits.
O(m)
Since we have at most 22 different reachable markings, the markings µ0 ,
µ1 , µ, and µ0 are storable in 2O(m) bits. The counter c is storable in 2O(m) bits,
too. Therefore, the whole algorithm needs at most 2O(m) bits of space to decide
reachability for eHornets. qed.
We use a well known fact about non-deterministic space complexity:
Theorem 1 (Savitch). For each place constructible function s(n) ≥ log(n) we
have NSpace(s(n)) ⊆ DSpace(s2 (n)).
Now we use the technique of Savitch to construct a deterministic algorithm
from the non-determistic algorithm above.
Theorem 2. The reachability problem ReachseH for safe eHornets can be solved
within exponential space: ReachseH ∈ DSpace(2O(m) ).
Proof. We known by Lemma 1 that ReachseH ∈ NSpace(2O(m) ).
2
From Savitch’s Theorem we obtain that ReachseH ∈ DSpace 2O(m) =
DSpace 22·O(m) = DSpace 2O(m) . qed.
4 Conclusion
In this paper we studied the subclass of safe eHornets. While reachability is
PSpace-complete for safe Eos, we obtain that the reachability problem for safe
eHornets requires at leats exponential space.
Our result here tightens a previous result for the upper bound of reachability.
[12] establishes a double exponential space complexity using a simple reduction
technique. Here, we have shown that exponential space is sufficient, i.e. upper
and lower bound are equal.
We like to emphasise that the power of safe eHornets 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.
12
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 Lecture Notes in Computer Science., 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 Lecture Notes in Computer Science., Springer-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 Lecture Notes in Computer Science., Springer-Verlag (2005) 268 –
288
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
Lecture Notes in Computer Science. 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 The-
ory of Petri Nets (ICATPN’2009). Volume 5606 of Lecture Notes in Computer
Science., Springer-Verlag (2009) 243–262
8. Köhler-Bußmeier, M., Heitmann, F.: Safeness for object nets. Fundamenta Infor-
maticae 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.: On the complexity of safe, elementary Hornets. In: Proceed-
ings of the International Workshop on Concurrency, Specification, and Program-
ming (CS&P 2012). Volume 928., CEUR Workshop Proceedings (2012)
11. Lipton, R.J.: The reachability problem requires exponential space. Research Re-
port 62, Dept. of Computer science (1976)
12. Köhler-Bußmeier, M., Heitmann, F.: Complexity results for elementary Hornets.
In Colom, J.M., Desel, J., eds.: PETRI NETS 2013. Volume 7927 of Lecture Notes
in Computer Science., Springer-Verlag (2013) 150–169
13. Ehrig, H., Mahr, B.: Fundamentals of algebraic Specification. EATCS Monographs
on TCS. Springer-Verlag (1985)