Structural and Dynamic Restrictions of Elementary Ob ject Systems

Abstract

Elementary object systems (Eos for short) are Petri nets in which tokens may be Petri nets again. Originally proposed by Valk for a two levelled structure, the formalism was later generalised for arbitrary nesting structures. However, even if restricted to a nesting depth of two, Eos are Turingcomplete and thus many problems like reachability and liveness are undecidable for them. Nonetheless, since they are useful to model many practical applications a natural question is how to restrict the formalism in such a way, that the resulting restricted formalism is still helpful in a modelling context, but so that important verification problems like reachability become quickly decidable. In the last years several structural and dynamic restrictions for Eos have therefore been investigated. These investigations have been central to the first author's recent PhD thesis and have been published in past CS&P conferences. In this paper we add several new results and present them together with the old in a unified fashion highlighting the central message of these investigations.

-

Object Petri Nets are Petri Nets whose tokens may be Petri Nets again and thus may have an inner structure and activity. This approach is useful to model mobile systems and other systems arising in Computer Science which enjoy a certain nesting of structures (cf. [ 13 ] and [ 14 ]).

This approach, which is also called the nets-within-nets paradigm, was proposed by Valk [ 27, 28 ] for a two levelled structure and generalised in [ 15, 16 ] for arbitrary nesting structures. By now many related approaches like recursive nets [ 6 ], nested nets [ 24 ], adaptive workflow nets [ 25 ], AHO systems [ 11 ], PN2 [ 10 ], Mobile Systems [ 23 ], and many others are known. Another line of research also dealing with nesting, but not in the field of Petri nets, is concerned with process calculi. Arguably most prominently there are the Ambient Calculus of Gordon and Cardelli [ 1 ] and the Seal Calculus [ 2 ] among many others. See [ 18 ] and [ 7 ] for a detailed discussion.

Unfortunately even if restricted to a two level structure as in elementary object systems, the formalism is Turing-complete. A natural question is how to restrict the formalism in such a way, that the resulting restricted formalism is still helpful in a modelling context, but so that important verification problems like reachability become quickly decidable. This “borderline” between modelling power and fast algorithms is in the case of p/t nets usually drawn at free choice Petri nets.

In the following we survey several structural restrictions for Eos and give results concerning the complexity of the reachability problem. Since we conclude, that even in very restricted cases the reachability problem becomes practically hard to decide, we then survey dynamic restrictions of Eos, most notably a safeness notion. Here, too, we focus on the complexity on the reachability problem.

The following section gives fundamental definitions of Eos. In Section 3 we survey results on structural restrictions and in Section 4 we survey results on dynamic restrictions. The paper ends with a summary of these results and a conclusion.

In the following we assume basic knowledge of Petri nets, see e.g. [ 26 ] and of Eos, see e.g. [ 18 ]. We do not define all notions rigorously here due to space restrictions, but all notions and an in-depth study can be found in [ 7 ]. 2

Fundamentals

An elementary object system (Eos) is composed of a system net and a set of object nets where each of these nets is a p/t net. While the object nets use the usual black tokens, the system net’s places are marked with either black tokens or object nets. For this each place of the system net is typed with an object net with the meaning the only object nets of these type may rest on that place. Additionally each transition may be labelled with a channel. The meaning here is that transitions with the same label may only fire synchronously. De nition 1 (EOS). An elementary object system ( Eos) is a tuple OS = (Nb , N , d, l) such that: 1. Nb is a p/t net, called the system net. 2. N is a finite set of disjoint p/t nets, called object nets. 3. d : Pb → N is the typing of the system net places. 4. l = (bl, (lN )N∈N ) is the labelling.

An Eos with initial marking is a tuple OS = (Nb , N , d, l, µ0) where µ0 ∈ M is the initial marking.

A system net transition may be labelled with a channel for each object net. Where an object net transition is only labelled with one channel. If for example a system net transition bt is labelled with channel c1 for the object net N1 and with channel c2 for object net N2, then btmay only fire, if it is possible to synchronously fire a transition in N1 which is labelled with channel c1 and if it is possible to synchronously fire a transition in N2 which is labelled with channel c2. Firing may also happen system-autonomously (an unlabelled system net transition fires independently from any object net transition) or object-autonomously (firing of an unlabelled object net transition)

