In distributed systems (like e.g. applications based on micro services or multi-agent system) robustness is a major research topic [1]. In some of our previous work on availability [2,3,4], we observed that the analysis required an additional model part where we have to specify our assumptions about 'sources' of unreliability. So, there are two models: the system itself and the error model. The error model usually requires specific domain knowledge. Therefore, the approach is not applicable out-of-the-box.

As a rule of thumb, in micro service or container-based architectures we assume that the unit of failure is a service/container. More generally, we assume that each 'computational unit' is a source of failure. Here, we follow the let it crash approach -as popularised by the programming language Erlang -and assume that our computational units are either operational or completely crashed, i.e., we have a crash failure model opposed to a Byzantine error model [5].

Petri nets [6] are a standard model for distributed systems. For traditional Petri net models, including coloured variants, it is hard to identify such computational units since any subnet of the net could represent one of them. Therefore, we need additional domain knowledge to identify these sub-nets as the whole structure does not provide clear hints to identify them. 1Our main goal is to derive the computational units directly from the system model -without the use of domain knowledge. For Nets-within-Nets as proposed by Valk [7] we have a natural candidate to describe such a localised service: the net-tokens. They are clearly localized and can be understood as computational entities. This idea is also applicable to other models having an explicit notion of computational context, like the Ambient Calculus [8] or the 𝜋-calculus [9]. But, for most formalisms the borderlines of computational contexts are not that obvious and usually have to be identified with the modeller's help.

After we have identified net-tokens as computational units it is straightforward to define robustness: Robustness means that the system still provides its service even when one or more units are malfunctioning. Here, we model a malfunction by a complete deactivation of a net-token, which provides no observable inner activity any more. To formally express the crash-failure of computational units we define a state space extension where we have so called crash or break-down events.

Our main application area are multi-agent systems (MAS). The first author uses nets-withinnets to specify adaptivity of agents in the context MAS-organisations [10] where one considers large-scale and and agent-independent aspects of MAS, like roles, norms, positions, interaction protocols etc. His MAS-organisation framework Sonar [11] is based on Petri nets, which facilitates the definition of the semantics as well as the analysis. For these Sonar-MAS the agents are modelled as net-tokens within the overall MAS organisation net. The natural unit to break-down is an agent (i.e. a net-token), so our concept of robustness fits well here.

We like to mention some limitations of our idea: Obviously, our let it crash assumption is not fulfilled in general; but it matches with our main research area, i.e., adaptive agents, where agent is any active computational entity, like services, containers, mobile devices, etc. Additionally, we admit that for a quantitative analysis, like in [12], a fault-model is still needed.

The paper has the following structure. Section 2 introduces base nets-within-nets (Eos). Section 3 defines the concept of robustness for Eos: The definition extends the reachability graph with additional events that model a break-down. In Section 4 we show that this semantic extension can be characterized syntactically by a slight modification of the Eos structure. The work closes with a conclusion and outlook.

Object nets [13,14,15], follow the nets-within-nets paradigm as proposed by Valk [7]. Other approaches adapting the nets-within-nets approach are nested nets [16], mobile predicate/transition nets [17], Reference nets [18], PN 2 [19], hypernets [20], and adaptive workflow nets [21]. There are relationships to Rewritable Petri nets [22] and Reconfigurable Petri Nets [23]. Object Nets can be seen as the Petri net perspective on contextual change, in contrast to the Ambient Calculus [8] or the 𝜋-calculus [9], which form the process algebra perspective. With nets-within-nets we study Petri nets where tokens are Petri nets in turn, i.e., we have nested markings. For the class of elementary object net systems (Eos), we restrict the nesting to two levels [13,15]. 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 ̂︀ 𝑡 fires autonomously, which moves the net-token from ̂︀ 𝑝 1 to ̂︀ 𝑝 2 without changing its marking.

2. Object autonomous: The object net fires transition 𝑡 1 by "moving" the black token from 𝑞 1 to 𝑞 2 . The object net remains at its location ̂︀ 𝑝 1 .

