=Paper=
{{Paper
|id=Vol-1698/CS&P2016_09_Abdullahi&Mueller_Towards-Efficient-Verification-of-Elementary-Object-Systems
|storemode=property
|title=Towards Efficient Verification of Elementary Object Systems
|pdfUrl=https://ceur-ws.org/Vol-1698/CS&P2016_09_Abdullahi&Mueller_Towards-Efficient-Verification-of-Elementary-Object-Systems.pdf
|volume=Vol-1698
|authors=Ismaila Jihad Abdullahi,Berndt Müller
|dblpUrl=https://dblp.org/rec/conf/csp/AbdullahiM16
}}
==Towards Efficient Verification of Elementary Object Systems==
https://ceur-ws.org/Vol-1698/CS&P2016_09_Abdullahi&Mueller_Towards-Efficient-Verification-of-Elementary-Object-Systems.pdf
Towards Efficient Verification of Elementary Object
Systems
Ismaila Jihad Abdullahi, and Berndt Müller
University of South Wales
(Ismaila.abdullahi, bertie.muller) @southwales.ac.uk
Abstract. 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 veri-
fication feasible.
Keywords: Elementary Reference-net System, nets-within-nets, Petri nets,
isomorphic property, computational complexity
1 Introduction
Elementary Object Systems (EOS for short) are based on the nets-within-nets para-
digm of (Valk, 1991,2003) in which the nesting of nets involved in the model is re-
stricted to two levels and are generalised in (Köhler and Heitmann, 2009) for arbitrary
nesting structure. This formalism provides a modelling technique that allows tokens
of Petri nets to be Petri nets themselves, called object nets. Object nets are tokens with
internal structure and inner activity and have been applied in a variety of scenarios,
e.g., multi-agent systems.
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 for-
malists as shown in (Köhler and Rölke, 2004) and (Lomazova, and Schnoebelen,
1999). As in similar formalists, we have to distinguish autonomous and synchronous
transitions. The need for application of a partial order (unfolding) approach for dy-
namic analysis of EOS have encouraged and driven the development of this new for-
malism. We refer the reader to (Valk, 1991) for an introduction to the nets-within-
nets.
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 Fundamentals of Petri nets
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 pre-
set of a node 𝑥 ∈ 𝑃 ∪ 𝑇, denoted ⦁𝑥, is the set containing the elements that immedi-
ately 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 ena-
bled 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
̂ , Σ𝑚0 , ℓ, 𝓌, 𝑹𝟎 ) where
reference-net system is a tuple 𝑅𝑆 = (𝑁
𝑁̂ = (𝑃̂ , 𝑇,
̂ 𝐹̂ ) 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 sys-
tem 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 𝑎̂ ∈ (𝐹̂ ) adja-
cent 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 𝑹𝟎 (𝑝̂ ) ∈ ℕ ⟺
),
𝑹𝟎 (𝑝̂ ) ∈ {𝑁⦁ }.
In the example of Fig. 1 an 𝑅𝑆 = (𝑁 ̂ , Σ, ℓ, 𝓌, 𝑴𝟎 ) is shown, where Σ = {𝑁1 , 𝑁2 }.
̂
Arcs of 𝑁 can be identified by their labelling from 𝓌(𝑡̂). Hence {x, y,} can be bound
to marked named object nets in places ̂𝑝1 𝑎𝑛𝑑 𝑝̂2 adjacent to transition ̂𝑡′ to enable
it. In the initial marking, places 𝑝̂1 𝑎𝑛𝑑 𝑝̂2 contain references to the marked named
object nets 𝑁1 𝑎𝑛𝑑 𝑁2 respectively.
We denote by 𝒩 = {𝑖|(𝑖, 𝑁𝑖, , 𝑚𝑖 ) ∈ Σ}, 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. Con-
dition (2) says that each variable appearing in the outgoing arc of a system net transi-
tion 𝑡̂ 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 abil-
ity to describe nesting of object nets, synchronisation, and mobility, but does not al-
low 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 physi-
cal entities
Fig. 1. An example of an ERS
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 varia-
bles on arcs adjacent to 𝑡̂. A binding 𝛽 specifies which variables are bound to names,
where 𝛽: 𝓌(𝑡̂) ∪ {•} ⟶ 𝒩 ∪ {𝑁⦁ }with 𝒩 = {𝑖|(𝑖, 𝑁𝑖, , 𝑚𝑖 ) ∈ Σ} satisfying the condi-
tions: 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 ele-
mentary 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 (𝑹, 𝑴)
̂ (𝛽(𝓌(𝑝̂ , 𝑡̂)), 𝑁𝛽(𝓌(𝑝̂,𝑡̂)) , 𝑚𝛽(𝓌(𝑝̂,𝑡̂)) ) ∈ 𝑹(𝑝̂ ) and
if: ∀ ̂𝑝 ∈ 𝑃:
∀𝑝 ∈ 𝑃𝑖 ∶ Π𝑖 (𝑴) ≥ 𝐹𝑖 (𝑝, 𝑡𝑖 ),. (5)
This is denoted by (𝑹, 𝑴)[𝑡̂, 𝑡𝑖 > Let be 𝑚𝑖 [𝑡𝑖 > 𝑚′𝑖 (w.r.t 𝑁𝑖 ). The successor
marking (𝑹′, 𝑴′) is defined by
𝑹′(𝑝̂) = 𝑹(𝑝̂ )\ (𝛽(𝓌(𝑝̂ , 𝑡̂)), 𝑁𝛽(𝓌(𝑝̂,𝑡̂)) , 𝑚𝛽(𝓌(𝑝̂,𝑡̂)) ) ∪
(𝛽(𝓌(𝑡̂, 𝑝̂ )), 𝑁𝛽(𝓌(𝑡̂,𝑝̂)) , 𝑚𝛽(𝓌(𝑡,̂𝑝̂)) ) : ∀𝑝̂ ∈ 𝑃̂ and
𝑴′ = 𝑴𝒊→𝒎𝒊 . (6)
This is denoted by (𝑅, 𝑀)[𝒕̂, 𝒕𝒊 > (𝑹′ , 𝑴′ ).
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 𝑡̂ 𝑖𝑠 ac-
tivated in (𝑹, 𝑴) if there is a net token such that:
(𝛽(𝓌(𝑝̂ , 𝑡̂)), 𝑁𝛽(𝓌(𝑝̂,𝑡̂)) , 𝑚𝛽(𝓌(𝑝̂,𝑡̂)) ) ∈ 𝑹(𝑝̂ )∀𝑝̂ ∈ 𝑃̂ . (7)
Since we use 𝜏, for in action, this is denoted by (𝑹, 𝑴)[( 𝑡̂, 𝜏) >. The successor
marking (𝑹′ , 𝑴′ )is defined by
∀𝑝̂ ∈ 𝑃̂ ∶ 𝑹′(𝑝̂ ) = 𝑹(𝑝̂ )\ (𝛽(𝓌(𝑝̂ , 𝑡̂)), 𝑁𝛽(𝓌(𝑝̂,𝑡̂)) , 𝑚𝛽(𝓌(𝑝̂,𝑡̂)) ) ∪ (𝛽(𝓌(𝑡̂, 𝑝̂ )), 𝑁𝛽(𝓌(𝑡̂,𝑝̂)) , 𝑚𝛽(𝓌(𝑡,̂𝑝̂)) )
𝑴′ = 𝑴 . (8)
This is denoted by (𝑹. 𝑴)[(𝑡1̂ , 𝜏) > (𝑹′ , 𝑴′ ).
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 (𝑹, 𝑴) (denot-
ed(𝑹, 𝑴)[(𝜏̂ , 𝑡𝑖 ) >]. The successor marking (𝑹′, 𝑴′) of RS is defined by
𝑹′ = 𝑹 and
𝑴′ = 𝑴1→mi if 𝑚𝑖 [ 𝑡𝑖 > 𝑚′𝑖 for Π𝑖 (𝑴) = 𝑚𝒊 . (9)
We denote this by (𝑹, 𝑴)[(𝜏̂ , 𝑡𝑖 ) > (𝑹′, 𝑴′).
To introduce the occurrence sequences for 𝐸𝑅𝑆 we assume an 𝐸𝑅𝑆 as defined in
Definition 3.2. Let 𝑅𝑆 be an 𝐸𝑅𝑆𝑎𝑛𝑑(𝑹, 𝑴), (𝑹′ , 𝑴′ ) ∈ ℳ𝑟 .
Definition 3.7 For a new alphabet Γ ≔ (𝑇̂ ∪ {𝜏̂ }) × (𝑇1 ∪ {𝜏}) ×, … , (𝑇𝑘 ∪ {𝜏})\
(𝜏̂ , 𝜏, … , 𝜏)where (𝜏̂ , 𝜏, … , 𝜏) denotes the neutral element of Γ ∗ , we define:
(𝑹, 𝑴)[(𝜏̂ , 𝜏, … , 𝜏) > (𝑹′ , 𝑴′) if (𝑹, 𝑴) = (𝑹′ , 𝑴′) and
̆ (𝑡̂ , 𝛼) > (𝑹′ , 𝑴′ ) 𝑖𝑓 ∃(𝑹′′ , 𝑴′′ ) ∶ (𝑹, 𝑴)[𝑤
(𝑹, 𝑴)[𝑤 ̆ > (𝑹′′ , 𝑴′′ ) 𝑎𝑛𝑑
̆ ∈ Γ ∗ , 𝑡̂, ∈ 𝑇̂ ∪ {𝜏̂ } 𝑎𝑛𝑑 𝛼 ∈ ((𝑇1 ∪ {𝜏}) × , … , (𝑇𝑘 ∪ {𝜏}). ( 10)
(𝑹′′ , 𝑴′′ )[(𝑡̂ , 𝛼) > (𝑅 ′ , 𝑀′ ) 𝑓𝑜𝑟 𝑠𝑜𝑚𝑒 𝑤
To denote that (𝑹′, 𝑴′) is reachable from (𝑹, 𝑴) by some occurrence sequence of
∗
actions we write (𝑹, 𝑴) → (𝑹′ , 𝑴′ ).
The set of reachable markings of a reference system RS from a marking (𝑹, 𝑴) is
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 condi-
tions 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 mark-
ings there is at most one net-token on each system net place and each net-token is 1-
safe i.e.,:
∀(𝑹, 𝑴) ∈ 𝑅(𝑅𝑆), ∀𝑝̂ ∈ 𝑃̂ : (𝑅(𝑝̂ ), ) ≤ 1 and
∀(𝑖, 𝑁𝑖 , 𝑚𝑖 ) ∈ 𝑹(𝑝̂ ):∀𝑝𝑖 ∈ 𝑃𝑖 ∶ ∀𝑝̂ ∈ 𝑃̂ (𝑹(𝑝̂ ), Π𝑖 (𝑴(𝑝𝑖 )) > 0 ⟹ Π𝑖 (𝑴(𝑝𝑖 )) ≤ 1.
Observation 3.9: Given an ERS if for all reachable markings there is at most one
token on each system net place and each net-token is 1-safe, then all reachable mark-
ings are 1-safe.
Theorem 3.10 If an ERS is safe, then its set of reachable markings is finite. The
proof to this theorem is presented in appendix A.
4 Transformation of ERS into P/T- nets
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 (Miyamoto & Horiguchi, 2013; Lomazova & Erma-
kova, 2016). We highlight the similarities and differences between the proposed ap-
proach and these related studies. Miyamoto and Horiguchi present a translation tech-
nique for transforming classical Multi-Agent nets (MANs) into Modular Nets (MNs)
and show isomorphism of state spaces of both nets including the computational com-
plexity for transforming MAN into MNs. The major similarities between our work
and that of (Lomazova&Ermakova, 2016) is that they developed a set of rules for
translating a safe conservative nested Petri net (NP-net) into an equivalent P/T net.
The main differences are that we established clearly an important relation between the
isomorphic properties of state space of safe-ERS and a 1-safe P/T net. Among such
results are the establish Lemmas, and proof of a theorem for the isomorphism. More-
over, we adopt a different way of introducing the procedure for transforming nets-
within-nets into 1-safe P/T net, which consequently give a neater and easier-to-
understand presentation.
4.1 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 net-
token 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} . (11)
𝑃𝑁∗ 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:
𝑃𝑁∗ ≔ ⋃𝑖∈Σ𝑛𝑡 {(𝑝𝑖 , 𝑖)|𝑝𝑖 ∈ 𝑃𝑖 , 𝑖 ∈ ℝ, 𝑖 ≥ 1} . (12)
Therefore the set 𝑃𝑁∗ ∗ of a target P/T-net 𝑁 ∗ as shown in Fig.2 is the union of these
set, namely
𝑃𝑁∗ ∗ ≔ 𝑃′ 𝑁∗ ∪ 𝑃𝑁∗ . (13)
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 generat-
ed places from 𝑃𝑁∗ ∗ . If a net-token with name 𝑖 ∈ ℝ𝑖 resides in a place 𝑝̂ in an initial
marking 𝑅0 (𝑝̂ ) of the system net, then a black token in placed on (𝑝̂ , 𝑖) ∈ 𝑃𝑁∗ ∗ as the
initial marking 𝑀0∗ of the constructed, namely
𝑀0∗ (𝑝̂ , 𝑖) = 𝑅0 (𝑝̂ ). (14)
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
on (𝑝̂ , 𝑖) ∈ 𝑃𝑁∗ ∗ in 𝑀0∗ ,namely
𝑀0∗ (𝑝, 𝑖) = 𝑀 0 (𝑝). (15)
Fig. 2. Set of places of P/T net Fig 3: initial marking
If a place in the system net is a place that contains a black token, then the unique
copy corresponding to the place in 𝑁 ∗ is also marked with a black token. In the given
ERS, reference to the net-token 𝑁1 resides in 𝑝̂1 , and reference to the net-token re-
sides in ̂𝑝2 . Hence, we have tokens in (𝑝′1 , 1) and(𝑝′2 , 2) for 𝑁 ∗ . Likewise, we define
the markings for places (𝑝1 , 1) and (𝑝1 , 2). This is illustrated in Fig.3 above.
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)
In the example ERS, the set 𝑤(𝑡̂) of input arc variables that can be bound to a
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.
∗
We define a set 𝐹𝑠𝑎𝑡 of arcs for system autonomous transitions in 𝑁 ∗ as follows:
∗
𝐹𝑠𝑎𝑡 = ⋃𝑎̂∈𝐹̂ {(𝑥′ , 𝑦 ′ |(𝑥, 𝑦) = 𝓌(𝑎̂), 𝑥 ′ ∈ 𝑃′ 𝑁∗ (𝑥) ∪ 𝑇𝑠𝑎𝑡
∗ (𝑥), ′
𝑦 ∈ 𝑃′ 𝑁∗ (𝑦) ∪
∗ (𝑦)}
𝑇𝑠𝑎𝑡 . (18)
Rule 4: Generate a family of transitions representing autonomous transitions in
∗
each net-token. For a set 𝑇𝑛𝑎𝑡 of transitions of 𝑁 ∗ we define a set of similar autono-
mous transitions as follows.
Fig. 4. Transitions and arcs from Rule 3 Fig. 5, Transitions and arcs after Rule 4
∗
𝑇𝑛𝑎𝑡 ≔ ⋃𝑖∈Σ𝑛𝑡 {𝑡|𝑡𝑖 ∈ 𝑇𝑖 ∧ 𝑡𝑖 𝑖𝑠 𝑎𝑛 𝑜𝑏𝑗𝑒𝑐𝑡 𝑎𝑢𝑡𝑜𝑛𝑜𝑚𝑜𝑢𝑠 𝑡𝑟𝑎𝑛𝑠𝑖𝑡𝑖𝑜𝑛} . (19)
∗
We define a set 𝐹𝑛𝑎𝑡 of arcs of net-token autonomous transitions in 𝑁 ∗ as follows:
∗ ∗
𝐹𝑛𝑎𝑡 = {(𝑝, 𝑖), 𝑡) ∈ 𝑃𝑁∗ × 𝑇𝑛𝑎𝑡 |(𝑝, 𝑡) ∈ 𝐹𝑖 > 0} ∪
∗
{(𝑡, (𝑝. 𝑖) ∈ 𝑇𝑛𝑎𝑡 × 𝑃𝑁∗ |(𝑡, 𝑝) ∈ 𝐹𝑖 > 0} . (20)
This is depicted in Fig.5.
Rule 5: Generate a family of transitions representing synchronisation transitions
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/T-
net 𝑁 ∗ 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.
∗
𝑇𝑠𝑦𝑛𝑐𝑖
≔ ⋃𝑘𝑖=1{𝑡𝑖.𝛽𝑖 (𝑥) = {𝑡̂, 𝑡1 , … , 𝑡𝑘 }|𝑥 ∈ 𝑤(𝑡̂), 𝑡̂ ∈ 𝑇̂, 𝑡1 ∈ 𝑇1 , … , 𝑡𝑘 ∈ 𝑇𝑘 } . (21)
In our example two places 𝑝̂1 𝑎𝑛𝑑 𝑝̂2 are marked with one net-token each in the in-
itial marking. We add two transitions 𝑡1 = {{𝑡1̂ , 𝑡21 , 𝜏} and 𝑡2 = {𝑡1̂ , 𝜏, 𝑡22 } annotated
with @1 and @2, which is shown in Fig.6. The result of transforming ERS into P/T-
net is shown in Fig. 7.
Fig. 6. Synchronous firing transitions and arcs Fig. 7. Result of transforming ERS
5 Isomorphic Properties of the State Spaces
We establish an isomorphism between the states of an ERS and the generated 1-
safe 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:
∗ ∗ ∗
Tsat , Tnat , and Tsync i
from Rule 3, Rule 4 and Rule 5 respectively in N ∗ . In the fol-
lowing, we define some mappings from the P/T-net to and ERS.
Definition 5.1 A mapping 𝑓̂ maps a marking 𝑀∗ of a P/T-net 𝑁 ∗ from the set of
places 𝑃̂ to markings 𝑅 of a system net of an ERS as follows:
𝑓̂(𝑀∗ )(𝑝̂ , 𝑖) = 𝑅(𝑝̂ ) 𝑠𝑢𝑐ℎ 𝑡ℎ𝑎𝑡 (𝑝̂ , 𝑖) ∈ 𝑃𝑁∗ ∗ : 𝑝̂ ∈ 𝑃̂ : 𝑖 ∈ ℝ . (22)
Definition 5.2 A mapping 𝑓 maps a marking 𝑀∗ of a P/T-net 𝑁 ∗ from the set of
places 𝑃𝑖 of net-token 𝑖 of ERS to a marking 𝑀 of a net-token of ERS as follows:
𝑓(𝑀∗ )(𝑝, 𝑖) = 𝑀(𝑝) 𝑠𝑢𝑐ℎ 𝑡ℎ𝑎𝑡 (𝑝, 𝑖) ∈ 𝑃𝑁∗ ∗ : 𝑝 ∈ 𝑃𝑖 : 𝑖 ∈ ℝ . (23)
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:
𝑔̂(𝑡 ′𝛽𝑖(𝑥) ) = (𝑡̂, 𝜏) . (24)
𝑤ℎ𝑒𝑟𝑒 𝛽𝑖 (𝑥) is a binding function that binds a variable 𝑥 ∈ 𝑤(𝑡̂) on arcs adjacent
̂
to 𝑡 to an object net name.
∗
Definition 5.4 𝑔 is a function that maps a transition 𝑡 ∈ 𝑇𝑛𝑎𝑡 of P/T-net 𝑁 ∗ to
an object-autonomous firing mode (𝜏, 𝑡𝑖 ) ∉ 𝑑𝑜𝑚(ℓ) of an ERS as follows:
𝑔(𝑡) = (𝜏, 𝑡𝑖 ) . (25)
∗
Definition 5.5 𝑔𝑠 is a mapping function that maps a transition 𝑡𝑖.𝛽𝑖 (𝑥) ∈ 𝑇𝑠𝑦𝑛𝑐 𝑖
of
P/T-net 𝑁 to a synchronisation firing mode (𝑡̂, 𝑡1 , … , 𝑡𝑘 ) ∈ ℓ of an ERS as follows:
∗
𝑔𝑠 (𝑡𝑖.𝛽𝑖(𝑥) ) = {(𝑡̂, 𝑡1 , … , 𝑡𝑘 )} . (26)
̂ and 𝑁 ∗ constructed by Rules 1 to 5, hold.
The following lemmas related to 𝑁
̂ level, the following equality holds:
Lemma 5.6 For the initial marking at 𝑁
𝑅0 (𝑝̂ ) = 𝑓̂ (𝑀0∗ )(𝑝̂ , 𝑖) . (27)
Lemma 5.7 Suppose that 𝑅 = 𝑓 ̂(𝑀∗ ) and(𝑡̂, 𝜏) = 𝑔̂(𝑡 ′𝛽𝑖 (𝑥) ). The following propo-
sition holds:
𝑀∗ [𝑡 ′𝛽𝑖(𝑥) > ⇔ 𝑅[(𝑡̂, 𝜏) > . (28)
Lemma 5.8 Suppose that 𝑅1 = 𝑓̂(𝑀1∗ ), 𝑀1∗ [𝑡 ′𝛽𝑖(𝑥) > 𝑀2∗ , and 𝑅1 [𝑔̂(𝑡 ′𝛽𝑖(𝑥) ) > 𝑅2 .
The following equality holds: 𝑅2 = 𝑓̂ (𝑀2∗ ) . (29)
Lemma 5.9 For the initial marking of the object net, the following holds:
𝑀0 (𝑝) = 𝑓(𝑀0∗ )(𝑝, 𝑖) . (30)
Lemma 5.10 Suppose that 𝑀 = 𝑓(𝑀∗ ) and(𝜏, 𝑡𝑖 ) = 𝑔(𝑡). The following proposi-
tion holds:
𝑀∗ [𝑔(𝑡) > ⇔ 𝑀[((𝜏, 𝑡𝑖 )) > . (31)
Lemma 5.11 Suppose that 𝑀1 = 𝑓(𝑀1∗ ), 𝑀1∗ [𝑡 > 𝑀2∗ , and 𝑀1 [𝑔(𝑡) > 𝑀2 . The fol-
lowing equality holds:
𝑀2 = 𝑓(𝑀2∗ ) . (32)
Lemma 5.12 Suppose that (𝑅1, 𝑀1 ) = 𝑓𝑠 (𝑀1∗ ) and 𝑡𝑠 = 𝑔𝑠 (𝑡𝑖.𝛽𝑖 (𝑥) ). The following
proposition holds:
𝑀1∗ [𝑔𝑠 (𝑡𝑖.𝛽𝑖(𝑥) ) > ⇔ (𝑅1 , 𝑀1 )[𝑡𝑠 > . (33)
Lemma 5.13 Suppose(𝑅1 , 𝑀1) = 𝑓𝑠 (𝑀1∗ ), 𝑀1∗ [𝑡𝑖.𝛽𝑖(𝑥) > 𝑀2∗ and (𝑅1, 𝑀1)[𝑔𝑠 (𝑡𝑖.𝛽𝑖(𝑥) ) > (𝑅2 , 𝑀2 ) .
The following equality holds:
(𝑅2 , 𝑀2 ) = 𝑓𝑠 (𝑀2∗ ) . (34)
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 mark-
ings of the 1-safe P/T-net 𝑁 ∗ and the initial marking in RS. From Lemma 5.7 a sys-
tem-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
(𝑅, 𝑀) 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 gener-
ated 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 equiva-
lent 1-safe P/T-net. Hence the standard analysis techniques for 1-safe P/T-net can be
applied for ERS.
6 Conclusion
While general elementary object systems (EOS) come with some constraints that
limit their expressiveness for automatic verification purposes, in this paper a modifi-
cation that relaxes these constraints was given: elementary reference-net systems,
ERS. Also, we proposed a set of rules for transforming ERS to behaviourally equiva-
lent 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 unfold-
ing of the transformed 1-safe P/T to a direct unfolding of a 1-safe ERS without com-
puting an intermediate expansion.
References
Köhler, M. and Heitmann, F., 2009. On the expressiveness of communication
channels for object nets. Fundamenta Informaticae, 93(1-3), pp.205-219.
Köhler, M. and Rölke, H., 2004. Properties of object Petri nets. In Applications and
Theory of Petri Nets 2004 (pp. 278-297). Springer Berlin Heidelberg.
Lomazova, I.A. and Schnoebelen, P., 1999, July. Some decidability results for
nested Petri nets. In Perspectives of System Informatics (pp. 208-220). Springer Ber-
lin Heidelberg.
Lomazova, I.A. and Ermakova, V.O., 2016 Verification of Nested Petri Nets Using
an Unfolding Approach.
Miyamoto, T. and Horiguchi, K., 2013. Modular reachability analysis of Petri nets
for multiagent systems. IEEE Transactions on Systems, Man, and Cybernetics: Sys-
tems, 43(6), pp.1411-1423.
Valk, R., 1991. Modelling concurrency by task/flow EN systems. In 3rd Workshop
on Concurrency and Compositionality (Vol. 191).
Valk, R., 2003. Object Petri nets: Using the nets-within-nets paradigm, Advanced
Course on Petri Nets 2003 (J. Desel, W. Reisig, G. Rozenberg, Eds.), 3098.
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 corre-
sponding 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 autono-
mous 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:
𝑀∗ ((𝑝̂ , 𝑖)) ≥ 𝑊𝑠𝑎𝑡
∗
((𝑝̂ , 𝑖), 𝑡 ′𝛽𝑖(𝑥) ) . (35)
Since 𝑅 = 𝑓̂(𝑀∗ ), the number of token in place (𝑝̂ , 𝑖) equals the number of tokens
in place 𝑝̂ ∈ 𝑃̂ of a system net 𝑁
̂:
𝑀∗ ((𝑝̂ , 𝑖)) = 𝑅(𝑝̂ ) . (36)
From Rule 3, the weight of the arc from (𝑝̂ , 𝑖) to 𝑡 ′𝛽𝑖 (𝑥) equals number of variables
on the arc from 𝑝̂ to 𝑡̂ under the binding 𝛽:
∗
𝑊𝑠𝑎𝑡 ((𝑝̂ , 𝑖), 𝑡 ′𝛽𝑖(𝑥) ) = 𝛽(𝑤(𝑝̂ , 𝑡̂)) . (37)
From (35), (36) & (37), for each place 𝑝̂ ∈ 𝑃̂ the following holds:
𝑅(𝑝̂ ) ≥ 𝛽(𝑤(𝑝̂ , 𝑡̂)) . (38)
From Def. 3.5, 𝑅[( 𝑡̂, 𝜏) >.
(⟸)(38) holds since 𝑅[( 𝑡̂, 𝜏) >; (36) & (37) also hold. Therefore, (35) holds.
From Def. 2.3, 𝑀∗ [𝑡 ′𝛽𝑖(𝑥) >
Appendix D: Proof of Lemma 5.8
Proof: From Def. 2.3, the number of tokens in place (𝑝̂ , 𝑖) in a successor marking
𝑀2∗ is expressed as follows:
𝑀2∗ (𝑝̂ , 𝑖) = 𝑀1∗ (𝑝̂ , 𝑖) − 𝑊𝑠𝑎𝑡
∗
((𝑝̂ , 𝑖), 𝑡 ′𝛽𝑖(𝑥) ) + 𝑊𝑠𝑎𝑡
∗
(𝑡 ′𝛽𝑖(𝑥) , (𝑝̂ , 𝑖)) . (39)
Since 𝑅1 = 𝑓̂(𝑀1∗ ), (30) holds. Similarly to (31), it holds that
∗
𝑊𝑠𝑎𝑡 (𝑡 ′𝛽𝑖(𝑥) , (𝑝̂ , 𝑖)) = 𝛽(𝑤(𝑡̂, 𝑝̂ )) . (40)
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:
𝑀∗ ((𝑝, 𝑖)) ≥ 𝑊𝑛𝑎𝑡
∗
((𝑝, 𝑖), 𝑡) . (42)
Since 𝑀 = 𝑓(𝑀∗ ), the number of tokens in(𝑝, 𝑖) equals the number of tokens in
𝑝 ∈ 𝑃𝑖 of an object net 𝑁𝑖 :
𝑀∗ ((𝑝, 𝑖)) = 𝑀(𝑝) . (43)
From Rule 4, the weight of the arc from (𝑝, 𝑖) to 𝑡 equals the weight of the arc from
𝑝𝑖 to 𝑡𝑖
∗
𝑊𝑛𝑎𝑡 ((𝑝, 𝑖), 𝑡) = 𝑊𝑖 (𝑝𝑖 , 𝑡𝑖 ) . (44)
From (40) and (41), for each place 𝑝 ∈ 𝑃𝑖 the following inequality holds:
𝑀(𝑝) ≥ 𝑊𝑖 (𝑝𝑖 , 𝑡𝑖 ) . (45)
From Def. 4.6, 𝑀[(𝜏, 𝑡𝑖 ) >.
(⟸)(45) holds since 𝑀[(𝜏, 𝑡𝑖 ) >; (43) & (44) also hold. Therefore, (42) holds.
From Def.2.3, 𝑀∗ [𝑡 > . □
Appendix G: Proof of Lemma 5.11
Proof: From Def. 2.3.2, the number of tokens in place (𝑝, 𝑖) in a successor marking
𝑀2∗ is expressed as follows:
𝑀2∗ (𝑝, 𝑖) = 𝑀1∗ (𝑝, 𝑖) − 𝑊𝑛𝑎𝑡
∗ ∗
((𝑝, 𝑖), 𝑡) + 𝑊𝑛𝑎𝑡 (𝑡, (𝑝, 𝑖)) . (46)
Since 𝑀1 = 𝑓(𝑀1∗ ), (43) holds. Similarly to (44), it holds that
∗
𝑊𝑛𝑎𝑡 (𝑡, (𝑝, 𝑖)) = 𝑊𝑖 (𝑝𝑖 , 𝑡𝑖 ) . (47)
Therefore, the following equation holds:
𝑀2∗ (𝑝, 𝑖) = 𝑀1 (𝑝𝑖 ) − 𝑊𝑖 (𝑝𝑖 , 𝑡𝑖 + 𝑊𝑖 (𝑡𝑖 , 𝑝𝑖 ) = 𝑀2∗ (𝑝, 𝑖) (See Def. 3.6) (48)
Finally it holds that 𝑀2 = 𝑓(𝑀2∗ ) because (46) holds for each place. □
Appendix H: Proof of Lemma 5.12
Proof: (⇒) For 𝑡̂, it can be proved in a similar way to Lemma 5.7 that
∀𝑝̂ ∈ ⦁𝑡̂: 𝑅(𝑝̂ ) ≥ 𝛽(𝑤(𝑡̂, 𝑝̂ )) . (49)
For (𝑡1 , … , 𝑡𝑘 ) it can be proven in a similar to Lemma 5.10 for each net-token
transition 𝑡𝑖 ∈ 𝑇𝑖 that
∀𝑝𝑖 ∈ ⦁𝑡𝑖 : 𝑀1 (𝑝𝑖 ) ≥ 𝑊𝑖 (𝑝𝑖 , 𝑡𝑖 ) . (50)
From Rule 5, and equations (48) and (49) it holds that (𝑅1 , 𝑀1 )[𝑡𝑠 >.
∗
(⟸) For 𝑡𝑖.𝛽𝑖 (𝑥) ∈ 𝑇𝑠𝑦𝑛𝑐𝑖
which is added in Rule 5, it can be shown that in a simi-
lar way to Lemma 5.7 that
∀(𝑝̂ , 𝑖) ∈ 𝑃′ 𝑁∗ : 𝑀1∗ ((𝑝̂ , 𝑖)) ≥ 𝑊 ∗ ((𝑝̂ , 𝑖), 𝑡̂) . (51)
Similarly, it can be shown from Lemma 5.10 for 𝑡𝑖 ∈ 𝑇𝑖 that participate in 𝑡𝑖.𝛽𝑖(𝑥) ∈
∗
𝑇𝑠𝑦𝑛𝑐𝑖
that
∀(𝑝𝑖 , 𝑖) ∈ 𝑃𝑁∗ : 𝑀1∗ (𝑝𝑖 , 𝑖) ≥ 𝑊𝑛𝑎𝑡
∗ (𝑝
𝑖 , 𝑡𝑖 ). (52)
The action (𝑡̂, 𝑡1 , … , 𝑡𝑘 ) share no input places by assumption in Rule 1. From
Def. 2.3, (51) & (52): 𝑀1∗ [𝑡𝑖.𝛽𝑖(𝑥) > . □
Appendix I: Proof of Lemma 5.13
Proof: It can be proved in a similar way to Lemma 5.8 and 5.11 by Def. 2.3, and
Rules 3 & 4. □