A formal treatment can be found in e.g. [ 9 ]. We only give an example here to illustrate the main points of the firing rule.

Example 1. Figure 1 shows an Eos with the system net Nb and the object nets N = {N1, N2}. The system has four net-tokens: two on place p1 and one on p2 and p3 each. The net-tokens on p1 and p2 share the same net structure, but have independent markings.

Formally we have the system net Nb = (Pb, Tb, pre, post) with the places and transitions given by Pb = {p1, . . . , p6} and Tb = {t}, the object net N1 = (P1, T1, pre1, post1) with P1 = {a1, b1} and T1 = {t1} and the the object net N2 = (P2, T2, pre2, post2) with P2 = {a2, b2, c2} and T2 = {t2}. The typing is given by d(p1) = d(p2) = d(p4) = N1 and d(p3) = d(p5) = d(p6) = N2.

We have two channels ch1 and ch2. The labelling function bl of the system net is defined by bl(t)(N1) = ch1 and bl(t)(N2) = ch2. The labelling lN1 of the first object net is defined by setting lN1 (t1) = ch1. Similarly, lN2 is defined by lN2 (t2) = ch2.

There is only one (synchronous) event: Θ = Θl = {t[N1 7→ t1, N2 7→ t2]}. The event is also written shortly as t[t1, t2].

The initial marking µ has two net-tokens on p1, one on p2, and one on p3: µ = p1[a1 + b1] + p1[0] + p2[a1] + p3[a2 + b2] Note that for Figure 1 the structure is the same for the three net-tokens on p1 and p2 but the net-tokens’ markings are different.

The marking µ enables t[N1 7→ t1, N2 7→ t2] in the mode (λ, ρ), where µ = p1[0] + p1[a1 + b1] + p2[a1] + p3[a2 + b2] = p1[0] + λ λ = p1[a1 + b1] + p2[a1] + p3[a2 + b2] ρ = p4[a1 + b1 + b1] + p5[0] + p6[c2]

The net-tokens’ markings are added by the projections ΠN2 resulting in the markings ΠN2 (λ). The sub-synchronisation generate ΠN2 (ρ). (The results are shown above and below the transition t in Figure 2.) After the synchronisation we obtain the successor marking µ′ with net-tokens on p4, p5, and p6 as shown in Figure 2: µ′ = (µ − λ) + ρ = p1[0] + ρ

= p1[0] + p4[a1 + b1 + b1] + p5[0] + p6[c2]

For general Eos the following theorem holds due to K¨ohler-Bußmeier [ 12 ]. Theorem 1 (Kohler 2007). Eos can simulate 2-counter machines. Important problems like reachability and liveness are thus undecidable.

In the following two sections we focus on introducing structural and dynamic restrictions that result in a decidable reachability problem. 3

Structural Restrictions

The main reason why Eos are Turing-complete is a null-test that is possible due to the firing rule. In Figure 3 the system net transition bt1 is not able to fire: the object net in the preset has a token on place a1. This token would have to be distributed among the places of the same object net type in the postset of bt1, but there is no such place. The transition bt2 to the right may fire. The object net’s marking is 0 and so there are no tokens that need to be distributed.

Conservative Eos avoid this by demanding that each object net type that appears in the preset of a system net transition also appears in the postset of that transition.

De nition 2 (Conservative Eos). A typing is called conservative iff (d(•bt) ∪ {•}) ⊆ (d(bt•) ∪ {•}), i.e. each object net type that appears in the preset of bt also appears in its postset.

An Eos is conservative iff its typing d is.

While boundedness and coverability become decidable for conservative Eos, reachability and liveness remain undecidable. This was proven in [ 12 ] and [ 21 ]. Theorem 2. For conservative Eos boundedness and coverability are decidable, while reachability and liveness are undecidable.

