Robustness: A natural Definition based on Nets-within-Nets Michael Köhler-Bussmeier1 , Lorenzo Capra2 1 Hamburg University of Applied Sciences, Berliner Tor 7, D-20099 Hamburg 2 Dipartimento di Informatica, Università degli Studi di Milano - Italy Abstract In modern distributed systems robustness is a major requirement. In previous work on availability, the analysis required an additional model part that specifies the assumptions about where in the model there are areas 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. Instead, we like to derive an error model directly from the system model. We will show that for Elementary Object Systems we have a natural candidate to describe such a localised area of failure: the net-tokens. They are clearly localised and can be understood as computational entities (like containers in Kubernetes). Keywords Robustness, nets within nets, nets as tokens, multi-agent systems 1. Defining Robustness for Models of Distributed Architectures 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 PNSE’23, International Workshop on Petri Nets and Software Engineering, 2023 " michael.koehler-bussmeier@haw-hamburg.de (M. Köhler-Bussmeier); capra@di.unimi.it (L. Capra) ~ https://www.haw-hamburg.de/michael-koehler-bussmeier (M. Köhler-Bussmeier)  0000-0002-3074-4145 (M. Köhler-Bussmeier); 0000-0002-1029-1169 (L. Capra) © 2023 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) 70 Michael Köhler-Bussmeier et al. CEUR Workshop Proceedings 70–87 identify these sub-nets as the whole structure does not provide clear hints to identify them.1 Our 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-within- nets 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. 2. Nets-within-Nets, EOS 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 predi- cate/transition nets [17], Reference nets [18], PN2 [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. 1 Sometimes we consider Petri nets that have a compositional structure, like workflows with AND-splits or OR-choices; or we can identify an refinement structure. In these cases we can identify at least sub-structures, which are candidates for these computational units. However, there is no one-to-one correspondence between the sub-structures and the concept of a computational unit. 71 Michael Köhler-Bussmeier et al. CEUR Workshop Proceedings 70–87 Figure 1: An Elementary Object Net System (Eos) 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 𝑡 and the object net transition 𝑡1 , then both must fire synchronously: The net transition ̂︀ 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 𝜇 = 𝑝̂︀1 [𝑞1 ]. ∑︀ 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 𝑁 : (︁⋃︁ (︀ −1 )︀)︁ ℳ := MS 𝑑 (𝑁 ) × MS (𝑃𝑁 ) (1) 𝑁 ∈𝒩 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 object- autonomous events. The set of events is denoted Θ (cf. the appendix for details). Definition 1 (Elementary Object System, EOS). An elementary object system (Eos) is a tu- ple OS = (𝑁̂︀ , 𝒩 , 𝑑, Θ, 𝜇0 ), where: 1. 𝑁 ̂︀ is a p/t net, called the system net. 72 Michael Köhler-Bussmeier et al. CEUR Workshop Proceedings 70–87 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 𝜇 −−→ 𝜇′ – are given in the appendix. For a in-depth OS 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. 3. Defining Robustness for EOS We have a very simple idea: The most natural unit of computation in a Eos is easy to identify – it 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 break- downs 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.2 We 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: 𝐵𝐷𝑘+1 := {(⟨𝜇, 𝑘⟩, ⟨𝜇′ , 𝑘 + 1⟩) | ∃𝜇′′ : 𝜇 = 𝑝[𝑀 ̂︀ ] + 𝜇′′ ∧ 𝑀 ̸= 0 ∧ 𝜇′ = 𝑝[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: * 𝑉0 = {⟨𝜇, 0⟩ | 𝜇0 → − 𝜇} (2) 2 If one wishes to distinguish between a deadlock and a break-down, we have to ensure that net-tokens do not deadlock unless they are unmarked. We can guarantee this by adding a side-transition to each place in the object net. 73 Michael Köhler-Bussmeier et al. CEUR Workshop Proceedings 70–87 * 𝑉𝑘+1 = {⟨𝜇′′ , 𝑘 + 1⟩ | (⟨𝜇, 𝑘⟩, ⟨𝜇′ , 𝑘 + 1⟩) ∈ 𝐵𝐷𝑘+1 ∧ 𝜇′ → − 𝜇′′ } (3) We define the edges of level 𝑘 as: 𝜃 𝐸𝑘 := {(⟨𝜇, 𝑘⟩, ⟨𝜇′ , 𝑘⟩) | 𝜇 → − 𝜇′ } (4) 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. (︁⋃︀ )︁ 𝑘 ⋃︀𝑘 Definition 2. The graph RG 𝑘 (OS ) = 𝑉 𝑖=0 𝑖 , 𝑖=0 (𝐸𝑖 ∪ 𝐵𝐷 𝑖 ) is called the failure exten- sion of OS up to level 𝑘 or the 𝑘-failure extension. ⋃︀ The graph RG * (OS ) := (𝑉 * , 𝐸 * ) where 𝑉 * := 𝑖≥0 𝑉𝑖 and 𝐸 * = 𝑖≥0 (𝐸𝑖 ∪ 𝐵𝐷𝑖 ) is called ⋃︀ the *-failure extension. 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: 𝐵𝐷 1 𝐵𝐷2 𝐵𝐷𝑘 (𝑉0 , 𝐸0 ) −−−→ (𝑉1 , 𝐸1 ) −−−→ · · · −−−→ (𝑉𝑘 , 𝐸𝑘 ) Proposition 1. Whenever a firing sequence that is enabled within the sub-graph (𝑉𝑖+1 , 𝐸𝑖+1 ) it is enabled within (𝑉𝑖 , 𝐸𝑖 ), too. 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: ∑︀𝑚 𝑎𝑖 [𝐴𝑖 ] ⪯ 𝑛𝑗=1 ̂︀𝑏𝑗 [𝐵𝑗 ] ⇐⇒ ∃ injection 𝑓 : {1, ..., 𝑚} → {1, ..., 𝑛} : ∑︀ 𝑖=1 ̂︀ ∀1 ≤ 𝑖 ≤ 𝑚 : ̂︀ 𝑎𝑖 = ̂︀𝑏𝑓 (𝑖) ∧ 𝐴𝑖 ≤ 𝐵𝑓 (𝑖) 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 system- autonomous 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. 74 Michael Köhler-Bussmeier et al. CEUR Workshop Proceedings 70–87 3.1. The semantic definition of robustness 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. Definition 3 (Robustness). A property 𝜑 is satisfied 𝑘-robustly by the Eos OS iff 𝜑 holds in RG 𝑘 (OS ). This is denoted by OS , 𝜇0 |=𝑘 𝜑, or short: 𝜇0 |=𝑘 𝜑 wheneverOS is clear from the context. A property 𝜑 is satisfied *-robustly by the Eos OS iff 𝜑 holds in RG * (OS ). This is denoted by 𝜇0 |=* 𝜑. Fact 1. Note, that a property 𝜑 holds for an Eos OS iff 𝜑 is 0-robust, since RG(OS ) ≃ RG 0 . 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 75 Michael Köhler-Bussmeier et al. CEUR Workshop Proceedings 70–87 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 : 𝜇0 |= 𝜑 =⇒ (𝜇0 + 𝑘 · 𝜇0 ) |=𝑘 𝜑 Proof (Sketch) 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. 4. The Syntactical Characterisation of Robustness 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. Figure 2: Construction of the Eos OS * . 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 𝑡𝑘𝑖𝑙𝑙 . 76 Michael Köhler-Bussmeier et al. CEUR Workshop Proceedings 70–87 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. Figure 3: Construction for Run-Places in the Eos OS * . 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 𝑡𝑖 ). We replace each system net transition with such a subnet.3 The resulting internal transitions ̂︀ 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 𝑘. 3 We could skip this construction for system net transitions which have exactly one place in the preset and one in the postset. 77 Michael Köhler-Bussmeier et al. CEUR Workshop Proceedings 70–87 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. 5. Conclusion 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 popular – let 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. 78 Michael Köhler-Bussmeier et al. CEUR Workshop Proceedings 70–87 References [1] M. Baldoni, C. Baroglio, R. Micalizio, Fragility and robustness in multiagent systems, in: C. Baroglio, J. Hubner, M. Winikoff (Eds.), Engineering Multi-Agent Systems. EMAS 2020, volume 12589 of Lecture Notes in Computer Science, Springer-Verlag, 2020. [2] M. Müller, M. Köhler-Bußmeier, Availability analysis of the ONOS architecture, in: E. Kindler, M. Köhler-Bußmeier, H. Rölke (Eds.), International Workshop on Petri Nets and Software Engineering 2021, volume 2907 of CEUR Workshop Proceedings, Aachen, 2021, pp. 41–64. URL: http://ceur-ws.org/Vol-2907/. [3] L. Capra, M. Köhler-Bußmeier, A Maude formalization of object nets, in: S. Bonfanti, T. Kobayashi, D. Perez-Palacin (Eds.), 6th International Workshop on Formal Approaches for Advanced Computing Systems, FAACS’22, 2022. [4] L. Capra., M. Köhler-Bußmeier., Modelling adaptive systems with nets-within-nets in maude, in: Proceedings of the 18th International Conference on Evaluation of Novel Approaches to Software Engineering - ENASE„ INSTICC, SciTePress, 2023, pp. 487–496. doi:10.5220/0011860000003464. [5] L. Lamport, R. Shostak, M. Pease, The byzantine generals problem, ACM Transactions on Programming Languages and Systems (1982) 382–401. [6] W. Reisig, Petri Nets: An Introduction, Springer-Verlag, Heidelberg, 1985. [7] R. Valk, Object Petri nets: Using the nets-within-nets paradigm, in: J. Desel, W. Reisig, G. Rozenberg (Eds.), Advanced Course on Petri Nets 2003, volume 3098 of Lecture Notes in Computer Science, Springer-Verlag, 2003, pp. 819–848. [8] L. Cardelli, A. D. Gordon, G. Ghelli, Mobility types for mobile ambients, in: Proceedings of the Conference on Automata, Languages, and Programming (ICALP’99), volume 1644 of Lecture Notes in Computer Science, Springer-Verlag, 1999, pp. 230–239. [9] R. Milner, J. Parrow, D. Walker, A calculus of mobile processes, parts 1-2, Information and computation 100 (1992) 1–77. [10] V. Dignum, J. Padget, Multiagent organizations, in: G. Weiss (Ed.), Multiagent Systems, 2nd ed., Intelligent Robotics; Autonomous Agents Series, MIT Press, 2013, pp. 51–98. [11] M. Köhler-Bußmeier, M. Wester-Ebbinghaus, D. Moldt, A formal model for organisational structures behind process-aware information systems, Transactions on Petri Nets and Other Models of Concurrency. Special Issue on Concurrency in Process-Aware Information Systems 5460 (2009) 98–114. [12] M. A. Marsan, G. Balbo, G. Conte, S. Donatelli, G. Franceschinis, Modelling with Gener- alized Stochastic Petri Nets, Wiley Series in Parallel Computing, John Wiley and Sons, 1995. [13] M. Köhler, H. Rölke, Properties of Object Petri Nets, in: J. Cortadella, W. Reisig (Eds.), International Conference on Application and Theory of Petri Nets 2004, volume 3099 of Lecture Notes in Computer Science, Springer-Verlag, 2004, pp. 278–297. [14] M. Köhler-Bußmeier, F. Heitmann, On the expressiveness of communication channels for object nets, Fundamenta Informaticae 93 (2009) 205–219. [15] M. Köhler-Bußmeier, A survey on decidability results for elementary object systems, Fundamenta Informaticae 130 (2014) 99–123. [16] I. A. Lomazova, Nested Petri nets – a formalism for specification of multi-agent distributed 79 Michael Köhler-Bussmeier et al. CEUR Workshop Proceedings 70–87 systems, Fundamenta Informaticae 43 (2000) 195–214. [17] D. Xu, Y. Deng, Modeling mobile agent systems with high level Petri nets, in: IEEE International Conference on Systems, Man, and Cybernetics’2000, 2000. [18] O. Kummer, Referenznetze, Logos Verlag, 2002. [19] K. Hiraishi, PN2 : An elementary model for design and analysis of multi-agent systems, in: F. Arbab, C. L. Talcott (Eds.), Coordination Models and Languages, COORDINATION 2002, volume 2315 of Lecture Notes in Computer Science, Springer-Verlag, 2002, pp. 220–235. [20] M. A. Bednarczyk, L. Bernardinello, W. Pawlowski, L. Pomello, Modelling mobility with Petri hypernets, in: J. L. Fiadeiro, P. D. Mosses, F. Orejas (Eds.), Recent Trends in Algebraic Development Techniques (WADT 2004), volume 3423 of Lecture Notes in Computer Science, Springer-Verlag, 2004, pp. 28–44. [21] I. A. Lomazova, K. M. van Hee, O. Oanea, A. Serebrenik, N. Sidorova, M. Voorhoeve, Nested nets for adaptive systems, in: Application and Theory of Petri Nets and Other Models of Concurrency, Lecture Notes in Computer Science, Springer-Verlag, 2006, pp. 241–260. [22] L. Capra, A maude implementation of rewritable petri nets: a feasible model for dynamically reconfigurable systems, in: M. Gleirscher, J. v. d. Pol, J. Woodcock (Eds.), First Workshop on Applicable Formal Methods 2021, 2021. [23] J. Padberg, L. Kahloul, Overview of reconfigurable petri nets, in: R. Heckel, G. Taentzer (Eds.), Graph Transformation, Specifications, and Nets, volume 10800, Springer-Verlag, 2018, pp. 201–222. [24] M. Köhler-Bußmeier, F. Heitmann, Safeness for object nets, Fundamenta Informaticae 101 (2010) 29–43. [25] M. Köhler-Bußmeier, F. Heitmann, Liveness of safe object nets, Fundamenta Informaticae 112 (2011) 73–87. [26] M. Köhler-Bußmeier, On the complexity of the reachability problem for safe, elementary Hornets, Fundamenta Informaticae 129 (2014) 101–116. Dedicated to the Memory of Professor Manfred Kudlek. [27] M. Köhler-Bußmeier, F. Heitmann, An upper bound for the reachability problem of safe, elementary hornets, Fundamenta Informaticae 143 (2016) 89–100. [28] A. Emerson, Temporal and modal logic, volume B, MIT press, 1990. [29] E. Kindler, Invariants, composition, and substitution, Acta Informatica 32 (1995) 299–312. [30] M. Köhler-Bußmeier, H. Rölke, Analysing adaption processes of Hornets, in: M. Köhler- Bußmeier, D. Moldt, H. Rölke (Eds.), Petri Nets and Software Engineering 2022, PNSE’22, volume 3170, CEUR, 2022, pp. 80–98. [31] M. Köhler-Bußmeier, J. Sudeikat, Balance vs. contingency: Adaption measures for organiza- tional multi-agent systems, in: K. Jander, L. Braubach, C. Badica (Eds.), 15th International Symposium on Intelligent Distributed Computing (IDC’22), volume 1089 of Studies in Computational Intelligence, Springer-Verlag, 2023. 80 Michael Köhler-Bussmeier et al. CEUR Workshop Proceedings 70–87 A. Petri Nets 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 m1 , m2 : 𝐷 → N is defined component-wise: (m1 + m2 )(𝑑) := m1 (𝑑) + m2 (𝑑). Multiset-difference m1 − m2 is defined by (m1 − m2 )(𝑑) :=∑︀ max(m1 (𝑑) − m2 (𝑑), 0). We use common notations for the cardinality of a multiset |m| := 𝑑∈𝐷 m(𝑑) and multiset ordering m1 ≤ m2 , where the partial order ≤ is defined by m1 ≤ m2 ⇐⇒ ∀𝑑 ∈ 𝐷 : m1 (𝑑) ≤ m2 (𝑑). A multiset m is finite if |m| < ∞. 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 repre- sentation 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 𝑥𝑖 ∈ 𝐷. ′ 𝑓 ♯ : MS (𝐷) → MS (𝐷′ ): ♯ ∑︀𝑛mapping 𝑓∑︀: 𝑛𝐷 → 𝐷 is extended to a multiset homomorphism Any ♯ 𝑓 ( 𝑖=1 𝑥𝑖 ) = 𝑖=1 𝑓 (𝑥𝑖 ). This includes the special case 𝑓 (0) = 0. We simply write 𝑓 to denote the mapping 𝑓 ♯ . The notation is in accordance with the set-theoretic notation 𝑓 (𝐴) = {𝑓 (𝑎) | 𝑎 ∈ 𝐴}. Definition 4. A p/t net 𝑁 is a tuple 𝑁 = (𝑃, 𝑇, pre, post), such that 𝑃 is a set of places, 𝑇 is a set of transitions, with 𝑃 ∩ 𝑇 = ∅, and pre, post : 𝑇 → MS (𝑃 ) are the pre- and post-condition functions. A marking of 𝑁 is a multiset of places: m ∈ MS (𝑃 ). A p/t net with initial marking m0 is denoted 𝑁 = (𝑃, 𝑇, pre, post, m0 ). We use the usual notations for nets like ∙ 𝑥 for the set of predecessors and 𝑥∙ for the set of successors for a node 𝑥 ∈ (𝑃 ∪ 𝑇 ). For 𝑡 ∈ 𝑇 we have ∙ 𝑡 = {𝑝 ∈ 𝑃 | pre(𝑡)(𝑝) > 0} and 𝑡∙ = {𝑝 ∈ 𝑃 | post(𝑡)(𝑝) > 0}. For 𝑝 ∈ 𝑃 we have ∙ 𝑝 = {𝑡 ∈ 𝑇 | post(𝑡)(𝑝) > 0} and 𝑝∙ = {𝑡 ∈ 𝑇 | pre(𝑡)(𝑝) > 0}. A transition 𝑡 ∈ 𝑇 of a p/t net 𝑁 is enabled in marking m iff ∀𝑝 ∈ 𝑃 : m(𝑝) ≥ pre(𝑡)(𝑝) holds. The successor marking when firing 𝑡 is m′ (𝑝) = m(𝑝) − pre(𝑡)(𝑝) + post(𝑡)(𝑝) for all 𝑝 ∈ 𝑃 . Using multiset notation enabling is expressed by m ≥ pre(𝑡) and the successor 𝑡 marking is m′ = m − pre(𝑡) + post(𝑡). We denote the enabling of 𝑡 in marking m by m −→. 𝑁 𝑡 ′ Firing of 𝑡 is denoted by m −→ m . The net 𝑁 is omitted if it is clear from the context. 𝑁 𝜖 𝑤 Firing is extended to sequences 𝑤 ∈ 𝑇 * in the obvious way: (i) m → − m; (ii) If m −→ m′ 𝑡 𝑤𝑡 * and m′ → − m′′ hold, then we have m −→ m′′ . We write m →− m′ whenever there is some * 𝑤 ′ 𝑤 ∈ 𝑇 such that m − → m holds. The set of reachable markings is RS (m0 ) := {m | ∃𝑤 ∈ 𝑤 𝑇 * : m0 −→ m}. 81 Michael Köhler-Bussmeier et al. CEUR Workshop Proceedings 70–87 B. Elementary Object Systems 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. Typing 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 𝑁 . No place of the system net is mapped to the system net itself since 𝑁 4 ̂︀ ̸∈ 𝒩 . A typing is called conservative iff for each place 𝑝̂︀ in the preset of a system net transition ̂︀ 𝑡 such 𝑝) ̸= ∙ there is place in the postset being of the same type: (𝑑(∙ ̂︀ that 𝑑(̂︀ 𝑡)∪{∙}) ⊆ (𝑑(̂︀ 𝑡∙ )∪{∙}). An Eos is conservative iff its typing 𝑑 is. 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 𝜇 = 𝑘=1 𝑝̂︀𝑘 [𝑀𝑘 ]. Markings of the form 𝑝[0] ̂︀ with 𝑝) = ∙ are abbreviated 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 𝑁 : (︁⋃︁ (︀ −1 )︀)︁ ℳ := MS 𝑑 (𝑁 ) × MS (𝑃𝑁 ) (5) 𝑁 ∈𝒩 We define the partial order ⊑ on nested multisets by setting 𝜇1 ⊑ 𝜇2 iff ∃𝜇 : 𝜇2 = 𝜇1 + 𝜇. A more liberal variant is the order ⪯ defined by: ⇐⇒ 𝛼 = 𝑚 𝑎𝑖 [𝐴𝑖 ] ∧ 𝛽 = 𝑛𝑗=1 ̂︀𝑏𝑗 [𝐵𝑗 ] ∧ ∑︀ ∑︀ 𝛼⪯𝛽 𝑖=1 ̂︀ ∃ injection 𝑓 : {1, ..., 𝑚} → {1, ..., 𝑛} : (6) ∀1 ≤ 𝑖 ≤ 𝑚 : ̂︀ 𝑎𝑖 = ̂︀𝑏𝑓 (𝑖) ∧ 𝐴𝑖 ≤ 𝐵𝑓 (𝑖) ∑︀For 𝛼 ⪯ 𝛽 the injection 𝑓 generates a sub-marking of 𝛽 which is denoted 𝑓 (𝛼) = 𝑚 𝑎𝑓 (𝑖) [𝐴𝑓 (𝑖) ]. 𝑖=1 ̂︀ Note that 𝛼 ⊑ 𝛽 is a special case of 𝛼 ⪯ 𝛽, where 𝐴𝑖 ≤ 𝐵𝑓 (𝑖) is restricted to 𝐴𝑖 = 𝐵𝑓 (𝑖) . 4 In some sense, net-tokens are object nets with its own marking. However, net-tokens should not be considered as instances of an object net (as in object-oriented programming), since net-tokens do not have an identity. This is reflected by the fact that the firing rule joins and distributes the net-tokens’ markings. Instead, all net-tokes of an object net act as a collective entity, like a group. This group can be considered as an object with identy – an object with its state distributed over the net-tokens. For in in-depth discussion of this semantics cf. [7]. 82 Michael Köhler-Bussmeier et al. CEUR Workshop Proceedings 70–87 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 𝑝̂︀ | 𝑝̂︀ ∈ 𝑃̂︀}, where id 𝑝̂︀ formalises object-autonomous firing on the place 𝑝: ̂︀ 1. Each idle transition id 𝑝̂︀ has 𝑝̂︀ as a side condition: pre(id 𝑝̂︀) = post(id 𝑝̂︀) := 𝑝. ̂︀ 2. Each idle transition id 𝑝̂︀ synchronises only with transitions from 𝑁 = 𝑑(̂︀ 𝑝): ∀̂︀ 𝜏 [𝜗] ∈ Θ : 𝜏̂︀ = id 𝑝̂︀ =⇒ ∀𝑁 ∈ 𝒩 : (𝜗(𝑁 ) ̸= 0 ⇐⇒ 𝑁 = 𝑑(̂︀ 𝑝)) Definition 5 (Elementary Object System, EOS). An elementary object system (Eos) is a tu- ple OS = (𝑁̂︀ , 𝒩 , 𝑑, Θ, 𝜇0 ), where: 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 ̂︀ 𝑡)(𝑁 ) = ch 1 + · · · + 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 ̂︀ 𝑡[𝜗] by setting 𝜗(𝑁 ) := 𝑡1 + · · · + 𝑡𝑛 to be any transition multiset such that the labels match: 𝑙𝑁 (𝑡1 ) + · · · + 𝑙𝑁 (𝑡𝑛 ) = ̂︀ 𝑙(̂︀ 𝑡)(𝑁 ). 83 Michael Köhler-Bussmeier et al. CEUR Workshop Proceedings 70–87 Figure 4: An Elementary Object Net System The system net is 𝑁̂︀ = (𝑃̂︀, 𝑇̂︀, pre, post), where 𝑃̂︀ = {̂︀ 𝑝1 , . . . , 𝑝̂︀6 } and 𝑇̂︀ = {̂︀ 𝑡}. One object net is 𝑁1 = (𝑃1 , 𝑇1 , pre1 , post1 ) with 𝑃1 = {𝑎1 , 𝑏1 } and 𝑇1 = {𝑡1 }. Another object net is 𝑁2 = (𝑃2 , 𝑇2 , pre2 , post2 ) with 𝑃2 = {𝑎2 , 𝑏2 , 𝑐2 } and 𝑇2 = {𝑡2 }. The typing is 𝑑(̂︀ 𝑝1 ) = 𝑑(̂︀ 𝑝2 ) = 𝑑(̂︀𝑝4 ) = 𝑁1 and 𝑑(̂︀ 𝑝3 ) = 𝑑(̂︀𝑝5 ) = 𝑑(̂︀ 𝑝6 ) = 𝑁2 . The labelling generates one event: Θ = {̂︀ 𝑡[𝑁1 ↦→ 𝑡1 , 𝑁2 ↦→ 𝑡2 ]}. The initial marking has two net-tokens on 𝑝̂︀1 , one on 𝑝̂︀2 , and one on 𝑝̂︀3 : 𝜇 = 𝑝̂︀1 [𝑎1 + 𝑏1 ] + 𝑝̂︀1 [0] + 𝑝̂︀2 [𝑎1 ] + 𝑝̂︀3 [𝑎2 + 𝑏2 ] 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. B.1. Firing Rule The projection Π1 on the first component abstracts from the substructure of all net-tokens for a marking of an Eos: (︁∑︁𝑛 )︁ ∑︁𝑛 Π1 𝑝̂︀𝑘 [𝑀𝑘 ] := 𝑝̂︀𝑘 (7) 𝑘=1 𝑘=1 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: (︁∑︁𝑛 )︁ ∑︁𝑛 Π2𝑁 𝑝̂︀𝑘 [𝑀𝑘 ] := 𝑝𝑘 ) · 𝑀𝑘 1𝑁 (̂︀ (8) 𝑘=1 𝑘=1 where the indicator function 1𝑁 : 𝑃̂︀ → {0, 1} is 1𝑁 (̂︀ 𝑝) = 𝑁 . Note that Π2𝑁 (𝜇) 𝑝) = 1 iff 𝑑(̂︀ 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): 84 Michael Köhler-Bussmeier et al. CEUR Workshop Proceedings 70–87 𝜑(̂︀ 𝜏 [𝜗], 𝜆, 𝜌) ⇐⇒ Π1 (𝜆) = pre(̂︀𝜏 ) ∧ Π1 (𝜌) = post(̂︀ 𝜏) ∧ 2 ∀𝑁 ∈ 𝒩 : Π𝑁 (𝜆) ≥ pre𝑁 (𝜗(𝑁 )) ∧ (9) ∀𝑁 ∈ 𝒩 : Π2𝑁 (𝜌) = Π2𝑁 (𝜆) − pre𝑁 (𝜗(𝑁 )) + post𝑁 (𝜗(𝑁 )) ̂︁ = Π1 (𝜆) and 𝑀 With 𝑀 ̂︁′ = Π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 pre- condition 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𝑁 (𝜗(𝑁 )). ′ =𝑀 − 4. The firing of 𝜏̂︀[𝜗] 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 𝑝̂︀) = 𝑝̂︀ = post(id 𝑝̂︀) = Π1 (𝜌). So, there is an addend 𝜆 = 𝑝[𝑀 ̂︀ ] in 𝜇 with 𝑑(̂︀ 𝑝) = 𝑁 and 𝑀 enables 𝜗(𝑁 ). Definition 6 (Firing Rule). Let OS be an Eos and 𝜇, 𝜇′ ∈ ℳ markings. The event 𝜏̂︀[𝜗] is enabled in 𝜇 for the mode (𝜆, 𝜌) ∈ ℳ2 iff 𝜆 ⊑ 𝜇 ∧ 𝜑(̂︀ 𝜏 [𝜗], 𝜆, 𝜌) holds. 𝜏̂︀[𝜗](𝜆,𝜌) An event 𝜏̂︀[𝜗] that is enabled in 𝜇 for the mode (𝜆, 𝜌) can fire: 𝜇 −−−−−→ 𝜇′ . The resulting OS successor marking is defined as 𝜇′ = 𝜇 − 𝜆 + 𝜌. 𝜏̂︀[𝜗] 𝜏̂︀[𝜗](𝜆,𝜌) We write 𝜇 −−→ 𝜇′ whenever 𝜇 −−−−−→ 𝜇′ for some mode (𝜆, 𝜌). OS OS 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 again. The current marking 𝜇 of the Eos enables 𝑡[𝑁1 ↦→ 𝑡1 , 𝑁2 ↦→ 𝑡2 ] in the mode (𝜆, 𝜌), where ̂︀ 𝜇 = 𝑝̂︀1 [0] + 𝑝̂︀1 [𝑎1 + 𝑏1 ] + 𝑝̂︀2 [𝑎1 ] + 𝑝̂︀3 [𝑎2 + 𝑏2 ] = 𝑝̂︀1 [0] + 𝜆 𝜆 = 𝑝̂︀1 [𝑎1 + 𝑏1 ] + 𝑝̂︀2 [𝑎1 ] + 𝑝̂︀3 [𝑎2 + 𝑏2 ] 𝜌 = 𝑝̂︀4 [𝑎1 + 𝑏1 + 𝑏1 ] + 𝑝̂︀5 [0] + 𝑝̂︀6 [𝑐2 ] 85 Michael Köhler-Bussmeier et al. CEUR Workshop Proceedings 70–87 𝑡[𝑁1 ↦→ 𝑡1 , 𝑁2 ↦→ 𝑡2 ] in the mode (𝜆, 𝜌) Figure 5: The EOS of Figure 4 illustrating the firing of ̂︀ 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 transi- tion ̂︀ 𝑡.) After the synchronisation we obtain the successor marking 𝜇′ with net-tokens on 𝑝̂︀4 , 𝑝̂︀5 , and 𝑝̂︀6 as shown in Figure 5: 𝜇′ = (𝜇 − 𝜆) + 𝜌 = 𝑝̂︀1 [0] + 𝜌 = 𝑝̂︀1 [0] + 𝑝̂︀4 [𝑎1 + 𝑏1 + 𝑏1 ] + 𝑝̂︀5 [0] + 𝑝̂︀6 [𝑐2 ] Note, that we have only presented one mode (𝜆, 𝜌) and that other modes are possible, too. B.2. Properties of the Firing Rule In the following we relate those nested multisets, that coincide in their projections. The projection of a marking 𝜇 is defined as follows: Π(𝜇) := (Π1 (𝜇), (Π2𝑁 (𝜇))𝑁 ∈𝒩 ) (10) 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: 𝛼∼ = 𝛽 : ⇐⇒ Π(𝛼) = Π(𝛽) (11) ⇐⇒ Π1 (𝛼) = Π1 (𝛽) ∧ ∀𝑁 ∈ 𝒩 : Π2𝑁 (𝛼) = Π2𝑁 (𝛽) 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 ̂︀ 1 + 𝑝2 ] + 𝑝̂︀′ [𝑝3 ] ∼ 𝑝[𝑝 ̂︀ 3 + 𝑝2 ] + 𝑝̂︀′ [𝑝1 ] = 𝑝[𝑝 which means that ∼ = allows the tokens 𝑝1 and 𝑝3 to change their locations (i.e. between 𝑝̂︀ and 𝑝̂︀′ ). 86 Michael Köhler-Bussmeier et al. CEUR Workshop Proceedings 70–87 Since an event collects all relevant object nets of the firing mode and combines them to one “virtual object net” that is only present at the moment of firing, the location of the object nets’ tokens is irrelevant and can be ignored. These virtual object nets Π2𝑁 (𝜆) are also shown in the example of Figure 4. This invariance can be expressed as follows: Lemma 1. The enabling predicate is invariant with respect to the relation ∼ =: 𝜏 [𝜗], 𝜆, 𝜌) ⇐⇒ (∀𝜆′ , 𝜌′ : 𝜆′ ∼ 𝜑(̂︀ = 𝜆 ∧ 𝜌′ ∼ 𝜏 [𝜗], 𝜆′ , 𝜌′ )) = 𝜌 =⇒ 𝜑(̂︀ Proof From the definition of 𝜑 one can see that the firing mode (𝜆, 𝜌) is used only via its projection by Π. Since 𝜆′ ∼ = 𝜆, 𝜌′ ∼ = 𝜌 expresses equality modulo projection, the predicate 𝜑 cannot distinguish between 𝜆′ and 𝜆, resp. 𝜌′ and 𝜌. □ qed. As for p/t nets the firing rule has several nice properties • Let OS be an Eos and 𝜇 a marking. The event 𝜏̂︀[𝜗] is enabled in the mode (𝜆, 𝜌) iff it is enabled in the mode (𝜆′ , 𝜌′ ) such that 𝜆′ ∼ = 𝜆 ∧ 𝜌′ ∼ = 𝜌. This is an immediate consequence of Lemma 1. • Firing is reversible, i.e. for each Eos OS we obtain OS 𝑟𝑒𝑣 by inverting the arcs and have: 𝜃 𝜃𝑟𝑒𝑣 𝜇1 −−→ 𝜇2 ⇐⇒ 𝜇2 −−−𝑟𝑒𝑣 −→ 𝜇1 . OS OS • The behaviour of an Eos is a conservative extension of p/t nets in the following sense: When one abstract from the net-tokens structure by the projection Π1 , then the behaviour of the system net in the Eos cannot be distinguished from the system net 𝑁 ̂︀ regarded as 𝑡[𝜗] 𝑡 a p/t net, i.e. 𝜇 −−→ 𝜇′ =⇒ Π1 (𝜇) −→ Π1 (𝜇′ ). ̂︀ ̂︀ OS 𝑁 ̂︀ • The invariance calculus for p/t nets can be extended to Eos in a compositional way, i.e. invariance equations can be obtained from the invariance equations of the constituent components separately. 87