3. Synchronisation: Whenever we add matching synchronisation inscriptions at the system net transition ̂︀ 𝑡 and the object net transition 𝑡 1 , then both must fire synchronously: The object net is moved to ̂︀ 𝑝 2 whereas the black token moves from 𝑞 1 to 𝑞 2 inside. Whenever synchronisation is specified, autonomous actions are forbidden. An elementary object system (Eos) is composed of a system net, which is a p/t net ̂︀ 𝑁 = ( ̂︀ 𝑃 , ̂︀ 𝑇 , pre, post), and a set of object nets 𝒩 = {𝑁 1 , . . . , 𝑁 𝑛 }, which are p/t nets given as 𝑁 = (𝑃 𝑁 , 𝑇 𝑁 , pre 𝑁 , post 𝑁 ), where 𝑁 ∈ 𝒩 . We assume ̂︀ 𝑁 ̸ ∈ 𝒩 and the existence of the empty object net • ∈ 𝒩 , which models black tokens. The system net places are typed by the mapping 𝑑 : ̂︀ 𝑃 → 𝒩 meaning that a place ̂︀ 𝑝 ∈ ̂︀ 𝑃 of the system net may only contain net-tokens of the object net type 𝑑(̂︀ 𝑝) = 𝑁 . No place of the system net is mapped to the system net itself since ̂︀ 𝑁 ̸ ∈ 𝒩 . Since the tokens of an Eos are instances of object nets, a marking of an Eos is a nested multiset. A marking of an Eos OS is denoted 𝜇 = ∑︀ 𝑛 𝑘=1 (̂︀ 𝑝 𝑘 , 𝑀 𝑘 ), where ̂︀ 𝑝 𝑘 is a place of the system net and 𝑀 𝑘 is the marking of a net-token with type 𝑑(̂︀ 𝑝 𝑘 ). To emphasise the nesting, markings are also denoted as 𝜇 = ∑︀ 𝑛 𝑘=1 ̂︀ 𝑝 𝑘 [𝑀 𝑘 ]. For example, the marking show in Fig. 1 is

. The set of all markings which are syntactically consistent with the typing 𝑑 is denoted ℳ, where 𝑑 −1 (𝑁 ) ⊆ ̂︀ 𝑃 is the set of system net places of the type 𝑁 :

Analogously to markings, which are nested multisets 𝜇, the events of an Eos are also nested. An Eos allows three different kinds of events: system-autonomous, synchronous, and objectautonomous events. The set of events is denoted Θ (cf. the appendix for details).

). An elementary object system (Eos) is a tuple OS = ( ̂︀ 𝑁 , 𝒩 , 𝑑, Θ, 𝜇 0 ), where:

1. ̂︀ 𝑁 is a p/t net, called the system net.

2. 𝒩 is a finite set of p/t nets, called object nets, with disjoint set of nodes.

3. 𝑑 : ̂︀ 𝑃 → 𝒩 is the typing of the system net places. 4. Θ is the set of events. 5. 𝜇 0 ∈ ℳ is the initial marking.

More details -e.g. the firing rule 𝜇 𝜃 − − → OS 𝜇 ′ -are given in the appendix. For a in-depth presentation of Eos cf. [15]. Most problems for safe Eos (in which place markings [𝑀 𝑘 ] are sets) are PSpace-complete [24,25,15]. 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.

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. The complexity for safe, elementary Hornets is beyond PSpace: We have shown that "the reachability problem requires exponential space" for safe, elementary Hornets [26]. In [27] we give an algorithm that needs at most exponential space, which shows that lower and upper bound coincide.

We have a very simple idea: The most natural unit of computation in a Eos is easy to identifyit is a net-token. We assume that each computational unit may fail during the execution. This idea also applies to other models having an explicit notion of computational context, like the Ambient Calculus [8] or the 𝜋-calculus [9]. For other formalism the borderlines of computational contexts are not that obvious and usually have to be identified with the modeller's help.

Assume a given Eos OS = ( ̂︀ 𝑁 , 𝒩 , 𝑑, Θ, 𝜇 0 ). Its reachability graph RG(OS ) defines the behaviour in the absence of failures, i.e. the reachability graph is the state space for 𝑘 = 0 break-downs.