The idea in the definition of conservative Eos can be strengthen further by demanding that each object net type appears exactly once in the preset and the postset of a system net transition or does not appear at all. This leads to generalised state machines (GSM) which are suitable to model many practical applications, since each object net can be seen as a physical entity. De nition 3 (Generalised State Machines). Let G = (Nb , N , d, l, µ0) be an Eos. G is a generalised state machine (GSM) iff for all N ∈ N \ {N•} 1. ∀bt ∈ Tb : |{pb ∈ •bt | d(pb) = N }| = |{pb ∈ bt• | d(pb) = N }| ≤ 1 2. ∑pb∈Pb;d(pb)=N Π1(µ0)(pb) ≤ 1 holds.

In [ 17 ]) it was shown that for each GSM a p/t net, called reference net, can be easily constructed from which decidability results follow (see [ 12 ] and [ 17 ]). Theorem 3. The reachability problem is decidable for generalised state machines.

While this is a first positive result, the set of transitions is defined by the set of events of the GSM and the size of this set can become exponential in the size of the GSM.

Lemma 1 ([ 8 ], [ 9 ]). Let |T | := max{|TN | | N ∈ N } then |Θ| ≤ |Tb| · |T ||N |.

Given a GSM it might thus be very expensive to construct its reference net. This exponential blow up stems from the fact that in a GSM a m : nsynchronisation between the system net and the object nets exists, i.e. if there are m system net transitions labelled with channel c for object net N1 and if in N1 n transitions are labelled with channel c then each of the m system net transitions may fire synchronously with each of the n object net transitions, resulting in m · n different events.

To prevent this, we introduced deterministic GSMs and Eos in [ 8 ] (see also [ 9 ]). De nition 4 (Deterministic and Strongly Deterministic Eos). A Eos OS is called deterministic if for each N ∈ N and every two transitions t, t′ ∈ TN , t ̸= t′ with lN (t) ̸= τ ̸= lN (t′), lN (t) ̸= lN (t′) holds, i.e. if the labels for all all t ∈ TN with lN (t) ̸= τ are pairwise different.

OS is strongly deterministic if OS is deterministic and additionally for all bt and N with bl(bt)(N ) ̸= τ the labels bl(bt)(N ) are pairwise different.

Thus, in a deterministic Eos or GSM each channel is used at most once in each object net (resulting in a m : 1-synchronisation). In a strongly deterministic Eos or GSM each channel is additionally used at most once in the system net (resulting in a 1 : 1-synchronisation).

For Eos the definition of determinism does not significantly reduce the power of the formalisms introduced so far, namely of Eos or conservative Eos. Theorem 4 ([ 7 ]). The reachability problem for strongly deterministic, deterministic and general Eos is undecidable - even if the Eosis conservative.

However, for GSMs the size of the events and thus the size of the reference net is reduced considerably.

Lemma 2 ([ 7 ]). Let G = (Nb , N , d, l, µ0) be a deterministic or strongly deterministic GSM, then |Θ| is bounded above by |Tb| + ∑N∈N |TN |.

However, strongly deterministic GSMs can still simulate p/t nets and thus the reachability problem remains ExpSpace-hard.

Theorem 5 ([ 7 ]). Every p/t net system N can be simulated by a strongly deterministic GSM GN .

Corollary 1 ([ 7 ]). The reachability problem for strongly deterministic, deterministic and general GSMs is ExpSpace-hard.

Due to this results further structural restrictions are necessary to reduce the complexity of the reachability problem. Several structural restrictions known from p/t nets are carried over to GSMs and investigated in [ 8 ], [ 9 ], [ 21 ], and [ 7 ].

The results are summarised in Table 1. ttGSMs, ppGSMs, ptGSMs, and tpGSMs are GSMs where the system net and/or the object nets are restricted to be T-nets or P-nets. In ptGSMs the system net is a P-net and the object nets are T-nets and in tpGSMs the system net is a T-net and the object nets are Pnets. Despite being rather simple in the case of p/t nets, it is evident in Table 1, that the reachability problem becomes hard in the case of object nets due to the synchronisation between the system net and the object nets. Most notably in the case of ppGSMs where all participating nets are P-nets and thus similar to finite automata, the reachability problem is already PSpace-complete.

