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 outof-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).
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 [
After we have identified net-tokens as computational units it is straightforward to define robustness: Robustness means that the system still provides its service even when one or more units are malfunctioning. Here, we model a malfunction by a complete deactivation of a net-token, which provides no observable inner activity any more. To formally express the crash-failure of computational units we define a state space extension where we have so called crash or break-down events.
Our main application area are multi-agent systems (MAS). The first author uses
nets-withinnets to specify adaptivity of agents in the context MAS-organisations [
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 [
The paper has the following structure. Section 2 introduces base nets-within-nets (Eos). Section 3 defines the concept of robustness for Eos: The definition extends the reachability graph with additional events that model a break-down. In Section 4 we show that this semantic extension can be characterized syntactically by a slight modification of the Eos structure. The work closes with a conclusion and outlook.
Object nets [
1Sometimes 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.
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 [
̂︀ net-token from 1 to 2 without changing its marking. 1 to 2. The object net remains at its location 1.
̂︀ 2. Object autonomous: The object net fires transition 1 by “moving” the black token from 3. Synchronisation: Whenever we add matching synchronisation inscriptions at the system synchronisation is specified, autonomous actions are forbidden. net transition ̂︀and the object net transition 1, then both must fire synchronously: The object net is moved to ̂︀2 whereas the black token moves from 1 to 2 inside. Whenever since ̂︀ ̸∈ .
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 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 = ∑︀ where − 1( ) ⊆ ̂︀ is the set of system net places of the type : also denoted as = ∑︀ and is the marking of a net-token with type (̂︀). To emphasise the nesting, markings are The set of all markings which are syntactically consistent with the typing is denoted ℳ, =1 ̂︀[]. For example, the marking show in Fig. 1 is = ̂︀1[1].
=1(̂︀, ), where ̂︀ is a place of the system net ℳ := MS ︁( ⋃︁ ∈ ︀( − 1( ) × ple OS = (̂︀ , , , Θ, 0), where:
More details – e.g. the firing rule →−− OS
object nets, with disjoint set of nodes.
′ – are given in the appendix. For a in-depth
presentation of Eos cf. [
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 [
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 [
Assume a given Eos OS = (̂︀ , , , Θ, 0). Its reachability graph RG (OS ) defines the behaviour in the absence of failures, i.e. the reachability graph is the state space for = 0 break-downs.
̂︀
In the following we assume break-downs. We tag markings with the number of breakdowns and denote this as the pair ⟨, ⟩.
For technical convenience, we assume that transitions in object nets have a non-empty preset, so, the empty marking disables object-autonomous events and synchronisations. As a consequence, a break-down is like an enforced deadlock in the net-token.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) 2If one wishes to distinguish between a deadlock and a break-down, we have to ensure that net-tokens do not +1 =
{⟨ ′′, + 1⟩ | (⟨, ⟩, ⟨ ′, + 1⟩) ∈ +1 ∧ →′− * ′′} We define the edges of level as: := {(⟨, ⟩, ⟨ ′, ⟩) | →− ′}
Each sub-graph (, ) contains all the node of the same level and these sub-graphs are disjoint, since there are no edges from a higher level to a lower level, i.e. the level is increased sion of OS up to level or the -failure extension.
The graph RG * (OS ) := ( * , * ) where * := ⋃︀ ︁( ⋃︀
=0 , ⋃︀ the * -failure extension.
︁) =0( ∪ ) is called the failure exten≥ 0 and * = ⋃︀ ≥ 0( ∪ ) is called
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: (0, 0→)−− − 1 (1, 1→)−− − · · · 2 →−− − (, )
′ = ̂︀[0] + ′′, i.e. by a break-down of the net-token [ ]. ̂︀
We use the following partial-order ⪯ on nested multi-sets: 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 ∑︀=1 ̂︀ [] ⪯ ∑︀=1 ̂︀ [ ] ⇐⇒ ∃ injection : {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 systemautonomous events are possible. Thus, in the limit the Eos behaves like the system net ̂︀ when considered as a p/t net. Technically we obtain this behaviour by the projection Π1, which maps a marking to the multiset of system net places. 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.
RG (OS ). This is denoted by OS , 0 |= , or short: 0 |= wheneverOS is clear from the context.
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 [
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 [
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. [
robust.
Another interesting question is whether we can tolerate break-downs using redundancy, i.e., multiple copies of the net-tokens. This question is closely related to the Petri net concept of monotonicity. A property is monotonous if it holds also for any greater initial marking. It is well known that reachability is monotonous, while deadlock-freedom or liveness are – in general – not (However, for the structural sub-class of free-choice nets liveness is monotonous).
For monotonous properties redundancy is useful, i.e. we can add additional net-tokens to survive knock-outs of net-tokens. Here we simply multiply the initial marking and consider 0 + · 0.
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.
Our characterisation of robustness has the drawback that it is based on an extension of the usual Petri net semantics as we extend the reachability graph. In the following, we like to show that we can express this extension on a purely syntactical level, i.e., we modify the EosOS into another Eos OS * with the property that the ‘normal’ reachability graph of OS * is isomorphic to the break-down extension RG * (OS ). In this case, we can reduce the specialised analysis of OS to an ‘normal’ analysis of OS * using existing standard tools.
The main idea is quite simple (cf. Fig. 2): We apply the following construction to the Eos OS . • We add a run-place to each object net and this run-place is attached as a side condition to each transition . • The run-place is initially marked with one token. • We add a new transition to each object net that synchronises with the environment (via the channel ⟨of ⟩) and removes the token of the run-place. • In the system net we add for each place a new side transition
̂︀ ̂︀̂︀, which synchronises with .
The efect of the synchronous kill-event is that the net-token is dead afterwards (but usually contains useless tokens on the places other than the run-place). We like to establish that an empty run-place always indicates that the net-token has broken down. In this case we could drop the explicit tag from the state because it is implicitly given by the number of net-tokens with an empty run-place. However, this is not true, since the Eos firing rule ‘collects’ the net-tokens markings from all incoming arcs and ‘distributes’ this sum over all net-tokens generated on the outgoing arcs. For a system net transition that has, e.g., one incoming arc and two outgoing arcs, one of the generated net-tokens must have an empty run-place. However, the net-token should not be regarded as a break-down.
We can ‘repair’ this problem in the following way: We replace each system net transition ̂︀ by a simple subnet (cf. Fig. 3) that removes the tokens from the incoming places ̂︀ (using the synchronisation channel ⟨of ⟩ times) and individually re-creates one token on each run-place in each net-token on the outgoing places ̂︀′ (using the synchronisation channel ⟨on⟩ at the internal transitions ̂︀). We replace each system net transition with such a subnet.3 The resulting Eos is denoted as OS * .
Due to this construction, an empty run-place in a net-token (except for those net-tokens in the intermediate place ̂︀′′ of the subnet) is equivalent to a break-down.
When we consider the intermediate transitions ̂︀ as ‘silent’ events, then the constructed net OS * is bisimilar to the original state space OS .
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 .
3We could skip this construction for system net transitions which have exactly one place in the preset and one in the postset.
of OS , i.e. both state spaces are bisimilar: RG (OS ) ≈ RG (OS )
In the absence of break-downs, i.e., for = 0, the normal semantics coincides with the extended semantics and the given Eos coincides with its extension: Fact 3. For = 0 we obtain that all systems coincide: RG (OS ) ≃ RG 0(OS ) ≈ RG (OS 0).
With these constructions we have reduced checking properties w.r.t. robustness to a usual state space based query.
In this paper, we have shown that Nets-within-Nets have an intuitive representation of the concept of a ‘computational unit’: the net-tokens. Based on this, we could define a break-down of net-tokens and define the satisfiability of properties in the context of break-downs.
Our concept of robustness relies on an extension of the state space. We provided a reduction of this semantical definition (which extends the Petri net semantics) to a syntactical one (where we use the usual semantics): We transformed the Eos OS into the Eos OS * such that the ‘normal’ reachability graph of OS * is bisimilar to the break-down extension RG * (OS ). Therefore, we could still use existing tools to investigate robustness.
We plan to extend the simple – though 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
[
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-diference 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 representation in the form m = ∑︀∈ m() · , where m() denotes the multiplicity of . Multisets can also be represented as a formal sum in the form m = ∑︀ =1 , where ∈ .
Any mapping : → ′ is extended to a multiset homomorphism ♯ : MS () → MS (′): ♯ (∑︀ =1 (). This includes the special case ♯(0) = 0. We simply write =1 ) = ∑︀ 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 if ∀ ∈ : 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}.
so called black tokens.
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, An Eos is conservative if its typing is.
Typing type .4 No place of the system net is mapped to the system net itself since ̂︀ ̸∈ . a place ̂︀ ∈ ̂︀ of the system net with () = may contain only net-tokens of the object net ̂︀
The system net places are typed by the mapping : ̂︀ → with the meaning, that that (̂︀) ̸= ∙ there is place in the postset being of the same type: ((∙ ̂︀)∪{∙} ) ⊆ A typing is called conservative if for each place in the preset of a system net transition ̂︀such ̂︀ ((̂︀∙ )∪{∙} ).
An Eos is p/t-like if 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 (̂︀) = ∙ are abbreviated as [].
̂︀ the nesting, markings are also denoted as = ∑︀| | a place of the system net and is the marking of a net-token with type (̂︀). To emphasise =1 ̂︀[]. Markings of the form ̂︀[0] with where − 1( ) ⊆ ̂︀ is the set of system net places of the type :
The set of all markings which are syntactically consistent with the typing is denoted ℳ, ℳ := MS ︁( ⋃︁ ⊑ on nested multisets by setting 1 ⊑ 2 if ∃ : 2 = 1 + .
We define the partial order A more liberal variant is the order ⪯ ⪯ ⇐⇒ = ∑︀ =1 ̂︀ [] ∧ = ∑︀
=1 ̂︀ [ ] ∧
: ̂︀ = ̂︀ () ∧ ≤ () For
Note that the injection generates a sub-marking of which is denoted ( ) = ⊑ is a special case of ⪯ , where ≤ () is restricted to = (). 4In 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. [
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). ple OS = (̂︀ , , , Θ, 0), where:
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. ̂︀ ̂︀
5In the graphical representation the events are generated by transition inscriptions. For each object net ∈ a system net transition ̂︀ is labelled with a multiset of channels ̂︀(̂︀)( ) = ch1 + · · · + ch, depicted as ⟨ :ch1, :ch2, . . .⟩. Similarily, an object net transition may be labelled with a channel () = ch – depicted as ⟨:ch⟩ whenver there is such a label. We obtain an event ̂︀[] by setting ( ) := 1 + · · · + to be any transition multiset such that the labels match: (1) + · · · + () = ̂︀(̂︀)( ). 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 diferent. ̂︀ 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 (︁ ∑︁=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: Π =1 ̂︀[]︁) := ∑︁=1 1 (̂︀) · 2 (︁ ∑︁ (7) (8) where the indicator function 1 : ̂︀ → {0, 1} is 1 (̂︀) = 1 if (̂︀) = . Note that Π2 ( ) 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): Π1( ) = pre(̂︀) ∧ Π1( ) = post(̂︀) ∧
pre (( )) ∧ ∀ ∈ : Π2 ( ) = Π2 ( ) − pre (( )) + post (( )) (9) ∈ the predicate has the following meaning:
With ̂︁ = Π1( ) and ̂︁′ = Π1( ) as well as = Π2 ( ) and ′ = Π2 ( ) for all 1. The first conjunct expresses that the system net multiset ̂︁ corresponds to the precondition of the system net transition , i.e. ̂︁ = pre( ).
̂︀ ̂︀ 2. In turn, a multiset ̂︁′ is produced, that corresponds to the post-set of . 3. A multi-set ( ) of object net transitions is enabled if the sum of the net-token ̂︀ markings (of type ) enable it, i.e. ≥
pre (( )).
object net’s transitions on the net-tokens. 4. The firing of ̂︀[] must also obey the object marking distribution condition: ′ = − pre (( )) + post (( )), where post (( )) − pre (( )) is the efect of the 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 Π1( ). So, there is an addend = [ ] in with (̂︀) = and enables ( ).
̂︀ system net and the first and the second conjunct is:
Analogously, for an object-autonomous event we have an idle-transition ̂︀ = id for the ̂︀ Π1( ) = pre(id ) = = post(id ) = ̂︀ ̂︀ enabled in for the mode (, ) ∈ ℳ2 if ⊑ ∧ ( [], , ) 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
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[1 + 1] + 2[1] + 3[2 + 2] = ̂︀1[0] + 1[1 + 1] + 2[1] + 3[2 + 2] = ̂︀1[0] +
̂︀ ̂︀ ̂︀ = 4[1 + 1 + 1] + 5[0] + 6[2] ̂︀
̂︀ ̂︀
The net-token markings are added by the projections Π2 resulting in the markings Π2 ( ). The sub-synchronisation generates Π2 ( ). (The results are shown above and below the transition ̂︀.) After the synchronisation we obtain the successor marking ′ with net-tokens on ̂︀4, 5, and 6 as shown in Figure 5: ̂︀ ̂︀ ′ = ( − ) + = ̂︀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 ( ))∈ ) 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: ∼= : ⇐⇒ ⇐⇒ Π( ) = Π( ) Π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 ′). ̂︀ (10) (11)
Since an event collects all relevant object nets of the firing mode and combines them to one example of Figure 4. This invariance can be expressed as follows: “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 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 . □
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 (, ) if it is enabled in the mode ( ′, ′) such that ′ ∼= ∧ ′ ∼= . This is an immediate consequence ̂︀ • Firing is reversible, i.e. for each Eos OS we obtain OS by inverting the arcs and have: • 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. →−− OS ̂︀[] →− components separately. • 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