In the following we assume break-downs. We tag markings 𝜇 with the number 𝑘 of breakdowns and denote this as the pair ⟨𝜇, 𝑘⟩.

For technical convenience, we assume that transitions in object nets have a non-empty preset, so, the empty marking disables object-autonomous events and synchronisations. As a consequence, a break-down is like an enforced deadlock in the net-token. 2We have additional break-down edges that connect the level 𝑘 with 𝑘 + 1; a break down edge models the fact that we have one more break-down in the system. A break-down picks some net-token ̂︀ 𝑝[𝑀 ] and disables it by setting the net-token's marking to 0:

For technical convenience we define 𝐵𝐷 0 := ∅. We define 𝑉 𝑘 as the nodes of level 𝑘. For 𝑘 = 0 we have the reachable markings. For 𝑘 > 0 we have all markings reachable from a marking after the last break-down:

70-87

We define the edges of level 𝑘 as:

Each sub-graph (𝑉 𝑖 , 𝐸 𝑖 ) contains all the node of the same level 𝑖 and these sub-graphs are disjoint, since there are no edges from a higher level to a lower level, i.e. the level is increased monotonously.

)︁ is called the failure extension of OS up to level 𝑘 or the 𝑘-failure extension.

The graph RG * (OS ) := (𝑉 * , 𝐸 * ) where

Note, that RG(OS ) is isomorphic to RG 0 (OS ) as we only have to remove the tag 0 from the nodes.

Due to the explicit notion of levels in the marking ⟨𝜇, 𝑘⟩ the structure of RG 𝑘 (OS ) is a chain of sub-graphs (𝑉 𝑖 , 𝐸 𝑖 ); these sub-graphs are linked by the breakdown edges 𝐵𝐷 𝑖 . Schematically:

Proof The central observation is that we must have a break-down connection between the two sub-graph (𝑉 𝑖 , 𝐸 𝑖 ) and (𝑉 𝑖+1 , 𝐸 𝑖+1 ). In this case, we modify the marking 𝜇 = ̂︀ 𝑝[𝑀 𝑖 ] + 𝜇 ′′ into 𝜇 ′ = ̂︀ 𝑝[0] + 𝜇 ′′ , i.e. by a break-down of the net-token ̂︀ 𝑝[𝑀 ]. We use the following partial-order 𝛼 ⪯ 𝛽 on nested multi-sets:

As we have shown in [15,Lemma 5.1] that he firing rule is monotonous w.r.t. the order ⪯. Obviously, we have 𝜇 ∈ 𝑉 𝑘 , 𝜇 ′ ∈ 𝑉 𝑘+1 and 𝜇 ′ ⪯ 𝜇 for the markings given above. Whenever 𝜇 ′ enables a sequence in (𝑉 𝑖+1 , 𝐸 𝑖+1 ) then 𝜇 enables this sequence in (𝑉 𝑖+1 , 𝐸 𝑖+1 ), too. Since we have obtained (𝑉 𝑖+1 , 𝐸 𝑖+1 ) from (𝑉 𝑖 , 𝐸 𝑖 ) by setting some net-token's marking to 0, the sequence is enabled in (𝑉 𝑖 , 𝐸 𝑖 ), too.

qed.

We can also describe the behaviour in the limit, i.e. for 𝑘 → ∞: For each increase of the level we have one more break-down. So, if we consider the sub-graph (𝐸 𝑘 , 𝑉 𝑘 ) for very large 𝑘, we usually have that all net-tokens are down. In this case the net-tokens do not enable object-autonomous events any more and also no synchronous events are possible; only systemautonomous events are possible. Thus, in the limit the Eos behaves like the system net ̂︀ 𝑁 when considered as a p/t net. Technically we obtain this behaviour by the projection Π 1 , which maps a marking 𝜇 to the multiset of system net places.