acGSMs are GSMs where all nets are acylic and fcGSMs are GSMs where all nets are free-choice nets. For cfGSMs the definition of conflict-freedom has to be adapted, because it is not enough to demand a similar structural restrictions as for p/t nets if one wants to structurally rule out conflicts (cf. [ 8 ] and [ 7 ]). De nition 5 (Con ict-Free GSMs ([ 8 ])). A GSM OS = (Nb , N , d, l, µ0) is conflict-free if 1. ∀N ∈ N ∪ {Nb } ∀p ∈ Pb ∪ PN : |p•| > 1 ⇒ p• ⊆ •p 2. ∀N ∈ N ∀p ∈ PN : (∃t ∈ p• ∃bt1, bt2 ∈ Tb ∃pb ∈ Pb ∃c ∈ C : bt1 ̸= bt2 ∧ pb ∈ •bt1 ∩ •bt2 ∧ d(pb) = N ∧ lN (t) = bl(bt1)(N ) = bl(bt2)(N ) = c) ⇒ p ∈ t• holds. We also say that OS is a cfGSM.

Proofs for the results in Table 1 can be found in [ 7 ] with pointers to the literature where the results where first proven.

Most notably in Table 1 are the results for ppGSMs and for fcGSMs. They show that even very strong structural restrictions as in the case of ppGSMs lead to an already hard to solve reachability problem and that more openly structural restrictions as in the case of fcGSMs where the formalism would be suitable for modelling purposes lead to complexity results that render algorithms practically unusable. Thus other restrictions than structural restrictions are necessary if one aims at solving the reachability problem quickly. 4

Dynamics Restrictions

In [ 7 ] unary and persistent Eos are introduced where in unary Eos in each reachable marking at most one event is enabled and in persistent Eos conflicts are dynamically ruled out. For both formalisms, however, the reachability problem remains undecidable. These dynamical restrictions are thus not strong enough for our purpose.

In general, the state space of an Eos is of infinite size which is a source for undecidability results or strong lower complexity bounds. In [ 19 ] we therefore introduced four different notions of safeness for Eos, safe(1), safe(2), safe(3), and safe(4), to adapt the notion of safeness for p/t nets to Eos. For p/t nets 1-safeness guarantees not only finiteness of the state space size but also that each reachable marking can be seen as a set. This set idea is adapted in [ 19 ]. Furthermore, a safe(4) Eos is also a safe(3) Eos which is in turn a safe2 Eos and so on. Positive results concerning the solvability of the reachability problem thus carry over from safe(i) to safe(i + 1) and negative results carry over from safe(i + 1) to safe(i).

However, despite the fact that the markings are sets, safe(1) and safe(2) Eosstill have an infinite state space and the reachability problem remains undecidable for them even if the Eos is additionally structurally restricted. Theorem 6 ([ 19 ], [ 7 ]). The reachability problem is undecidable for safe(1) or safe(2) Eos - even in the case of strongly deterministic and conservative Eos.

In the following we concentrate on safe(3) Eos which have a finite state space.

De nition 6 (Safeness). An Eos OS is safe(3) or simply safe iff for all reachable markings there is at most one token on each system net place and each net-token is safe: ∀µ ∈ RS (OS ) : ∀pb ∈ Pb : Π1(µ)(pb) ≤ 1 ∧

∀N ∈ N : ∀p ∈ PN : ∀pb[M ] ≤ µ : M (p) ≤ 1 Theorem 7 ([ 19 ], [ 7 ]). If an Eos is safe(3) or safe(4), then its set of reachable markings is finite.

Indeed, an upper bound for the state space size if given in [ 7 ]. Let k := |Pb| and l := max{|PN | | N ∈ N }, then there are at most (1+2l)k different markings.

For safe Eos two very strong result can be shown. Not only are reachability and liveness decidable, but every property that can be expressed in the temporal logics LTL or CTL can be decided in polynomial space in the size of the Eos and the formula. The the problems are PSpace-hard follows directly from similar results for safe p/t nets (see e.g. [ 5 ]). It is thus surprising that this bound can also be met from above in the case of safe Eos despite their quite huge state space.

Theorem 8 ([ 19 ], [ 7 ]). Given a safe(3) or safe(4) Eos OS and an LTL formula ϕ, checking whether OS satisfies ϕ can be done in polynomial space in the size of OS and ϕ, that is, there is a polynomial p, independent of OS and ϕ, such that the algorithm uses O(p(|OS | + |ϕ|)) space.

