=Paper=
{{Paper
|id=Vol-3430/paper5
|storemode=property
|title=Robustness: A natural Definition based on Nets-within-Nets
|pdfUrl=https://ceur-ws.org/Vol-3430/paper5.pdf
|volume=Vol-3430
|authors=Michael Köhler-Bussmeier,Lorenzo Capra
|dblpUrl=https://dblp.org/rec/conf/apn/Kohler-Bussmeier23a
}}
==Robustness: A natural Definition based on Nets-within-Nets==
https://ceur-ws.org/Vol-3430/paper5.pdf
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