The semantic definition of robustness uses our definition of the reachability graph extended with break-downs. We introduce a hierarchy for satisfiability by restricting the numbers of break-down events: The usual satisfiability of a property 𝜑 considers the normal reachability graph RG 0 (OS ); whenever we extend the reachability graph towards RG 1 (OS ) we check whether the property can withstand a break-down of at most one net-token. We can generalise this idea to an arbitrary number 𝑘 of break-down events. In general, a property 𝜑 that is satisfied 𝑘-robustly will not be satisfied 𝑘 + 1-robustly. Especially, a property 𝜑 that is satisfied by an Eos (0-robustly) is not satisfied 1-robustly, i.e., in general even one break-down destroys the property 𝜑. Liveness of the Eos is a typical example. In other words: robustness does not come for free. Usually the Eos model has to take care to satisfy a property 𝑘-robustly, e.g., by having model parts that will restart crashed net-tokens in a well-defined state.

An example for a property 𝜑 that is satisfied even *-robustly is safeness [24], i.e., the property that there is at most one net-token on each place in the system net. This is due to the fact that a break-down modifies the marking 𝜇 in a way that does not change the projection Π 1 (𝜇) to the system net and, consequently, does not enable any 'unseen' transition of the system net.

In our context of organisational multi-agent systems the notion of robustness allows us to specify two central classes of properties:

• Flexibility/Adaptivity: The MAS has the possibility to react to changes in the environment (here: break-downs of other agents) to re-establish a desired property 𝜑 is expressed as OS , 𝜇 0 |= * AGEF𝜑 -the usual liveness property in CTL [28].

• Resilience: The system always stays in a 'safe' region of the state space -even in the presence of break-downs of other agents -is expressed as OS , 𝜇 0 |= * AG𝜑 -a classical invariant property (aka as a safety property).

A structural property for the system net is derived from the net topology only. The classical example are net-invariants. A structural invariant holds for any initial marking and not only a given one (cf. [29] for the discussion between invariants and structural invariants). Fact 2. A structural property is independent from the net-tokens' markings and therefore *robust.

Another interesting question is whether we can tolerate break-downs using redundancy, i.e., multiple copies of the net-tokens. This question is closely related to the Petri net concept of monotonicity. A property is monotonous if it holds also for any greater initial marking. It is well known that reachability is monotonous, while deadlock-freedom or liveness are -in general -not (However, for the structural sub-class of free-choice nets liveness is monotonous).

For monotonous properties redundancy is useful, i.e. we can add additional net-tokens to survive knock-outs of net-tokens. Here we simply multiply the initial marking and consider 𝜇 0 + 𝑘 • 𝜇 0 . Proposition 2. Let 𝜑 be a monotonous property. When 𝜑 holds in the initial marking 𝜇 0 , then 𝜑 is 𝑘-robust in the initial marking 𝜇 0 + 𝑘 • 𝜇 0 :

We can execute at most 𝑘 break-downs. So any marking 𝜇 reachable from (𝜇 0 + 𝑘 • 𝜇 0 ) is still greater than some marking reachable from 𝜇 0 only. Since the property holds in 𝜇 0 and is monotonous it holds in RG 𝑘 (OS ).

qed.

Our characterisation of robustness has the drawback that it is based on an extension of the usual Petri net semantics as we extend the reachability graph. In the following, we like to show that we can express this extension on a purely syntactical level, i.e., we modify the EosOS into another Eos OS * with the property that the 'normal' reachability graph of OS * is isomorphic to the break-down extension RG * (OS ). In this case, we can reduce the specialised analysis of OS to an 'normal' analysis of OS * using existing standard tools. The main idea is quite simple (cf. Fig. 2): We apply the following construction to the Eos OS .

• We add a run-place to each object net and this run-place is attached as a side condition to each transition 𝑡. • The run-place is initially marked with one token.

• We add a new transition 𝑡 𝑘𝑖𝑙𝑙 to each object net that synchronises with the environment (via the channel ⟨off⟩) and removes the token of the run-place. • In the system net we add for each place ̂︀ 𝑝 a new side transition ̂︀ 𝑡 ̂︀ 𝑝,𝑘𝑖𝑙𝑙 which synchronises with 𝑡 𝑘𝑖𝑙𝑙 .