Corollary 2. The reachability problem for safe Eos is PSpace-complete. Theorem 9 ([ 20 ], [ 7 ]). Given a safe(3) or safe(4) Eos OS and a CTL formula ϕ checking whether OS satisfies ϕ can be done in O(|OS |4 · |ϕ|) space. Corollary 3. The liveness problem for safe Eos is PSpace-complete.

Both model checking algorithms are an adaption of a technique from Esparza for 1-safe p/t nets [ 5 ]. The LTL model checking algorithms additionally uses techniques from Vardi from automata theory [ 29 ].

The proofs of the above theorems are very involved. Detailed discussions and proofs can be found in [ 19 ], [ 20 ], and [ 7 ].

In addition to the results above it can also be decided in polynomial space if an Eos is safe(3), which is helpful from a modelling point of view. Theorem 10 ([ 7 ]). Given an Eos OS it is PSpace-complete to decide if OS is safe.

Safe Eos can in addition be structurally restricted. In some cases as in the case of conflict-free Eos this reduces the complexity of the reachability problem (cf. Table 2). However, the formalisms where this happens seem to be too restricted to be useful in a modelling context.

A discussion of structural restrictions of safe(1) and safe(2) Eos can be found in [ 7 ]. 5

Conclusion and Outlook

In summary we have investigated formalisms which are useful to model mobility, interaction, and nesting of structures. We then focused on object nets, but it is possible to adapt these results for other formalisms mentioned in the introduction. Since in their general form object nets are Turing-complete it was our goal to restrict the formalism of elementary object systems such that modelling capabilities mostly remain and interesting applications can still be conveniently modelled, and also such that properties can be automatically and quickly verified.

To achieve this goal we have restricted the formalism structurally and dynamical. We introduced restrictions natural for object nets like determinism and strong determinism and carried over restrictions known from p/t nets to object nets. We then focused on the complexity of the reachability problem to evaluate the formalisms. The results are summarised in Table 1 and 2.

As a conclusion structural restrictions alone are not enough even if the possibility to synchronise is additionally restricted. The restriction to safe(3) Eos,however, allows for a quick verification of important properties and is also still useful from a modelling point of view.

In [ 7 ] Eos and GSMs are furthermore generalised to an arbitrary but fixed nesting depth k > 2. In this case a safeness definition can also be introduced which allows to carry over the results for CTL and LTL model checking. These problems are then solvable in polynomial space, too, albeit the polynomial worsens.

Also in [ 7 ] object net systems are introduced, which allow a vertical transport of net tokens, i.e. a transport of net tokens between nesting levels. For this systems different safeness definitions are introduced in [ 7 ]. In particular, it is not enough to demand that on each place resides at most one (net) token. Due to the arbitrary nesting depth, the state space might still be infinite. However, for the strongest safeness definition for object net systems in [ 7 ], which among other things does not allow the creation and destruction of net tokens, again PSpacecompleteness results for LTL- and CTL-model-checking can be established.

Open question in the context presented here are, obviously, to match upper and lower bounds in the tables above. While this might be interesting from a theoretical point of view, the effect for the question tackled here are limited. The open cases are for formalisms which are structurally restricted in such a way, that using them in a modelling context is doubtful. Thus even if the reachability problem is solvable more quickly than PSpace the formalisms will not be practically useful.

Another open question concerns the borderline between safe(1) and safe(2) Eos and the borderline between safe(3) and safe(4) Eos. While it is known that e.g. for safe(3) and safe(4) Eos the reachability problem is PSpace-complete, the polynomial will almost surely be smaller for safe(4) Eos. Again this question is more from a theoretical nature.

A question with much practical relevance is how to improve the LTL- and CTL-model-checking algorithms uses so far in this context. In [ 7 ] the algorithm are rather direct and not optimised. It is to be expected that these algorithms can be improved. Afterwards, it would be nice to implement these algorithms in a tool which can then be used by modellers. We believe that such a tool might be very useful in practice, since many applications can be modelled more intuitively with object nets and such a tool would allow to verify properties of the model automatically and with modest time and space requirements.

