Elementary Object Systems (EOS) is a class of Object Petri Nets that follows the “nets-within-nets” paradigm. It combines several practical as well as theoretical properties for the needs of multi-agent-systems. However, it comes with some constraints that limit their expressiveness for automatic verification purposes due to the highly expressive nature of the underlying class of Petri nets. In this paper, we proposed a set of transformation rules from EOS to basic Petri nets nets and show isomorphism of the state spaces in order to make verification feasible.
Elementary Object Systems (EOS for short) are based on the nets-within-nets
paradigm of
We aim to provide a path to verification of properties of a slightly modified version
of EOS, called elementary reference-net systems (ERS), with reference semantics that
is practically relevant and overcomes fundamental decidability issues with other
formalists as shown in
Compared to EOS, two main additions are introduced for ERS: Firstly, we provide each marked object net located in places of the system net with a unique name so that object nets with the same marking can be distinguished. Secondly, we use variables to label arcs of the system net. So that when firing transitions, variables are bound to object nets names instead of statically typing system net places allowing dynamic use of net-tokens without fixing types for places of the system net.
We extend the notion of 1-safe P/T nets to ERS to guarantee that the state space is finite and markings are bounded. Further to the definition of ERS, we propose a set of transformation rules from 1-safe ERS into P/T nets and show isomorphism of the state spaces of ERS with its generated P/T net.
In Section 2 we review some preliminaries from Petri net theory. Section 3 gives an introduction to ERS. Section 4 presents the set of transformation rules from 1-safe ERS to 1-safe P/T nets. Section 5 proves the isomorphism of the state spaces of 1-safe ERS and of the transformed 1-safe P/T net. 2
Here we give some definitions from theory of P/T-net, Relevant for our study.
Definition 2.1(P/T net) A place/transition is a tuple = ( , , , )where is a finite set of places, is a finite set of transitions, disjoint from , ⊆ ( × ) ∪ ( × ) is the flow relation, and : ⟶ ℕ\{0} is the arc weight function. The preset of a node ∈ ∪ , denoted ⦁ , is the set containing the elements that immediately precede in the net i.e.: ⦁ = { ∈ ∪ |( , ) ∈ }. Analogously, the postset of a node is denoted ⦁.
Definition 2.2 (Marking and Enabled transition ). A marking of a P/T-net = ( , , , ) is a function : ⟶ ℕ. A P/T net system =( , 0) is a net = ( , , ) together with an initial marking 0. Let Σ = ( , 0) be a net system. A transition ∈ is enabled in a marking iff ( ) ≥ ( , )for all ∈ ⦁ . An enabled transition in marking is denoted by [ >. A transition that is enabled in a marking may or may not fire. Firing of transition removes tokens from input places of and puts new tokens onto output places of . The successor marking ′ is defined as ′ ( ) = ( ) − ( , ) + ( , ). We denote this by [ > ′. For a finite sequence of transition = 1, … , we write [ > ′ if there are markings 1, … +1 such that 1 = , +1 = ′ and [ > +1, for all = 1, … , . The set of reachable markings of Σ is the set of all markings reachable from the initial marking. Σ is k-bounded if, for every reachable marking m and every place p ∈ P, m(p) ≤ k, and Σ is safe if it is 1-bounded. Moreover, Σ is bounded if it is k-bounded, for some k ∈ N. One can show that the set RM(Σ) is finite if Σ is bounded i.e. if |RM(Σ)| < ∞. 3
Elementary Reference-net System (ERS) By convention, the components of the system net will carry a hat: ̂ , ̂ , ̂, ̂, … etc.
Definition 3.1 Let the triple = ( , , ) be a named marked object net, where , is a unique name of an object net; is a structure of the object net, and is a marking in . (Let Σ = {( 1, 1, 1), … , ( , , )} be a finite set of unique marked named object nets). The structure of an object net with a unique name ∈ Σ is a P/T- net = ( , , ), where , is the set of places of the object net, is the set of its transitions and
⊆ ( × ) ∪ ( × ) is the flow relation. We assumed that all sets of nodes are pairwise disjoint and set Σ ≔ ⋃ ∈Σ Σ ≔ ⋃ ∈Σ . By • we denote the name of ordinary black tokens.
Definition 3.2 (ERS)
Let
be a finite set of named variables. An elementary reference-net system is a tuple
= ( ̂ , Σ 0, ℓ, , ) where ̂ = ( ̂ , ̂ , ̂ ) is a p/t net called a system net, where ̂ is its set of places, ̂ is its set of transitions and ̂ ⊆ ( ̂ × ̂ ) ∪ ( ̂ × ̂ ) is the flow relation. Σ 0 ≔ {( 1, 1, 10), … , ( , , 0)}, is a finite set of marked named object nets. ℓ ⊆ ( ̂ ∪ { ̂}) × ( 1i ∪ { }) ×, … , ( ∪ { })\{ ̂, , … , )} , is the synchronisation relation, where ̂and are special symbols intended to denote inactions at the system and the object net levels respectively. If = ( ̂, 1, … , ) and ̂, ≠ and ∃ ∈ {1, … , } such that ≠ , then we say that ̂ ∈ Σ for every ∈ {1, … , } with = |Σ|, participate in . This is the reason why ( ̂, , … , ) is excluded from the set of synchronisation relation: at least one object net must participate in every synchronisation action with the system net. : ̂ ⟶
∪ { •} is an arc labelling function such that for an arc ̂ ∈ ( ̂ ) adjacent to a place ̂the inscription of
( ̂ ) matches the name of object net in ̂ specifies the initial making, where : ̂ → ℕ ∪ (Σ) ℎ Σ = {( 1, 1, 1), … , ( , , }. It has to satisfy the condition ( ̂) ∈ ℕ ⟺ ( ̂) ∈ { ⦁}.
= ( ̂ , Σ, ℓ, , ) is shown, where Σ = { 1, 2}.
to marked named object nets in places ̂ 1 it. In the initial marking, places 1̂ object nets 1 2 respectively.
̂2 adjacent to transition ̂ ′ to enable ̂2 contain references to the marked named
= { |( , ,, ) ∈ Σ}, a finite set of object nets names.
Moreover, variables appearing on arcs adjacent to a transition ̂of the system net must satisfy the following four conditions: ∀ ̂∈ ̂ ∀ ̂∈ ̂ ∀ ̂∈ ⦁ ̂, ∃ ̂′ ∈ ̂⦁, ∀ ̂∈ ⦁ ̂, ∃ ̂′ ∈ ̂⦁, ℎ ℎ ( ̂, ̂) = ( ̂, ̂′) ( ̂, ̂) = • (1) ℎ ℎ ( ̂′, ̂) = ( ̂, ̂) ( ̂, ̂) = • (2) ∀ ̂∈ ̂ and for any two places 1̂, ̂2, ∈ ⦁ ̂, 1̂ ≠ ̂2 ℎ ( 1̂, ̂) ≠ ( ̂2, ̂). (3) ∀ ̂∈ ̂ and ̂′1, ̂′2, ∈ ̂⦁, ̂1 ≠ ̂2 ℎ ( ̂, ̂′1) ≠ ( ̂, ̂′2). (4)
Condition (1) says that each variable appearing in the incoming arc of a system net transition ̂also has to appear in the outgoing arc of ̂ or no such variable exist. Condition (2) says that each variable appearing in the outgoing arc of a system net transition ̂also has to appear in the incoming arc of ̂ or no such variable exist. These two conditions means that no new object net is created and no destroyed after a transition firing in the system net. Condition (3) prevents the ability to join two object nets, and (4) prevents the splitting of an object net. This is because in reality, complex physical entities cannot be cloned at run time. With these restrictions, ERS still retain the ability to describe nesting of object nets, synchronisation, and mobility, but does not allow splitting of the inner marking of an object net or joining the inner marking of several object nets. Assuming these inner markings as modelling the inner state of an agent, this is a reasonable restriction and ERSs are then well suitable to model physical entities
For its behaviour, we introduce the notion of marking for elementary reference-net system ERS under reference semantics. Hence in general a marking is given by 1. a distribution of object nets or black tokens : ̂ → ℕ ∪ (Σ) and 2. The vector = ( 1, … , ) with the current marking of each (1 ≤ ≤ ).
specifies for each system net place ̂a number of black tokens or a multiset of marked named object nets (if ̂contain reference(s) to marked named object nets). If we abbreviate ( 1, … , ) by and the set of all such vectors by ℳ, we obtain the following Definition 3.3. By Π ( ) we denote the − ℎ component of and by → the tuple, where the − ℎ component is substituted by , ∈ ℕ .
In what follows a marked named object net is referred to as net-token. For a given ERS, by ∑ = Σ ∪ { •} we denote the set of all marked named net-tokens. Only when not introduced in the marking! Sometimes by abuse of notation, for a named object net ( , , ) in a place ̂of a marking of the system net we write ( ̂) =
Definition 3.3 Given an elementary reference-net system = ( ̂ , Σ , ℓ, , ) we define ℳ ≔ { | = ( 1, … , ) ∧ ∈ ( )}. Then a marking of an elementary reference-net system is a pair ( , ) where ∈ ℳand : ̂ → (Σ ). Specifying 0 by the initial markings of the marked named object nets 0 = ( 10, … , 0) we obtain the initial marking ( , ) of . The set of all markings of is denoted by ℳr .
Let ̂∈ ̂ be a transition in the system net ̂ , then • ̂= { ̂|( ̂, ̂) ∈ ̂ }, and ̂⦁ = { ̂|( ̂, ̂) ∈ ̂ } are sets of its pre- and post-conditions. We denote by ( ̂) ≔ { ( ̂, ̂)|( ̂, ̂) ∈ ̂ } ∪ { ( ̂, ̂)|( ̂, ̂) ∈ ̂ } = ⦁ ̂× { ̂} ∪ { } × ̂⦁ the set of all variables on arcs adjacent to ̂. A binding specifies which variables are bound to names, where : ( ̂) ∪ {•} ⟶ ∪ { ⦁}with = { |( , ,, ) ∈ Σ} satisfying the conditions: for each ∈ ( ̂)∪ {•}, there exist ∈ such that ( ) = =• ℎ ( ) = •.
The firing rule will be introduced in three modes.
Definition 3.4 (synchronisation firing mode) Let( , )be a marking of an elementary reference-net system, ̂∈ ̂ a transition of ̂ , and let be a variable binding defined for all ∈ ( ̂)∪ {•}. Let 1,..., ∈ Σ be object nets involved in the firing of ̂. Then ̂ can fire provided that in each ∈ Σ for every ∈ {1,…, } a transition ∈ Σ such that( ̂, 1,…, ) ∈ ℓ. Then ( ̂, 1,…, ) is enabled in ( , ) if: ∀ ̂ ∈ ̂: ( ( ( ̂, ̂)), ( (̂,̂)), ( (̂,̂))) ∈ ( ̂) and ∀ ∈ ∶ Π ( ) ≥ ( , ),.
This is denoted by ( , )[ ̂, > Let be [ > ′ (w.r.t ). The successor marking ( ′, ′) is defined by
Definition 3.6(object –autonomous firing mode) Let ( , ) be a marking of an elementary reference-net system = (̂ ,Σ ,ℓ, , )and ∈ a transition of a net-token = ( , , ) ∈ ( ̂) for some ̂∈ ̂, such that ∄( ̂, ,…, ,…, ) ∈ ℓ, and is activated in . Then we say that ( ̂, ) is activated in ( , ) (denoted( , )[( ̂, ) >]. The successor marking ( ′, ′) of RS is defined by ′ = and ′ = 1→ miif [ > ′ for Π ( ) = . ′(̂) = ( ̂)\( ( ( ̂, ̂)), ( (̂,̂)), ( (̂,̂))) ∪ ( ( ( ̂, ̂)), ( (̂,̂ )), ( (̂,̂))):∀ ̂∈ ̂ and ′ = → .
This is denoted by ( , )[̂, > ( ′, ′). (5) (6) (7) (8) (9)
Definition 3.5(system-autonomous firing mode) Let ( , ) be a marking of an elementary reference-net system = (̂ ,Σ ,ℓ, , )and ̂∈ ̂ a transition of ̂ with a binding such that ∄( ̂, ,…, ) ∈ ℓ ∶ ∃ ∈ {1,…, } ∶ ≠ . Then ̂ activated in ( , ) if there is a net token such that: ( ( ( ̂, ̂)), ( (̂,̂)), ( (̂,̂))) ∈ ( ̂)∀ ̂∈ ̂ .
marking ( ′, ′)is defined by ∀ ̂∈ ̂ ∶ ′( ̂)= ( ̂)\( ( ( ̂, ̂)), ( (̂,̂)), ( (̂,̂)))∪ ( ( ( ̂, ̂)), ( (̂,̂ )), ( (̂,̂))) ′ = .
This is denoted by ( . )[( 1̂, ) > ( ′, ′).
We denote this by ( , )[( ̂, ) > ( ′, ′).
Definition 3.2. Let be an ( , ), ( ′, ′) ∈ ℳ . as defined in
Definition 3.7 For a new alphabet Γ ≔ ( ̂ ∪ { ̂}) × ( 1 ∪ { }) ×, … , ( ∪ { })\ ( ̂, , … , )where ( ̂, , … , ) denotes the neutral element of Γ∗, we define: ( , )[( ̂, , … , ) > ( ′, ′) if ( , ) = ( ′, ′) and
( , )[ ̆ ( ̂, ) > ( ′, ′) ∃( ′′, ′′) ∶ ( , )[ ̆ > ( ′′, ′′) ( ′′, ′′)[( ̂, ) > ( ′, ′) ̆ ∈ Γ∗, ̂, ∈ ̂ ∪ { ̂} ∈ (( 1 ∪ { }) × , … , ( ∪ { }). ( 10)
∗ actions we write ( , ) → ( ′, ′).
denoted by ( , ( , )). ( ), is the set of markings reachable from the initial marking ( , ). The reachability graph ( ( ) is obtain as for P/T-net systems, which is a digraph whose nodes is the set of reachable markings and edges are the ( ̂, ) tuples (( , ), ( ̂, ), ( ′, ′)) ∈ ℳ × ( ̂, ) × ℳ where ( , ) → ( ′, ′).
We now extend the definition of 1-safe P/T-net to ERS. We introduce two conditions for safeness of ERS as a generalisation of the safeness notion for P/T-nets.
Definition 3.8 (1-safe ERS) = ( ̂ , Σ, ℓ, , ) . RS is 1-safe if and only if all reachable markings are 1-safe and if and only if in all reachable markings there is at most one net-token on each system net place and each net-token is 1safe i.e.,: ∀( , ) ∈ ( ), ∀ ̂∈ ̂ : ( ( ̂), ) ≤ 1 and ∀( , , ) ∈ ( ̂):∀ ∈ ∶ ∀ ̂∈ ̂ ( ( ̂), Π ( ( )) > 0 ⟹ Π ( ( )) ≤ 1.
4
We construct a behaviorally equivalent finite P/T-net model for the entire ERS model and show this by strong bisimulation equivalence between states of the two models. By doing so, we develop a set of transformation rules that provide the same behavioral properties as the original one for formal verification and analysis.
Related work can be found in
Transformation Rules
This subsection gives a set of transformation rules for transforming Elementary Reference-net system (Section 3) into P/T-net. There exist five rules and they must be applied in sequence from Rule 1 to Rule 5. With these rules ERS can be translated into a P/T net system ∗.
Let = ( ̂ , Σ, ℓ, , )be an ERS with a set Σ of all marked named net tokens in the initial marking. By ℝ we denote the set of all names used in Σ . The net will be translated into a P/T-net system ∗ = ( ∗ ∗, ∗∗, ∗∗, 0∗)
Rule 1: Generate the set ∗∗ of places of a P/T-net ∗. The first, is the set ′ ∗ of places from the system net ̂ , and the second the set ∗ of all places of each nettoken in the initial marking of the system net. Finally, we take the union of these set as the set ∗∗ of a target P/T-net ∗, with the assumption that ′ ∗ ∩ ∗∗ = ∅.
′ ∗ is generated by duplicating all places of the system net for each net-token name used in the initial marking of the system net and labelled it with a pair ( ′, ) where ′is a place in ̂ . Thus the set is defined as follows:
′ ∗ ≔ ⋃ ′∈ ̂ {( ′, )| ∈ ℝ, ≥ 1} .
∗∗ ≔ ′ ∗ ∪ ∗ .
Rule 2: Define the initial marking for ∗. For a P/T-net ∗ we define an encoding of markings on places from the set of places ̂ in an ERS by markings on the generated places from ∗∗. If a net-token with name ∈ ℝ resides in a place ̂in an initial ∗ is generated by taking a copy of each place in the set for each net-token and labelled it with a pair ( , ) where is a place in . It is defined as follows: (11) (12) (13) ∗ ≔ ⋃ ∈Σ {( , )| ∈ , ∈ ℝ, ≥ 1} .
Therefore the set ∗∗ of a target P/T-net ∗ as shown in Fig.2 is the union of these set, namely initial marking 0∗ of the constructed, namely marking 0( ̂) of the system net, then a black token in placed on ( ̂, ) ∈ ∗∗ as the 0∗( ̂, ) = 0( ̂). on ( ̂, ) ∈ ∗∗ in 0∗ ,namely 0∗( , ) = 0( ).
Also, we define an encoding of markings on places from the set of places on the generated places from ∗∗. If all places ( , ) for all such that ( , ) ∈ ∗ ∗ is marked in the initial marking 0 of the net-token ∈ ℝ , then of black token is placed (14) (15)
copy corresponding to the place in ∗ is also marked with a black token. In the given the markings for places ( 1, 1) and ( 1, 2). This is illustrated in Fig.3 above.
sides in ̂ 2. Hence, we have tokens in ( ′1, 1) and( ′2, 2) for ∗. Likewise, we define ∗
Rule 3: Generate a family of P/T-net transitions from a system net. We define a set of transitions of ∗ obtained from each autonomous transition of the system net ̂ by duplicating each autonomous transition for each input arc variable of ̂ that may be bound to any of the named net-token name in each place adjacent to ̂with appropriate input and output arcs, in ∗. ∗ ≔ ⋃ ̂∈ ̂ { ′ ( )| ∈ ( ̂): ̂ }.
(16)
named net-token for ′2 is as follows: ( ( ′2)) = { 1 = ( = 1) 2 = ( = 2)} . (17) Where 1
and 2 are bound to the input arc variable , respectively. Therefore, two transitions ′21
′22 are generated for transition ′2 from Rule 3.
= ⋃ ̂ ∈ ̂ {( ′, ′|( , ) = ( ̂ ), ′ ∈ ′ ∗( ) ∪ ∗ ( ), ′ ∈ ′ ∗( ) ∪ Rule 4: Generate a family of transitions representing autonomous transitions in of transitions of ∗ we define a set of similar autono ∗ ∗ ( )} . each net-token. For a set ∗ mous transitions as follows. } .
We define a set ∗
of arcs of net-token autonomous transitions in ∗as follows: ∗ = {( , ), ) ∈ ∗ × ∗ |( , ) ∈ > 0} ∪ {( , ( . ) ∈ ∗
× ∗|( , ) ∈ > 0} .
obtained from the system net and net-tokens. An occurrence of a synchronous firing presumes simultaneous occurrence of a transition ̂∈ ̂ with a set of transitions given by a binding in system net, and some net-tokens transitions( 1, … , ) ∈ ℓ. This can be viewed as a combination of Rule 3 and Rule 4 with the condition that all involved transitions must be elements in the transition relation ℓ of an ERS.
Transitions ( 1, … , ) occur simultaneously with ̂∈ ̂ of a system net, if ( ̂, ( , … , )) ∈ . We generate synchronisation transitions from an ERS in a P/Tnet ∗ accordingly. This implies that we will have |ℓ| such transitions in ∗. Each of these transitions is composed of a system net transition ̂∈ ̂ , and some transitions of net-tokens that participate in synchronous firing of ̂. They are defined as follows. In our example two places 1̂
̂2 are marked with one net-token each in the initial marking. We add two transitions 1 = {{ 1̂, 21, } and 2 = { 1̂, , 22} annotated net is shown in Fig. 7. (18) (19) (20)
We establish an isomorphism between the states of an ERS and the generated 1safe P/T-net. Recall that in Rule 2 we defined two separate initial markings for the P/T-net N∗: M0∗(p̂, i) and M0∗(p, i). The former is an encoding of markings from the set of places ̂P of the system net in an ERS and the latter is an encoding of markings from the set of places Pi of a net-token i. Likewise, we defined three sets of transitions: Ts∗at, Tn∗at, and Ts∗ynci from Rule 3, Rule 4 and Rule 5 respectively in N∗. In the following, we define some mappings from the P/T-net to and ERS.
places ̂ to markings of a system net of an ERS as follows: ̂( ∗)( ̂, ) = ( ̂) ℎ ℎ
( ̂, ) ∈ ∗∗: ̂∈ ̂ : ∈ ℝ .
places of net-token of ERS to a marking of a net-token of ERS as follows: ( ∗)( , ) = ( ) ℎ ℎ
( , ) ∈ ∗∗: ∈ : ∈ ℝ .
Definition 5.3 ̂ is a mapping that maps a transition ′ ( ) ∈ ∗ of P/T-net ∗ to a system-autonomous firing mode ( ̂, ) ∉ (ℓ) of an ERS as follows: ̂ ( ′ ( )) = ( ̂, ) . ( ) = ( , ) .
ℎ ( ) is a binding function that binds a variable ∈ ( ̂) on arcs adjacent to ̂ to an object net name.
an object-autonomous firing mode ( , ) ∉ (ℓ) of an ERS as follows:
Definition 5.5 is a mapping function that maps a transition . ( ) ∈ ∗ of
(22) (23) (24) (25) The following equality holds: 2 = ̂( 2∗) .
Lemma 5.8 Suppose that 1 = ̂( 1∗), 1∗[ ′ ( ) > 2∗, and 1[ ̂ ( ′ ( )) > 2.
= ( ∗) and( , ) = ( ). The following proposi 0( ) = ( 0∗)( , ) .
∗[ ( ) > ⇔ [(( , )) > . 2 = ( 2∗) .
Lemma 5.11 Suppose that 1 = ( 1∗), 1∗[ > 2∗, and 1[ ( ) > 2. The following equality holds:
Lemma 5.12 Suppose that ( 1, 1) = ( 1∗) and = ( . ( )). The following proposition holds: ( . ( )) = {( ̂, 1, … , )} .
0( ̂) = ̂( 0∗)( ̂, ) . ∗[ ′ ( ) > ⇔ [( ̂, ) > .
Lemma 5.7 Suppose that = ̂( ∗) and( ̂, ) = ̂ ( ′ ( )). The following proposition holds: 1∗[ ( . ( )) > ⇔ ( 1, 1)[ > .
( 2, 2) = ( 2∗) .
Lemma 5.13 Suppose( 1, 1) = ( 1∗), 1∗[ . ( ) > 2∗ and ( 1, 1)[ ( . ( )) > ( 2, 2) . From the above Lemmas, the following theorem holds.
Theorem 5.14 Let RS be a 1-safe ERS. Let also N∗be a 1-safe P/T-net obtained from RS by the set of transformation Rules 1 to 5 above. Then state spaces of RS and N∗ are isomorphic.
Proof: Lemmas5.6 and 5.9 defines a one-to-one mapping between the initial markings of the 1-safe P/T-net ∗and the initial marking in RS. From Lemma 5.7 a system-autonomous firing mode ( ̂, ) is enabled in a marking ( , ) if, and only if, the corresponding transition ′ ( ) is enabled in the corresponding marking ∗. Also from Lemma 5.10 an object-autonomous firing mode ( , ) is enabled in a marking (26) (27) (28) (29) (30) (31) (32) (33) (34) ( , ) if, and only if, the corresponding transition is enabled in the corresponding marking ∗. Again, from Lemma 5.12 a synchronous firing mode ( ̂, 1, … , ) is enabled in a marking ( , ) if, and only if, the corresponding transition . ( ) is enabled in the corresponding ∗. Finally from Lemmas 5.8, 5.11 and 5.13, the generated markings in the 1-safe P/T-net can be mapped to the generated markings in the RS. □
Thus we have shown that every ERS can be transformed to behaviourally equivalent 1-safe P/T-net. Hence the standard analysis techniques for 1-safe P/T-net can be applied for ERS. 6
While general elementary object systems (EOS) come with some constraints that limit their expressiveness for automatic verification purposes, in this paper a modification that relaxes these constraints was given: elementary reference-net systems, ERS. Also, we proposed a set of rules for transforming ERS to behaviourally equivalent 1-safe P/T nest. Furthermore, we established an important relationship between the isomorphic properties of state spaces of 1-safe ERS and 1-safe P/T net. Among such results are the established Lemmas, and the proof of a theorem which relates the state space of 1-safe P/T nets 1-safe ERS. The definition of elementary reference-net system, ERS, targets practical relevance and the use of a partial order (unfolding) approach for dynamic analysis of EOS. In future work, we aim to compare an unfolding of the transformed 1-safe P/T to a direct unfolding of a 1-safe ERS without computing an intermediate expansion. Appendix A: Proof of Theorem 3.10
Proof. Let RS be a safe ERS. Let ∶= | ̂ |and ∶= {| | |( , ( . , ), ) ∈ } be the number of system net places and the maximum number of places present in an object net, respectively.
By definition of safe ERS each net token is 1-safe and hence there are at most 2 different markings a net-token may have. By definition of safe ERS each system net place is either marked or unmarked with a net-token with one of these markings, thus there are up to (1 + 2 ) different markings of RS, i.e. | ( )| ≤ (1 + 2 ) . □ Appendix B: Proof of Lemma 5.6
Proof: An initial marking of a system net in an ERS can be expressed by 0 = 0( ̂), ∀ ̂∈ ̂ . By Rule 2, ( ̂, ) ∈ ∗∗ in the P/T-net has one token in the corresponding initial marking 0∗( ̂, ), therefore 0∗( ̂, ) = 0( ̂).
From Def. 5.1, ̂( 0∗)( ̂, ) becomes ̂( 0∗)( ̂, ) = 0( ̂) = 0( ̂) □ Appendix C: Proof of Lemma 5.7
Proof: (⇒) Suppose that ′ ( ) ∈ ∗ is a transition that represents an autonomous transition in the P/T- net then ( ̂, ) ∈ ̂ is a corresponding transition in the system net. From ∗[ ′ ( ) > and Def. 2.3, each place has at least ∗ (( ̂, ), ′ ( )) tokens namely for each place ( ̂, ) ∈ ∗∗, the following inequality holds: ∗(( ̂, )) ≥ ∗ (( ̂, ), ′ ( )) .
Since = ̂( ∗), the number of token in place ( ̂, ) equals the number of tokens in place ̂∈ ̂ of a system net ̂ : ∗(( ̂, )) = ( ̂) .
From Rule 3, the weight of the arc from ( ̂, ) to ′ ( ) equals number of variables on the arc from ̂to ̂under the binding : ∗ (( ̂, ), ′ ( )) = ( ( ̂, ̂)) .
From (35), (36) & (37), for each place ̂∈ ̂ the following holds: ( ̂) ≥ ( ( ̂, ̂)) .
From Def. 3.5, [( ̂, ) >.
(⟸)(38) holds since [( ̂, ) >; (36) & (37) also hold. Therefore, (35) holds. From Def. 2.3, ∗[ ′ ( ) > (35) (36) (37) (38) Appendix D: Proof of Lemma 5.8
2∗ is expressed as follows: 2∗( ̂, ) = 1∗( ̂, )− ∗ (( ̂, ), ′ ( )) + ∗ ( ′ ( ),( ̂, )) .
Since 1 = ̂( 1∗), (30) holds. Similarly to (31), it holds that ∗ ( ′ ( ),( ̂, )) = ( ( ̂, ̂)) .
Therefore: 2∗( ̂, ) = 1( ̂)− ( ( ̂, ̂)) + ( ( ̂, ̂)). (See Def. 3.5& 36) (41) Finally it holds that 2 = ̂( 2∗)because (41) holds for each place.
Appendix E: Proof of Lemma 5.9
Proof: An initial marking of an object net in an ERS can be expressed by 0 = 0( ),∀ ∈ , ∈ ℝ hold. Rule 2 says that place ( , ) ∈ ∗∗ in the P/T-net has one token in the corresponding initial marking 0∗( , ), therefore 0∗( , ) = 0( ).
From Def. 5.2, ( 0∗)( , ) becomes ( 0∗)( , ) = 0( ) □ Appendix F: Proof of Lemma 5.10
Proof: (⇒) Suppose that ∈ ∗ is a transition that represents an autonomous transition in the P/T- net then ( , ) ∈ is a corresponding transition in the object net. From ∗[ > and the Def. 2.3, each place has at least (( , ), ) tokens ∗ namely for each place ( , ) ∈ ∗∗, the following inequality holds: ∗(( , )) ≥ ∗ (( , ), ). ∗(( , )) = ( ). to ∗ (( , ), ) = ( , ). ( ) ≥ ( , ).
From Def. 4.6, [( , ) >. (39) (40)
□ (42) (43) (44) (45)
Since = ( ∗), the number of tokens in( , ) equals the number of tokens in ∈ of an object net :
(⟸)(45) holds since [( , ) >; (43) & (44) also hold. Therefore, (42) holds. From Def.2.3, ∗[ > . □ 2∗ is expressed as follows: 2∗( , ) = 1∗( , ) − ∗ (( , ), ) +
∗ ( , ( , )) .
Since 1 = ( 1∗), (43) holds. Similarly to (44), it holds that ∗ ( , ( , )) = ( , ) .
Finally it holds that 2 = ( 2∗) because (46) holds for each place. Appendix H: Proof of Lemma 5.12
For ( 1, … , ) it can be proven in a similar to Lemma 5.10 for each net-token ∀ ̂∈ ⦁ ̂: ( ̂) ≥ ( ( ̂, ̂)) . transition ∈ that ∀ ∈ ⦁ : 1( ) ≥ ( , ) .
(⟸) For . ( ) ∈ lar way to Lemma 5.7 that
∗ ∀( ̂, ) ∈ ′ ∗: 1∗(( ̂, )) ≥ ∗(( ̂, ), ̂) . (46) (47) (48) □ (49) (50) (51) (52) □
From Rule 5, and equations (48) and (49) it holds that ( 1, 1)[ >.
which is added in Rule 5, it can be shown that in a simiSimilarly, it can be shown from Lemma 5.10 for ∈ that participate in . ( ) ∈