The effect of the synchronous kill-event is that the net-token is dead afterwards (but usually contains useless tokens on the places other than the run-place). We like to establish that an empty run-place always indicates that the net-token has broken down. In this case we could drop the explicit tag 𝑘 from the state because it is implicitly given by the number of net-tokens with an empty run-place. However, this is not true, since the Eos firing rule 'collects' the net-tokens markings from all incoming arcs and 'distributes' this sum over all net-tokens generated on the outgoing arcs. For a system net transition that has, e.g., one incoming arc and two outgoing arcs, one of the generated net-tokens must have an empty run-place. However, the net-token should not be regarded as a break-down. We can 'repair' this problem in the following way: We replace each system net transition ̂︀ 𝑡 by a simple subnet (cf. Fig. 3) that removes the tokens from the 𝑚 incoming places ̂︀ 𝑝 𝑖 (using the synchronisation channel ⟨off⟩ 𝑚 times) and individually re-creates one token on each run-place in each net-token on the 𝑛 outgoing places ̂︀ 𝑝 ′ 𝑖 (using the synchronisation channel ⟨on⟩ at the internal transitions ̂︀ 𝑡 𝑖 ). We replace each system net transition with such a subnet. 3 The resulting Eos is denoted as OS * .

Due to this construction, an empty run-place in a net-token (except for those net-tokens in the intermediate place ̂︀ 𝑝 ′′ 𝑖 of the subnet) is equivalent to a break-down. When we consider the 𝑛 intermediate transitions ̂︀ 𝑡 𝑖 as 'silent' events, then the constructed net OS * is bisimilar to the original state space OS . Proposition 3. The extended Eos OS * is the syntactical representation of the *-failure extension of OS , i.e. both state spaces are bisimilar: RG * (OS ) ≈ RG(OS * ) With a small modification of the extended Eos OS * we can also describe the 𝑘-failure extension of OS :

• We add a global pool-place to the system net that contains exactly 𝑘 black tokens.

• Each kill-transition removes one token from the global pool-place.

We denote this modification of the Eos as OS 𝑘 .

Note that after 𝑘 kill-events the pool place is empty and further kill-events are disabled. The behaviour of OS 𝑘 is similar to the extension OS * except that we restrict the number of break-downs to 𝑘. Proposition 4. The extended Eos OS 𝑘 is the syntactical representation of the 𝑘-failure extension of OS , i.e. both state spaces are bisimilar: RG 𝑘 (OS ) ≈ RG(OS 𝑘 )

In the absence of break-downs, i.e., for 𝑘 = 0, the normal semantics coincides with the extended semantics and the given Eos coincides with its extension: Fact 3. For 𝑘 = 0 we obtain that all systems coincide: RG(OS ) ≃ RG 0 (OS ) ≈ RG(OS 0 ).

With these constructions we have reduced checking properties w.r.t. robustness to a usual state space based query.

In this paper, we have shown that Nets-within-Nets have an intuitive representation of the concept of a 'computational unit': the net-tokens. Based on this, we could define a break-down of net-tokens and define the satisfiability of properties in the context of break-downs.

Our concept of robustness relies on an extension of the state space. We provided a reduction of this semantical definition (which extends the Petri net semantics) to a syntactical one (where we use the usual semantics): We transformed the Eos OS into the Eos OS * such that the 'normal' reachability graph of OS * is bisimilar to the break-down extension RG * (OS ). Therefore, we could still use existing tools to investigate robustness.

We plan to extend the simple -though popularlet it crash-based model, e.g., by allowing the computational units (net-tokens) to gracefully degrade.

In future work, we will apply this notion of robustness to our multi-agent system Sonar [11], especially with a focus on the analysis of adaptivity as we have started with our previous work on the analysis of adaption processes [30] and adapting agent architectures [31]. In [30] we used the set of different types of net-tokens that occur in the current marking to define the system's gene-pool. Our current research hypothesis is that a more diverse gene-pool in adapting agent architectures [31] leads to more robust systems in general.