Questions not tackled so far which would open up whole new directions are compositionality and adaptivity. The goal in compositionality is to find properties and restrictions such that properties of the whole system can than be deduced from properties of components treated in isolation. This might reduce the complexity considerably. First results concerning compositionality with regard to nested nets are published in [ 3 ] and [ 4 ].

Adaptivity means to introduce formalisms which do not only allow a transport of net tokens as presented here, but also to manipulated these net tokens during run-time. First formalisms which allow this are adaptive workflow nets [ 25 ] and higher order nets [ 22 ].

This two questions, how to introduce compositionality and adaptivity for object nets, are the questions we want to tackle in the future. We believe that they will be of high practical relevance for run-time analysis of systems in general and workflows in particular.

References

1. Luca Cardelli and Andrew D. Gordon . Mobile ambients . Theoretical Computer Science , 240 : 177 - 213 , 2000 .

2. G. Castagna , J. Vitek , and F. Zappa Nardelli . The seal calculus . Information and Computation , 201 : 1 - 54 , 2005 .

3. Leonid W. Dworzan ´ski and Irina A . Lomazova . On compositionality of boundedness and liveness for nested Petri nets . In Marcin Szczuka, Ludwik Czaja, Andrzej Skowron, and Magdalena Kacprzak, editors, Concurrency, Speci cation and Programming (CS&P 2011) , Proceedings, Pultusk, Poland, 2011 . Bialystok University of Technology.

4. Leonid W. Dworzan ´ski and Irina A . Lomazova . On compositionality of boundedness and liveness for nested Petri nets . Fundamenta Informaticae , 120 ( 3-4 ): 275 - 293 , 2012 .

5. Javier Esparza . Decidability and complexity of petri net problems - an introduction . In Wolfgang Reisig and Grzegorz Rozenberg , editors, Lectures on Petri Nets I: Basic Models, Advances in Petri Nets , volume 1491 of Lecture Notes in Computer Science, pages 374 - 428 . Springer-Verlag, 1998 .

6. Serge Haddad and Denis Poitrenaud . Theoretical aspects of recursive Petri nets . In S. Donatelli and J. Kleijn, editors, Application and Theory of Petri Nets , volume 1639 of Lecture Notes in Computer Science, pages 228 - 247 . Springer-Verlag, 1999 .

7. Frank Heitmann . Algorithms and Hardness Results for Object Nets . PhD thesis , University of Hamburg, 2013 .

8. Frank Heitmann and Michael Ko¨ hler -Bußmeier. On defining conflict-freedom for object nets . In B. Farwer and M. Ko¨ hler-Bußmeier, editors, Proceedings of the Second International Workshop on Logic, Agents, and Mobility (LAM 2011 ), 2011 .

9. Frank Heitmann and Michael Ko¨hler-Bußmeier. P- and t-systems in the netswithin-nets-formalism . In Serge Haddad and Lucia Pomello , editors, Application and Theory of Petri Nets. 33rd International Conference, PETRI NETS 2012 . Hamburg, Germany, June 2012 . Proceedings, volume 7347 of Lecture Notes in Computer Science, pages 368 - 387 . Springer-Verlag, 2012 .

10. Kunihiko Hiraishi . PN2: An elementary model for design and analysis of multiagent systems . In Farhad Arbab and Carolyn L. Talcott, editors, Coordination Models and Languages , COORDINATION 2002 , volume 2315 of Lecture Notes in Computer Science, pages 220 - 235 . Springer-Verlag, 2002 .

11. Kathrin Hoffmann , Hartmut Ehrig, and Till Mossakowski . 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, pages 268 - 288 . Springer-Verlag, 2005 .

12. Michael K¨ohler . The reachability problem for object nets . Fundamenta Informaticae , 79 ( 3-4 ): 401 - 413 , 2007 .

13. Michael K ¨ohler, Daniel Moldt, and Heiko R¨olke. Modeling the behaviour of Petri net agents . In J. M. Colom and M. Koutny, editors, Application and Theory of Petri Nets , volume 2075 of Lecture Notes in Computer Science , pages 224 - 241 . Springer-Verlag, 2001 .

14. Michael K ¨ohler, Daniel Moldt, and Heiko R ¨olke. Modelling mobility and mobile agents using nets within nets . In W. v. d. Aalst and E. Best, editors, Application and Theory of Petri Nets , volume 2679 of Lecture Notes in Computer Science, pages 121 - 140 . Springer-Verlag, 2003 .