The definition of Petri nets relies on the notion of multisets. A multiset m on the set 𝐷 is a mapping m : 𝐷 → N. Multisets are generalisations of sets in the sense that every subset of 𝐷 corresponds to a multiset m with m(𝑑) ≤ 1 for all 𝑑 ∈ 𝐷. The empty multiset 0 is defined as 0(𝑑) = 0 for all 𝑑 ∈ 𝐷. Multiset addition for m 1 , m 2 : 𝐷 → N is defined component-wise:

𝑑), 0). We use common notations for the cardinality of a multiset |m| := ∑︀ 𝑑∈𝐷 m(𝑑) and multiset ordering m 1 ≤ m 2 , where the partial order ≤ is defined by

The set of all finite multisets over the set 𝐷 is denoted MS (𝐷). The set MS (𝐷) naturally forms a monoid with multiset addition + and the empty multiset 0. Multisets can be identified with the commutative monoid structure (MS (𝐷), +, 0). Multisets are the free commutative monoid over 𝐷 since every multiset has the unique representation in the form m = ∑︀ 𝑑∈𝐷 m(𝑑) • 𝑑, where m(𝑑) denotes the multiplicity of 𝑑. Multisets can also be represented as a formal sum in the form m = ∑︀ 𝑛 𝑖=1 𝑥 𝑖 , where 𝑥 𝑖 ∈ 𝐷. Any mapping 𝑓 : 𝐷 → 𝐷 ′ is extended to a multiset homomorphism 𝑓 ♯ : MS (𝐷) → MS (𝐷 ′ ):

. This includes the special case 𝑓 ♯ (0) = 0. We simply write 𝑓 to denote the mapping 𝑓 ♯ . The notation is in accordance with the set-theoretic notation

An elementary object system (Eos) is composed of a system net, which is a p/t net ̂︀ 𝑁 = ( ̂︀ 𝑃 , ̂︀ 𝑇 , pre, post) and a set of object nets 𝒩 = {𝑁 1 , . . . , 𝑁 𝑛 }, which are p/t nets given as 𝑁 = (𝑃 𝑁 , 𝑇 𝑁 , pre 𝑁 , post 𝑁 ), where 𝑁 ∈ 𝒩 . In extension we assume that all sets of nodes (places and transitions) are pairwise disjoint. Moreover we assume ̂︀ 𝑁 ̸ ∈ 𝒩 and the existence of the object net • ∈ 𝒩 , which has no places and no transitions and is used to model anonymous, so called black tokens.

The system net places are typed by the mapping 𝑑 : ̂︀ 𝑃 → 𝒩 with the meaning, that a place ̂︀ 𝑝 ∈ ̂︀ 𝑃 of the system net with 𝑑(̂︀ 𝑝) = 𝑁 may contain only net-tokens of the object net type 𝑁 . 4 No place of the system net is mapped to the system net itself since ̂︀ 𝑁 ̸ ∈ 𝒩 . A typing is called conservative iff for each place ̂︀ 𝑝 in the preset of a system net transition ̂︀ 𝑡 such that 𝑑(̂︀ 𝑝) ̸ = • there is place in the postset being of the same type:

An Eos is p/t-like iff it has only places for black tokens:

Nested Markings Since the tokens of an Eos are instances of object nets, a marking of an Eos is a nested multiset. A marking of an Eos OS is denoted 𝜇 = ∑︀ |𝜇| 𝑘=1 (̂︀ 𝑝 𝑘 , 𝑀 𝑘 ), where ̂︀ 𝑝 𝑘 is a place of the system net and 𝑀 𝑘 is the marking of a net-token with type 𝑑(̂︀ 𝑝 𝑘 ). To emphasise the nesting, markings are also denoted as

The set of all markings which are syntactically consistent with the typing 𝑑 is denoted ℳ, where 𝑑 −1 (𝑁 ) ⊆ ̂︀ 𝑃 is the set of system net places of the type 𝑁 :

We define the partial order ⊑ on nested multisets by setting 𝜇 1 ⊑ 𝜇 2 iff ∃𝜇 :

A more liberal variant is the order ⪯ defined by:

For 𝛼 ⪯ 𝛽 the injection 𝑓 generates a sub-marking of 𝛽 which is denoted

Events Analogously to markings, which are nested multisets 𝜇, the events of an Eos are also nested. An Eos allows three different kinds of events -as illustrated by the following Eos:

1. System-autonomous: The system net transition 𝑡 fires autonomously which moves the net-token from 𝑝 1 to 𝑝 2 without changing its marking. 2. Object-autonomous: The object net fires transition 𝑡 1 , which "moves" the black token from 𝑞 1 to 𝑞 2 . The object net itself remains at its location 𝑝 1 . 3. Synchronisation: The system net transition 𝑡 fires synchronously with 𝑡 1 in the object net. Whenever synchronisation is demanded, autonomous actions are forbidden.

The set of events is denoted Θ. Events are formalised as a pair ̂︀ 𝜏 [𝜗], where ̂︀ 𝜏 is either the transition that fires in the system net or a special "idle" transition id ̂︀ 𝑝 (cf. below); and 𝜗 is a function such that 𝜗(𝑁 ) is the multiset of transitions, which have to fire synchronously with ̂︀ 𝜏 , (i.e. for each object net 𝑁 ∈ 𝒩 we have 𝜗(𝑁 ) ∈ MS (𝑇 𝑁 )). 5 In general ̂︀ 𝜏 [𝜗] describes a synchronisation, but autonomous events are special subcases: Obviously, a system-autonomous events is the special case, where 𝜗 = 0 with 0(𝑁 ) = 0 for all object nets 𝑁 . To describe an object-autonomous event we assume the set of idle transitions {id 1. ̂︀ 𝑁 is a p/t net, called the system net.

2. 𝒩 is a finite set of disjoint p/t nets, called object nets.

3. 𝑑 : ̂︀ 𝑃 → 𝒩 is the typing of the system net places.

4. Θ is the set of events. 5. 𝜇 0 ∈ ℳ is the initial marking.

Example Figure 4 shows an Eos with the system net ̂︀ 𝑁 and the object nets 𝒩 = {𝑁 1 , 𝑁 2 }. The system has four net-tokens: two on place ̂︀ 𝑝 1 and one on ̂︀ 𝑝 2 and ̂︀ 𝑝 3 each. The net-tokens on ︀ 𝑝 1 and ̂︀ 𝑝 2 share the same net structure, but have independent markings. 5 In the graphical representation the events are generated by transition inscriptions. For each object net 𝑁 ∈ 𝒩 a system net transition ̂︀ 𝑡 is labelled with a multiset of channels ̂︀ 𝑙( ̂︀ 𝑡)(𝑁 ) = ch1 + • • • + ch𝑛, depicted as ⟨𝑁 :ch1, 𝑁 :ch2, . . .⟩. Similarily, an object net transition 𝑡 may be labelled with a channel 𝑙𝑁 (𝑡) = ch -depicted as ⟨:ch⟩ whenver there is such a label. We obtain an event ̂︀

The labelling generates one event:

The initial marking has two net-tokens on ̂︀ 𝑝 1 , one on ̂︀ 𝑝 2 , and one on ̂︀ 𝑝 3 :

Note that for Figure 4 the structure is the same for the three net-tokens on ̂︀ 𝑝 1 and ̂︀ 𝑝 2 but the net-token markings are different.

The projection Π 1 on the first component abstracts from the substructure of all net-tokens for a marking of an Eos:

The projection Π 2 𝑁 on the second component is the sum of all net-token markings 𝑀 𝑘 of the type 𝑁 ∈ 𝒩 , ignoring their local distribution within the system net:

where the indicator function

𝜇) results in a marking of the object net 𝑁 .

A system event ̂︀ 𝜏 [𝜗] removes net-tokens together with their individual internal markings. Firing the event replaces a nested multiset 𝜆 ∈ ℳ that is part of the current marking 𝜇, i.e. 𝜆 ⊑ 𝜇, by the nested multiset 𝜌. Therefore the successor marking is 𝜇 ′ := (𝜇 − 𝜆) + 𝜌. The enabling condition is expressed by the enabling predicate 𝜑 OS (or just 𝜑 whenever OS is clear from the context):