15. Michael K¨ohler and Heiko R¨olke. Concurrency for mobile object-net systems . Fundamenta Informaticae , 54 ( 2-3 ), 2003 .

16. Michael K¨ohler and Heiko R ¨olke. Properties of Object Petri Nets . In J. Cortadella and W. Reisig, editors, Application and Theory of Petri Nets , volume 3099 of Lecture Notes in Computer Science, pages 278 - 297 . Springer-Verlag, 2004 .

17. Michael K¨ohler and Heiko R ¨olke. Reference and value semantics are equivalent for ordinary object petri nets . In G. Ciardo and P. Darondeau, editors, Application and Theory of Petri Nets , volume 3536 of Lecture Notes in Computer Science, pages 309 - 328 . Springer-Verlag, 2005 .

18. Michael Ko¨ hler -Bußmeier. Decidability results for elementary object systems . Report of the department of informatics , Universit¨at Hamburg, Fachbereich Informatik, 2011 .

19. Michael K ¨ ohler -Bußmeier and Frank Heitmann . Safeness for object nets . Fundamenta Informaticae , 101 ( 1-2 ): 29 - 43 , 2010 .

20. Michael Ko¨hler-Bußmeier and Frank Heitmann. Liveness of safe object nets . Fundamenta Informaticae , 112 ( 1 ): 73 - 87 , 2011 .

21. Michael Ko¨hler-Bußmeier and Frank Heitmann. Conservative elementary object systems . Fundamenta Informaticae , 120 ( 3-4 ): 325 - 339 , 2012 .

22. Michael K ¨ ohler -Bußmeier and Frank Heitmann . Complexity results for elementary hornets . In Jos´e-Manuel Colom and J¨org Desel, editors, Application and Theory of Petri Nets and Concurrency. 34th International Conference, PETRI NETS 2013 . Milan, Italy, June 24-28, 2013 . Proceedings, volume 7927 of Lecture Notes in Computer Science, pages 150 - 169 . Springer-Verlag, 2013 .

23. Charles Lakos . A Petri net view of mobility . In Formal Techniques for Networked and Distributed Systems (FORTE 2005 ), volume 3731 of Lecture Notes in Computer Science, pages 174 - 188 . Springer-Verlag, 2005 .

24. Irina A. Lomazova. Nested Petri nets - a formalism for specification of multi-agent distributed systems . Fundamenta Informaticae , 43 ( 1-4 ): 195 - 214 , 2000 .

25. Irina A. Lomazova , Kees M. van Hee , Olivia Oanea , Alexander Serebrenik, Natalia Sidorova, and Marc Voorhoeve . Nested nets for adaptive systems . In Petri Nets and Other Models of Concurrency - ICATPN 2006. 27th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency , Turku, Finland, June 26-30, 2006 . Proceedings, volume 4024 of Lecture Notes in Computer Science, pages 241 - 260 . Springer-Verlag, 2006 .

26. Wolfgang Reisig and Grzegorz Rozenberg, editors. Lectures on Petri Nets I: Basic Models , volume 1491 of Lecture Notes in Computer Science. Springer-Verlag, 1998 .

27. Ru ¨diger Valk. Modelling concurrency by task/flow EN systems . In 3rd Workshop on Concurrency and Compositionality , number 191 in GMD-Studien, St. Augustin, Bonn, 1991 . Gesellschaft fu¨r Mathematik und Datenverarbeitung.

28. Ru ¨diger Valk. Object Petri nets: Using the nets-within-nets paradigm . In J¨org Desel , Wolfgang Reisig, and Grzegorz Rozenberg, editors, Advanced Course on Petri Nets 2003 , volume 3098 of Lecture Notes in Computer Science, pages 819 - 848 . Springer-Verlag, 2003 .

29. Moshe Vardi . An automata-theoretic approach to linear temporal logic . In F. Moller and G. Birtwistle, editors, Logics for Concurrency: Structure versus Automata , volume 1043 of Lecture Notes in Computer Science, pages 238 - 266 . Springer-Verlag, 1996 .