With ̂︁ 𝑀 = Π 1 (𝜆) and ̂︁ 𝑀 ′ = Π 1 (𝜌) as well as 𝑀 𝑁 = Π 2 𝑁 (𝜆) and 𝑀 ′ 𝑁 = Π 2 𝑁 (𝜌) for all 𝑁 ∈ 𝒩 the predicate 𝜑 has the following meaning:

1. The first conjunct expresses that the system net multiset ̂︁ 𝑀 corresponds to the precondition of the system net transition ̂︀ 𝜏 , i.e. ̂︁ 𝑀 = pre(̂︀ 𝜏 ).

2. In turn, a multiset ̂︁ 𝑀 ′ is produced, that corresponds to the post-set of ̂︀ 𝜏 .

3. A multi-set 𝜗(𝑁 ) of object net transitions is enabled if the sum 𝑀 𝑁 of the net-token markings (of type 𝑁 ) enable it, i.e. 𝑀 𝑁 ≥ pre 𝑁 (𝜗(𝑁 )).

𝜏 [𝜗] must also obey the object marking distribution condition: 𝑀 ′ 𝑁 = 𝑀 𝑁 − pre 𝑁 (𝜗(𝑁 )) + post 𝑁 (𝜗(𝑁 )), where post 𝑁 (𝜗(𝑁 )) − pre 𝑁 (𝜗(𝑁 )) is the effect of the object net's transitions on the net-tokens.

Note that conditions 1. and 2. assure 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 ̂︀ 𝑡[0] the enabling predicate 𝜑 can be simplified further. We have pre 𝑁 (0(𝑁 )) = post 𝑁 (0(𝑁 )) = 0. This ensures Π 2 𝑁 (𝜆) = Π 2 𝑁 (𝜌), i.e. the sum of markings in the copies of a net-token is preserved w.r.t. each type 𝑁 . This condition ensures the existence of linear invariance properties Analogously, for an object-autonomous event we have an idle-transition ̂︀ 𝜏 = id ̂︀ 𝑝 for the system net and the first and the second conjunct is: Π 1 (𝜆) = pre(id Note that the firing rule makes no a-priori assumptions about how to distribute the object net markings onto the generated net-tokens. Therefore we need the mode (𝜆, 𝜌) to formulate the firing of ̂︀ 𝜏 [𝜗] in a functional way.

Example Consider the Eos of Figure 4 The net-token markings are added by the projections Π 2 𝑁 resulting in the markings Π 2 𝑁 (𝜆). The sub-synchronisation generates Π 2 𝑁 (𝜌). (The results are shown above and below the transition ̂︀ 𝑡.) After the synchronisation we obtain the successor marking 𝜇 ′ with net-tokens on ̂︀ 𝑝 4 , ︀ 𝑝 5 , and ̂︀ 𝑝 6 as shown in Figure 5:

Note, that we have only presented one mode (𝜆, 𝜌) and that other modes are possible, too.

In the following we relate those nested multisets, that coincide in their projections. The projection of a marking 𝜇 is defined as follows:

Π(𝜇) := (Π 1 (𝜇), (Π 2 𝑁 (𝜇)) 𝑁 ∈𝒩 )

Obviously, there are several markings 𝜇 with the same projection, i.e. 𝜇 is not uniquely defined by Π(𝜇). The nested multisets, that coincide in their projections give rise to the equivalence ∼ = ⊆ ℳ 2 , called projection equivalence defined by:

The relation 𝛼 ∼ = 𝛽 abstracts from the location, i.e. the concrete net-token, in which a object net's place 𝑝 is marked as long as it is present in 𝛼 and 𝛽. For example, for 𝑑(̂︀ 𝑝) = 𝑑(̂︀ 𝑝 ′ ) we have

which means that ∼ = allows the tokens 𝑝 1 and 𝑝 3 to change their locations (i.e. between ̂︀ 𝑝 and ︀ 𝑝 ′ ).