Under consideration for publication in Formal Aspects of Computing

Extensional Petri Net
Xiaoju Dong1 , Yuxi Fu1 and Daniele Varacca2
1 BASICS, Department of Computer Science, Shanghai Jiao Tong University, Shanghai, China
2 PPS - CNRS & Université Paris Diderot, Paris, France

Abstract. Petri nets form a concurrent model for distributed and asynchronous systems. They are capable ofmodeling information flow in a closed system, but are generally not suitable for the study of compositionality.
We address the issue of Petri net compositionality by introducing extensional Petri nets. In an extensional
Petri net some places are external while others are internal. Every external place is labeled by a distinguishedinterface name. When composing two extensional Petri nets two places with a same label are coerced. An
external place can be turned into an internal place by applying localization operator. The paper takes a lookat bisimulation semantics and observational properties of the extensional Petri nets.
Keywords: Petri Net, Compositionality, Bisimulation

1. Introduction
Petri nets [Per81] form a model for concurrency and causality. They are best in describing information
flows in closed isolated hardware systems. It is well-known that Petri net theory lacks of a good notion ofcompositionality. Without compositionality it is difficult to apply Petri nets to study the dynamic aspectof mobile and distributed computing systems. In modern computing everything is connected. Systems arewidely distributed and highly concurrent. A system is bound to interact with environments in one way or
another. The demand for compostionality is stronger than ever. In real applications Petri nets tend to bevery large and very complex. The design of huge Petri nets is managed by designing smaller components,
and then sticking the components through interfaces to form larger Petri nets. A notion of composition isalready there in this design methodology. Accordingly the analysis of the property of the large Petri nets
can be carried out by analyzing the local property of the component Petri nets and then obtain the global
property by additional analysis. This is an obvious effective way to control the complexity of the analysisof large systems. In summary for both practical and theoretical purposes Petri nets are best seen as open
systems [Hao97] that can be built up and analyzed in a structural manner. In this paper we formalize theplace-transition nets so that they are open systems.
Interactions always occur at interfaces. In process calculi the interfaces are channels. Two processes
may communicate when they are connected to the two ends of a channel. To compose Petri nets we need
Correspondence and offprint requests to: Yuxi Fu, Department of Computer Science, Shanghai Jiao Tong University, 800
Dongchuan Road, Shanghai 200240, China. e-mail: fu-yx@sjtu.edu.cn

2

X. Dong, Y. Fu and D. Varacca

to pin down the interfaces. In literature there are different ways to define composition [Aal05, BDK01,
BDK2001, BuG95, BuG09, CWY04, DKK04, DNM88, FuL10, Fuy16, GHH08, Gol90, Nie87, YCX07]. Thereis a synchronization approach that allows transitions from different nets to be performed as a single action.
There is a shared memory approach that identifies places of different nets. There is a research line thatcombines the Petri net theory and the process algebraic theory, aiming at a unified framework of both.
There is also proposal that defines composition by categorical pushout.
Systems are composed because they have to interact. In literature there are two ways to define interactions
between nets. In transition based cooperations two or more transitions from different component nets aresynchronised at correlated transition labels. Synchronization is achieved in a most direct fashion. This isapparently very much influenced by the interaction mechanism of CCS [Mil89]. In place based scenario
nets are composed by coercing certain places from different nets. There is real information flow between
component nets, achieving the effect of message sharing mechanism. There are several variations in thissetup. The open Petri nets introduced by Baldan et. al. [BBG09, BCE01, BCE05, BCE07, BCE08] aredifferent from the variant proposed by [LJZ13]. In such nets some places with labels, called open or external,
are considered as interfaces with environments. Among the external places, some are input places, others
are output places. An external place can be both an input and an output one at the same time. This could
be distinguished by introducing dangling arcs attached to the places. In addition to external places, there
are synchronization transitions. When two nets are composed, the connections of transitions to their pre-set
and post-set should be preserved. New connections cannot be added. In the larger net, a new arc may be
attached to a place only if the corresponding place of the subnet has a dangling arc in the same direction.
Dangling arcs may be removed, but cannot be added in the larger net. Baldan et. al studied the denotationalsemantics of such open nets. Finally there are of course hybrid models that have both transition based andplace based features at the expanse of complicated syntax and semantics.
The configuration of a Petri net is fixed, whereas that of a process, say a CCS process, is dynamic. Thatcompares well to the difference between hardware and software. The advantage of fixed configurations is thatthey are subject to investigations using combinatorial (graph theoretical) tools and linear algebra. On theother hand the success of process algebra is that they offer an observational theory for interaction, without
which one cannot talk about any theory for composition. Our motivation in this paper is to redefine Petrinets in such a way that compositionality is a born feature rather than an enforced property. In other words
we are interested in the following question: What would Petri nets possibly look like had Petri anticipated theimportance of compositionality? He surely had not seen any process calculus back in 1962. At a theoreticallevel we hope to enrich the nice combinatorial and algebraic theory of Petri nets by an observational theoryof nets. The nets we propose in this paper, called extensional Petri nets, can be seen as a simplification of
the open Petri nets. In our approach only external places act as interfaces. We think of a place as a pool for
tokens or a shared memory. Accordingly we do not distinguish between input places and output places. In
our way of thinking transitions in Petri nets are internal actions. There is no way to synchronize transitions.
Observational equivalence on labeled nets has been studied extensively [BDH92, KoE99, KEB94, MeM90,
NPS95, PrW98, Win87] using bisimulation semantics [Bek84, Hoa78, Kin97, Mil89, MPW92]. Often a label
is attached to a transition so that the standard labeled transition semantics can be applied. The methodology
we will use in this paper is different in a couple of accounts. Firstly since the transitions are all internal
actions the labeled bisimulation semantics is out of place. The appropriate semantics ought to be the barbed
semantics [MiS92]. Secondly we pay particular attention to divergence. This makes sense in the setting ofPetri net model where all transitions are seen as internal actions [Fuy15]. The congruence relation we will
introduce for the extensional Petri nets is an instance of the model independent equality of interactive objects
studied in [Fuy16]. The model independence is important in our opinion because we do not want the equalityof nets to have anything to do with a particular process calculus or a particular process equivalence.
The purpose of this paper is to present the very basics of the extensional Petri net theory. We will becontent with the definition of the model and the bisimulation properties of the extensional Petri nets. We
will point out that the well-known properties about the Petri nets, like coverability, reachability and others,
have quite different and richer interpretations in the extensional model.
Section 2 defines extensional Petri nets and introduces two operations on these nets. Section 3 defines
extensional equality on the extensional Petri nets and provides an alternative characterization. Section 4
explains why the standard Petri net properties need be modified for the extensional Petri nets. Section 5
discusses the relationship to previous works and points out a few research issues.

Extensional Petri Net

3

Petri Net
w1

N

t1

w2



w3

t2



w4



w5


Extensional Petri Net
w1

N

a

t1

w2

w3

t2



w4



w5
b

Fig. 1. A Petri net and an extensional net

2. Extensional Petri Net
Consider a system consisting of a laptop connected to both a printer and a projector. It does not makesense to think that any computation step executed within the laptop can be coupled with some computation
step within the projector. Thus it is pointless to label any computation of a physical device because it cannot
be seen by any other devices. The correct modelling of the situation is that the laptop sends some information
to some place, and the projector picks up the information from that place. The interaction between the two
devices must happen through the interface, which is say a physical connection. Similarly the laptop may
deliver some information to some other place, from which the printer can fetch the message. In this case theconnection may be wireless. So in a broader picture the system contains a subsystem modelling the wirelesscommunication. The subsystem has a place to which the laptop sends the information and another place
accessible by the printer. This simple example serves to explain our design principle: Transitions within a
Petri net are internal actions not observable by any environments; the composition interfaces between Petrinets are places. When two nets are composed, some places in one net are merged with some places of theother net. To specify which is merged with which, we assign labels to places. In the following definition N
is the set of interface names, Z is the set of integers, and N is the set of nonnegative integers.
Definition 2.1. An extensional Petri net, or extensional net, is a 5-tuple N = hP, T, F, W, Ii where
1. P is the finite set of places, ranged over by s and its decorated versions;
2. T is the finite set of transitions, ranged over by t and its decorated versions, such that P ∩ T = ∅;3. F ⊆ P ×T ∪ T ×P is the flow relation;
4. W : F → N \ {0} is the weight function;
5. I : P → N is the interface function, which is a partial function injective on its domain of definition.
A marking of N is a function M : P → N. If M (s) = k we say that the place s contains k tokens. An empty
marking is one in which no places contain any tokens.
Given an extensional net N, we write PN , TN , FN , WN , IN for the components of the net. We write (N, M )to indicate that M is a marking of the extensional net N. Most of the time we simply write M , leaving theunderlying extensional net implicit. In Fig. 1 there is an example of extensional net with marking.
Since every P/T-net can be transformed to a net with unlimited capacities without affecting its behavior,
we will assume that every extensional net has unlimited capacity for all its places. A place of an extensional
net is external if it is labeled by an interface name; it is internal if it is unlabeled. By definition no two
external nodes have the same label. We shall write P e for the set of external places in P and P i for the setof internal places.
We think of a net as a physical device, and tokens as representing information. The transitions describe
how information flows within the device. The following standard terminologies help to define the dynamics
of the extensional nets.

4

X. Dong, Y. Fu and D. Varacca

Definition 2.2. Let N be an extensional net and M be a marking of N.
1. For x ∈ PN ∪ TN , • x = {y | yFN x} is the preset of x; x• = {y | xFN y} is the postset of x.
2. A transition t ∈ TN is M -enabled, notation M [ti, if ∀s ∈ • t.M (s) ≥ WN (s, t).
3. An M -enabled transition t may produce a follower marking M 0 defined as follows.
M (s) − WN (s, t),
if s ∈ • t \ t• ,M (s) + WN (t, s),
if s ∈t• \ • t,def
M 0 (s) =•• M (s) − WN (s, t) + WN (t, s), if s ∈ t ∩ t ,M (s),
otherwise.
We write M [tiM 0 to indicate that M evolves into M 0 by firing t.
When studying observational behaviours of extensional nets, it is unnecessary to spell out which transitionis fired because transitions are internal actions. We borrow the notation from process algebra by writingττM −→ M 0 if M [tiM 0 for some transition t. The reflexive and transitive closure of −→ is denoted by =⇒.
An extensional net is able to interact with its environment through its external places. Two nets interact
by sharing some external places. Extensional nets are thus composed by merging places with identical labels.
We shall always assume that two extensional nets N1 , N2 have disjoint sets of places (PN1 ∩ PN2 = ∅) anddisjoint sets of transitions (TN1 ∩ TN2 = ∅). The following notations are used.
e
PN= {s | s ∈ PN1 ∧ ¬∃s0 ∈PN2 .IN1 (s) = IN2 (s0 )},
1 \N2
e
PN
= {hs1 , s2 i | s1 ∈ (PN1 )e ∧ s2 ∈ (PN2 )e ∧ IN1 (s1 ) = IN2 (s2 )}.
1 ∩N2

In other words PN1 \N2 is the set of all the internal places of N1 plus all the external places of N1 that do
not connect to N2 , while PN1 ∩N2 is the set of pairs of external places of same label. Every pair of places in
PN1 ∩N2 are coerced in the composition. The following definition formalises this intuition.
Definition 2.3. The composition of two extensional nets N1 , N2 , denoted by N1 | N2 , is the extensional net
N defined as follows:ie• PN = PN∪ PN, where
i
i
i
PN
= PN
∪ PN
,
1
2
e
e
e
PN = PN1 \N2 ∪ PN
∪ PN1 ∩N2 .
2 \N1• TN = TN1 ∪ TN2 .
• FN is the following relation
FN1  PN1 \N2 ∪ FN2  PN2 \N1∪ {hhs1 , s2 i, ti | hs1 , ti ∈ FN1 , hs1 , s2 i ∈ PN1 ∩N2 }∪ {ht, hs1 , s2 ii | ht, s1 i ∈ FN1 , hs1 , s2 i ∈ PN1 ∩N2 }∪ {hhs1 , s2 i, ti | hs2 , ti ∈ FN2 , hs1 , s2 i ∈ PN1 ∩N2 }∪ {ht, hs1 , s2 ii | ht, s2 i ∈ FN2 , hs1 , s2 i ∈ PN1 ∩N2 }.
• WN is the function defined by
W (hs, ti),
 N1
WN2 (hs, ti),WN (hs, ti) = WN1 (hs1 , ti),
WN2 (hs2 , ti),

if s ∈ PN1 \N2 ,if s ∈ PN2 \N1 ,if s = hs1 , s2 i ∧ t ∈ TN1 ,if s = hs1 , s2 i ∧ t ∈ TN2 .

And dually for WN (ht, si).
• IN is the function defined as follows: IN1 (s), if s ∈ PN1 \N2 ,IN (s), if s ∈ PN \N1 ,IN (s) = I 2 (s ), if s = hs 2, s i.
N1 1
1 2

Extensional Petri Net

5

t11

a
w11

N1

b
w12

w13



w14


t21

w21

N2

t12



b
w22

w23

t22

w24




a
N1 | N2

t11

w11

w12

b

w13

t12

w14



w21

w22


a
(b)(N1 | N2) 

c



t21
t11

w11

w12

w23

w13

w24

c

t22
t12

w14


w21

w22





t21

w23

w24
t22


c

Fig. 2. Composition and localization

The composition of two markings M1 , M2 of the nets N1 , N2 respectively, notation M1 | M2 , is the marking
on N1 | N2 defined as follows:
if s ∈ PN1 \N2 , M1 (s),M2 (s),
if s ∈ PN \N1 ,(M1 | M2 )(s) = M (s ) + M (s ), if s = hs 2, s i.
1 1
2 2
1 2
An extensional net is locked if none of its transitions is fireable, it is deadlocked if it is locked no matter how
we change the number of tokens in its external places.
We also define a localization operator that removes the label of an external place and turns it into aninternal place.
Definition 2.4. The localization of an extensional net N at a name a, denoted by (a)N, is the extensional
net obtained from N by modifying the labeling function as follows:IN (s), if IN (s) 6= a,def
I(a)N (s) =↑,otherwise.
A marking of (a)N is the same thing as a marking of N, that is (a)M = M . Fig. 2 is a simple example ofcomposition and localization. The localization operator turns the external place labeled b into an internal
place. Once it has become internal, it no longer acts as an interface. Like in CCS both the composition
operator and the localization operator can be applied unconditionally. If N is an extensional net that does
not have any external place labelled a, then (a)N is semantically the same as N. The composition operator“|” is a must in any decent composition theory. Its prime role is to let interaction happen. The localization
operator is important because it imposes control over interaction. Both operators are fundamental. The
semantics of the composition operator is defined by the following standard structural rules:
M1 −→ M10τ

M2 −→ M20

τ

M1 | M2 −→ M1 | M20

M1 | M2 −→ M10 | M2

τ

τ

.

Back to the example we discussed in the beginning of the section. Let L, P and D be the extensional nets
for the laptop, the projector and the printer respectively. Suppose both L and P have a place labeled p, andboth L and D have a place labeled d. Then we can form the composite system L | P | D. The components
L and P may interact through the place labeled p, and L and D may interact through the place labeled d.
If we want to model the situation where the connection between the laptop and the projector is private, we
obtain the system (a)(L | P) | D. In this system no other devices are allowed to connect to the projector.

6

X. Dong, Y. Fu and D. Varacca

3. Bisimulation for Extensional Nets
According to the viewpoint advocated in this paper the observables of an extensional Petri net are theexternal places since they are the interfaces through which the environments may test the net. Quantitively
the status of an extensional net marking is determined by the number of tokens in the external places because
these tokens can be consumed by the nets composed with it.
In concurrency theory the standard bisimulation equivalence is the weak bisimulation of Park and Milner [Par81, Mil89]. From the observational point of view there are two decidedly improvements of the weakbisimulation. The first is the barbed bisimulation of Milner and Sangiorgi [MiS92]. This is the first step towards a model independent characterization of process equality. The second is the branching bisimulation of
van Glabbeek and Weijland [GlW89]. The branching approach draws a line between the internal transitions
that change states and those that do not change states. It has been shown in a number of settings that thebranching bisimilarity is more stable than the weak bisimilarity.
We define in this section an observational equivalence for the extensional nets. The particular equality
we are interested in is the absolute equality studied in [Fuy16]. This is the equality for both computation
models and interaction models. As an equality for computation it should be both bisimilar in the sense of van
Glabbeek and Weijland [GlW89] and divergence sensitive in the sense of Priese [Pri78]. Hence the following.
Definition 3.1. A binary relation R on extensional net markings is a bisimulation if the following are valid
whenever M1 RM2 .
τ

τ

τ

τ

1. If M1 −→ M10 , then either M2 =⇒ M20 for some M20 such that M1 RM20 and M10 RM20 , or M2 =⇒ M200 −→M20 for some M200 , M20 such that M1 RM200 and M10 RM20 .
2. If M2 −→ M20 , then either M1 =⇒ M10 for some M10 such that M10 RM2 and M10 RM20 , or M1 =⇒ M100 −→M10 for some M100 , M10 such that M100 RM2 and M10 RM20 .
Definition 3.2. A binary relation R on extensional net markings is codivergent if the following are valid
whenever M0 RM00 .
τ

τ

τ

τ

τ

τ

τ

τ

τ

τ

1. If M0 −→ M1 −→ M2 −→ M3 −→ . . . then M00 −→ M 00 for some M 00 such that Mi RM 00 for some i > 0.
2. If M00 −→ M10 −→ M20 −→ M30 −→ . . . then M0 −→ M 0 for some M 0 such that M 0 RMi0 for some i > 0.
From the point of view of interaction the equality should be compositional and preserve the capacity tointeract. The compositionality property is formalized next.
Definition 3.3. A binary relation R on extensional net markings is extensional if the following are valid.
1. (M1 | M2 ) R (M10 | M20 ) whenever M1 RM10 and M2 RM20 .
2. For every interface name a, (a)M R (a)M 0 whenever M RM 0 .
To introduce the next condition we need the important notion of observation. We will write C, D and theirdecorated versions for finite subsets of N .
Definition 3.4. An observation is a function O : C → N such that O(c) ≥ 0 for every c ∈ C. The observationeof a marking M of an extensional net N is the function OM : IN (PN) → N such that OM (a) = M (s) for theee).
s ∈ PNsatisfying IN (s) = a. The observation of a marking M is positive if OM (a) > 0 for some a ∈ IN (PN
Let O : C → N, O0 : D → N be observations with C ⊆ D. We write O ≤ O0 if O(c) ≤ O0 (c) for all c ∈ C.
We write O = O0 if O ≤ O0 ≤ O.
Definition 3.5. A marking M is observable, notation M ⇓, if M =⇒ M 0 for some M 0 with positive OM 0 .
Equal markings should be either both observable or both unobservable.
Definition 3.6. A relation R on markings is equipollent if M ⇓ ⇔ M 0 ⇓ whenever M RM 0 .
We are now able to define the absolute equality [Fuy16] for the extensional Petri nets. In this paper wegive it a different name for the reason that the communication mechanism of the model is based on sharedmemory rather than message-passing.

Extensional Petri Net

7

Definition 3.7. The extensional equality on the extensional net markings, denoted by =, is the largest
reflexive, extensional, equipollent, codivergent bisimulation on the extensional net markings.
It is easy to see that in the presence of reflexivity the union of a set of extensional, equipollent, codivergent
bisimulations is an extensional, equipollent, codivergent bisimulation. Hence the well definedness of theextensional equality. For more motivations and properties about the absolute equality the reader is referred
to [Fuy16]. For the applications of the absolute equality in computation and process models, consult [FuL10,
Fuy15, Fuy17a, Fuy17b]. The extensional equality of nets is yet another application of the absolute equality.
When reasoning about a relation we sometimes need to take its closure in one way or another. The
extensional closure of a binary relation R on the extensional net markings, denoted by R∗ is the least relation
satisfying the following: (i) R ⊆ R∗ ; (ii) (M | M 0 , M 00 | M 000 ) ∈ R∗ whenever M R∗ M 00 and M 0 R∗ M 000 .
Proposition 3.1. The relation = is both an equivalence and a congruence.
Proof. The relation = is reflexive by definition. The extensionality, equipollence, codivergence and bisimulation are symmetric and transitive. So = is an equivalence. To prove congruence, one notice that M = M 0
implies (a)M = M = M 0 = (a)M 0 for every interface name a. So all one has to prove is that =∗ is anextensional, equipollent, codivergent bisimulation. This is routine.
Definition 3.8. A renaming is an injective function ς : C → N for some finite C ⊆ N . A displacement is afunction δ : C → Z for some finite C ⊆ N .
The notation M ς denotes the extensional net marking obtained by renaming the labels of M according
to ς. The marking M δ is the marking M modified by the effect δ exerted by an environment. It is defined
as follows.
eM (s) + δ(a), if s ∈ PN
and IN (s) = a and δ is defined on a,def
M δ(s) =(1)
M (s),
otherwise,
The map M δ is not necessarily a legal marking. In the rest of the paper whenever we write M δ we always
assume that it is a legitimate marking. When we say M δ = N δ for all δ we mean that M δ = N δ holds forall such δ that both M δ and N δ are legitimate.
Lemma 3.1. Suppose ς is a renaming function. Then M = M 0 implies M ς = M 0 ς.
Proof. Let RM =M 0 be the subset of = that contains all the pairs (M1 , M10 ) of = such that M =⇒ M1 and
M 0 =⇒ M10 . Let ς be a renaming from {a} to N . It is easy to show that {(M ς, M 0 ς) | (M, M 0 ) ∈ R} ∪ = isthe largest reflexive, extensional, equipollent, codivergent bisimulation.
Before proving the next property about the equality, let’s recall some standard terminologies and technicalτlemmas. We say that M −→ M 0 is a (deterministic) computation step, notation M → M 0 , if M 0 = M ; it is aιnondeterministic computation step, notation M −→ M 0 , if M 0 6= M . The reflexive and transitive closure of
ι
τ
τ
τ
τ
→ is denoted by →∗ . If M = N then M −→ M 0 must be bisimulated by N −→ N1 −→ . . . −→ Nk −→ N 0ι000such that N → N1 → . . . → Nk , Nk −→ N and M = N . In some sense this is the property that justifies
the definition of bisimulation. It is related to the following two fundamental lemmas.
τττ

Lemma 3.2 (Computation Lemma). If M0 −→ M1 −→ . . . −→ Mk = M0 then M0 → M1 → . . . → Mk .
Lemma 3.3 (Bisimulation Lemma). If M =⇒ M 0 = N and N =⇒ N 0 = M then M = N .
The proofs of the two lemmas can be found in [Fuy16].
The extensional equality is often not easy to work with. The main difficulty is caused by the extensionality
condition. We are going to give an important characterization of the extensional equality that bypasses theextensionality condition. The characterization makes use of the following lemma.
Lemma 3.4. If M = N then the following hold: (i) M →∗ M 0 for some M 0 such that OM 0 ≥ ON andM 0 δ = N δ for all δ. (ii) N →∗ N 0 for some N 0 such that ON 0 ≥ OM and M δ = N 0 δ for all δ.
Proof. Suppose M, N are markings of the nets N1 , N2 respectively and that M = N . Assume that OM 6≤ ON
and neither a nor b appears in N1 | N2 . Let ec be the set of all labels that appear in N1 | N2 . Let N be an
extensional net with three transitions t1 , t2 , t3 , t4 , t5 and let L be a marking on N that assigns no tokens inany external places. When composed with N1 , the net N can perform the following actions.

8

X. Dong, Y. Fu and D. Varacca• It can fire t1 whose precondition requires all the tokens in the external places of N1 . After the action theobservation of the marking of N1 is M δ and a token in the place labeled a is produced. Having fired t1
the transition t4 can be fired to deadlock N.
• It can fire t2 that produces a token in the place labeled by b and empties all the external places of N1 .
Afterwards it can fire t5 to deadlock N.
• It can fire t3 to deadlock N and produces the same number of tokens as it consumes in all external places.
Additionally we require that the transitions t1 , t2 block each other. A diagrammatic illustration of N withmarking L is given below, in which we have ignored part of the net that connects to N1 .

ιSuppose that M | L −→ M δ | L0 is caused by firing t1 . This is a nondeterministic computation because it
disables the capacity to produce a token in the place labeled b. If N cannot reach to a marking N 0 suchthat ON 0 ≥ OM then (ec)(M δ | L0 ) is observable whereas no descendant of (ec)(N | L) is observable. This is acontradiction. We conclude that there must be some N 0 such that ON 0 ≥ OM and for some L0 ,
ιN | L →∗ N 0 | L −→ N 00 | L00 = M δ | L0 .
ιι

Now N | L −→ N | L0 = N , caused by the firing of t3 , must be bisimulated by N 0 | L →∗ N10 | L −→
ι
N10 | L0 = N10 for some N10 , and N 0 | L −→ N 0 | L0 = N 0 , caused by the firing of t3 , must be bisimulated byι
N | L →∗ N1 | L −→ N1 | L0 = N1 for some N1 . It follows that N =⇒ N1 = N 0 and N 0 =⇒ N10 = N . Thus0
N = N by appealing to the Bisimulation Lemma. Also notice that L00 must be the same as L0 , otherwise asimilar contradiction can be derived. It follows that N 00 = N 0 δ and N 0 δ | L0 = M δ | L0 . With a marking L0
the net N can fire t4 to deadlock itself we conclude from Bisimulation Lemma that N 0 δ = M δ.
Having seen the Computation Lemma and Lemma 3.4, let’s see a couple of examples.
1. Define a three place extensional net, all the three places being external. Let’s use the vector h1, 2, 3i todenote a marking. The net has three transitions that can be executed cyclically in the following manner.
τττ

(1, 2, 3) −→ (2, 3, 1) −→ (3, 1, 2) −→ (1, 2, 3).
The transitions are defined in the following diagrammatic presentation of the extensional Petri net.

By the Computation Lemma these three pairwise distinct markings are equal.
2. Suppose we have an extensional net with two external places. For either external place there is a transition
that increases the number of tokens in both places and another transition that decreases the number oftokens by one. The diagrammatic presentation is given below.

Extensional Petri Net

9

Starting from any nonempty marking this extensional net can reach to any marking. It follows from theComputation Lemma that all nonempty markings of this extensional net are equal. The empty marking
is not equal to any other marking.
The two examples also provide an intuition for Lemma 3.4.
Based on Lemma 3.4 we introduce another equality for the extensional net markings.
Definition 3.9. A codivergent bisimulation R on the extensional net markings is an open bisimulation if
the following statements are valid whenever M RN .
1. M =⇒ M 0 for some M 0 such that OM 0 ≥ ON and M 0 δRN δ for all replacement δ.
2. N =⇒ N 0 for some N 0 such that ON 0 ≥ OM and M δRN 0 δ for all replacement δ.
The open bisimilarity ' is the largest open bisimulation.
This new equality is justified by the following coincidence result.
Theorem 3.1. The open bisimilarity coincides with the extensional equality.
Proof. The inclusion = ⊆ ' follows from Lemma 3.4. In the other direction we need to prove that ' isreflexive, equipollent and extensional. Reflexivity and equipollence are obvious from definition. For extensionality we only have to prove that M ' N implies M | L ' N | L and L | M ' L | N for all extensional net
marking L because that is equivalent to the extensionality condition. It is not difficult to verify that both{(M | L, N | L) | M ' N and L is a marking} and {(L | M, L | N ) | M ' N and L is a marking} are open
bisimulations.

4. Observable Property for Extensional Nets
From the point of view of observation the number of tokens in any internal places is immaterial. If we see thenets from this perspective we should define Petri net properties that ignore all internal places. To explain
the basic idea let’s define coverability/reachability for the extensional nets.
Definition 4.1. Suppose N is an extensional net, M is a marking of N and O, O0 are observations of N.
We say that O0 is coverable by M , respectively reachable from M , if M =⇒ M 0 for some marking M 0 suchthat OM 0 ≥ O0 , respectively OM 0 = O0 . We say that O0 is coverable by O, respectively reachable from O, if
M 00 =⇒ M 000 for some markings M 00 , M 000 such that OM 00 = O and OM 000 ≥ O0 , respectively OM 000 = O0 .
It is well-known that both the coverability problem [KaM69, Rac78] and the reachability problem [SaT77,
May81, Kos82, Lam92] for the Petri nets are decidable. The next two results show that the decidability proofof a problem in the extensional net theory is built upon the decidability proof of the corresponding problem
in the Petri net theory. We assume that the reader is aware of the proof of the decidability of the coverability
problem. The proof is not short, so it cannot be repeated here.
Theorem 4.1. Given observations O, O0 of an extensional net N and a marking M of N, it is decidable tocheck if O0 is coverable by O respectively M .
Proof. Using Rackoff’s proof [Rac78] we argue that it is decidable to check if O0 is coverable by O. Suppose
N has n places and e external places. We write a marking of the net as an n-tuple hv1 , . . . , vn i ∈ Nn and an
external marking as an e-tuple hv1 , . . . , ve i ∈ Ne . We identify O to hu1 , . . . , ue i and O0 to hw1 , . . . , we i. The
question is if there are ue+1 , . . . , un , u01 , . . . , u0n ≥ 0 such that hu1 , . . . , un i =⇒ hu01 , . . . , u0n i and hu01 , . . . , u0e i ≥hw1 , . . . , we i. Suppose z = hz1 , . . . , zn i ∈ Zn . We say that z is i-bounded if 0 ≤ zj for all j such that0 ≤ j ≤ i, and that z is i-r-bounded, where r > 0, if 0 ≤ zj ≤ r for all j such that 0 ≤ j ≤ i. A sequence
z1 , z2 , . . . , zs is i-bounded/i-r-bounded if each zt , where 1 ≤ t ≤ s, is i-bounded/i-r-bounded. The sequenceis i-covering if zs (j) ≥ uj for all j such that 1 ≤ j ≤ i. Rackoff proved that if there is an i-bounded
and i-covering sequence, where 1 ≤ i ≤ n, from hu1 , . . . , un i then there is such a sequence whose length isp(m,i)
bounded by 22, where p(x, i) is a polynomial and m is the input size. Using this result it is easy to seethat the coverability question is equivalent to asking if hw1 , . . . , we , 0, . . . , 0i can be covered by a path fromp(m,e)
p(m,e)
hv1 , . . . , ve , m22, . . . , m22i, which is decidable. The argument for the other case is similar.

10

X. Dong, Y. Fu and D. Varacca

Similarly we can derive the decidability of the reachability problem in the extensional setting. The reader
is referred to the literature for the highly nontrivial decidability proof.
Theorem 4.2. Given two observations O, O0 of an extensional net N and a marking M of N, it is decidable
to check if O0 can be reached from O respectively M .
Proof. We can prove the theorem using the well-known KLMST algorithm [SaT77, May81, Kos82, Lam92]. A
simple argument is also possible in the case of checking O reaching O0 . It is decidable to check if hu1 , . . . , ue ican reach to hw1 , . . . , we i. If the answer is yes, we apply a result in [LeS15] stating that there is a bound,computable from the input net, on the length of the minimal path from hu1 , . . . , ue i to hw1 , . . . , we i. Using
this bound we can easily compute hue+1 , . . . , un i and hwe+1 , . . . , wn i such that hw1 , . . . , we , we+1 , . . . , wn i isreachable from hu1 , . . . , ue , ue+1 , . . . , un i.
Further questions about coverability and reachability can be asked. Suppose we know that ON can becovered by OM and that M 0 = M . Is it true that ON can be covered by OM 0 ? The answer is positive. Thisis because M =⇒ M1 for some M1 such that OM1 ≥ ON . Since M 0 = M there must be some M10 such thatM 0 =⇒ M10 = M1 . By Lemma 3.4 some M20 exists such that M10 →∗ M20 and OM20 ≥ OM1 . Thus OM20 ≥ ON .

M2’

M1

M1 ’
N

M

M’

Now consider a similar scenario. Suppose that ON can be covered by OM and that N 0 = N . Is it the casethat N 0 is coverable by M ? By assumption M =⇒ M 0 for some marking M 0 such that OM 0 ≥ ON . By
Lemma 3.4 there is some N1 such that N =⇒ N1 and ON1 ≥ ON 0 . The problem is that the transition
sequence from N to N1 is not necessarily a legal transition sequence from M 0 due to the presence of internal
places. Reachability satisfies even less algebraic property. Even if ON is reachable from OM and M 0 = M ,we know nothing about the reachability of ON from OM 0 . For example M may have the following transition
sequence (0, 0) → (2, 2) → (4, 4) → . . . → (2i, 2i) → . . . whereas M 0 may have the following transition
sequence (1, 1) → (3, 3) → (5, 5) → . . . → (2i + 1, 2i + 1) → . . .. It can be the case that M reaches to N if
and only if M 0 never reaches to N . Both coverability and reachability enjoy better algebraic property when
confined to those extensional nets whose internal markings are bounded. This is a reasonable restriction if
nets are regarded as physical devices.

5. RemarkWe have demonstrated that by simply assigning interface names to places that are meant to be interfaces we obtain a variant of Petri net model that enjoys nice compositional property as well as a smoothobservational theory. The extensional theory offers a new dimension for future investigations. The algebraic
theory of the extensional nets should be systematically studied. We expect that a property defined in termsof external places is algebraic in the sense that it is preserved by the extensional equality. Many decidability
results and algorithms in Petri net theory should be reexamined in this new framework. As we have seen the
problems are often generalized when casting in the setting of the extensional nets. Hopefully studies on theExtensional Petri Net

11

generalized problems will shed new light on these problems. This paper is only a starting point for a generalcompositional theory of Petri nets.
The observational theory of nets studied in this paper is different from any observational theory proposedin literature. We have applied the model independent approach of the theory of interaction to Petri nets.
Apart from obtaining a consistent theory the model independent approach allows one to study further
issues like completeness and expressiveness [Fuy16] of Petri net model. What is for example the relationshipbetween the extensional Petri net model and the value-passing calculus [Hoa78, Mil89, Fuy13]? How about theincompatibility result between the extensional Petri net model and the (higher order) π-calculus [MPW92,
FuZ15, Fuy17a]? What is a universal extensional Petri net [Fuy17b]? The observation theory of this paper
has laid down the fundamental framework for answering all these interesting questions.
As is pointed out in the introduction there is now a large literature on the compositionality of Petrinet. Compared to the most proposed models the extensional Petri model is quite light-weighted. Our goal
is not to pursue an integrated model that introduces a whole range of process operators in order to have abetter match to a process calculus. Net property analysis is hard in such a complicated model. Our model
also differs greatly from the models that admit labelling on transitions and synchronisation of transitions.
It is our opinion that a Petri net transition is different from a transition in a process calculus. In the lattermodel an input action or an output action is part of an interaction, whereas in the former model a transition
is a complete action. The synchronisation of two transitions in two components of a Petri net can only be
implemented through interfaces. Our approach to the compositionality of Petri net is not new. Assigninglabels to places is a feature of a number of models proposed in literature. Most of the time it comes with otherfeatures that complicate models considerably. The motivation of this work is to solve the compositionality
problem by introducing as few operators as possible so that the new model looks like Petri net model as muchas possible. Our understanding of the issue is that the minimal set of operators necessary for a compositional
theory only consists of the concurrent composition operator and the localization operator. The extensional
Petri net model formalizes the view that a net is composed from individual transitions. So a structural theory
is possible with the extensional Petri nets. Another advantage of our minimal model is that it inherits mostof the Petri net properties from the classical theory. The combinatorial approach and the algebraic approachwork just as well in the extensional scenario. The interplay between the net properties and the observational
properties is an avenue for further study.

Acknowledgments.
The work is supported by National Natural Science Foundation of China (61472239, 61772336). The authors
would like to thank the anonymous reviewers for the comments.

References[Aal05]van der Aalst, W.: Pi calculus versus Petri nets: Let us eat “humble pie” rather than further inflate the “Pi hype”.
BPTrends, 2005(5).
[BBG09]Baldan, P., Bonchi, F., Gadducci, F.: Encoding asynchronous interactions using open Petri nets. CONCUR’09,
LNCS, vol. 5710, 99–114, 2009.
[BCE01]
Baldan, P., Corradini, A., Ehrig, H., Heckel, R.: Compositional Modeling of Reactive Systems Using Extensional
Nets. C ONCUR’01, LNCS, vol. 2154, 502–518, 2001.
[BCE05]
Baldan, P., Corradini, A., Ehrig, H., Heckel, R.: Compositional Semantics for Open Petri Nets based on Deterministic Processes. Mathematical Structures in Computer Science, 15(1), 1–35 (2005).
[BCE07]
Baldan, P., Corradini, A., Ehrig, H., Heckel, R., König, B.: Bisimilarity and Behaviour-Preserving Reconfigurationsof Open Petri Nets, CALCO’07, LNCS, vol. 4624, 126–142, 2007.
[BCE08]Baldan, P., Corradini, A., Ehrig, H., König, B.: Open Petri Nets: Non-deterministic Processes and Compositionality.
ICGT’08, LNCS, vol. 5214, 257–273, 2008.
[BDH92]
Best, E., Devillers, R., Hall, J. G.: The Petri box calculus: a new causal algebra with multi-label communication,
Advances in Petri Nets, LNCS, vol. 609, 21–69, 1992.
[BDK01]
Best, E., Devillers, R., Koutny, M.: A Unified Model for Nets and Process Algebras. Handbook of Process Algebra
Elsevier Science, 875–944, Amsterdam, 2001.
[BDK2001] Best, E., Devillers, R., Koutny, M.: Petri Net Algebra. Monographs in Theoretical Computer Science, An EATCS
Series, Springer, 2001.
[Bek84]
Bergstra, J.A. and Klop, J.W.: The algebra of recursively defined processes and the algebra of regular processes,
ICALP’84, LNCS, vol. 172, 82-95, 1984.
[BuG95]Busi, N., Gorrieri, R.: A Petri Net Semantics for pi-Calculus, CONCUR’ 95, LNCS, vol. 962, 145–159, 1995.

12[BuG09][CWY04][DKK04][DNM88][Fuy13][Fuy15][Fuy16][Fuy17a][Fuy17b][FuL10][FuZ15][GlW89][GHH08][Gol90][Hao97][Hoa78][KaM69][KEB94][Kin97][Kos82][KoE99][Lam92][LeS15][LJZ13][May81][MeM90][Mil89][MiS92][MPW92][Nie87][NPS95][Par81][Per81][PrW98][Pri78][Rac78][SaT77][Win87][YCX07]

X. Dong, Y. Fu and D. Varacca

Busi, N., Gorrieri, R.: Distributed semantics for the π-calculus based on Petri nets with inhibitor arcs. Journal of
Logic and Algebraic Programming, 78(3), 138–162, 2009.
Cao, M., Wu, Z., Yang, G.: Pi Net – a New Modular Higher Petri Net. Journal of Shanghai Jiaotong Univeristy.
38(1), 52–58, 2004.
Devillers, R., Klaudel, H., Koutny, M.: Petri net semantics of the finite pi calculus.FORTE’04, LNCS, vol.3235(2),309–325, 2004.
Degano, P., Nicola, R.D., Montanari, U.: A Distributed Operational Semantics for CCS Based on C/E Systems.
Acta Informatica, 26-59, 1988.
The Value-Passing Calculus. Theories of Programming and Formal Methods, Lecture Notes in Computer Science
8051, 166–195, 2013.
Fu, Y.: Nondeterministic structure of computation. Math. Structures Comput. Sci., 25: 1295–1338, 2015.
Fu, Y.: Theory of Interaction. Theoretical Computer Science, 611, 1–49, 2016.
Fu, Y.: On the Power of Name-Passing Communication. CONCUR 2017, 2017.
Fu, Y.: The Universal Process. Logical Methods in Computer Science, 13, 1-23, 2017.
Fu, Y. , Lv, H.: On the Expressiveness of Interaction. Theoretical Computer Science, 411, 1387–1451, 2010.
Fu, Y. , Zhu, H.: The Name-Passing Calculus. arXiv:1508.00093, 2015.
van Glabbeek, R., Weijland, W.: Branching Time and Abstraction in Bisimulation Semantics. Information Processing’89, pp. 613–618, 1989.
Guo, X., Hao, K., Hou, H., Ding J.: the Representation of Petri Nets with Prohibition Arcs by Pi+ Calculus.
Journal of System Simulation, S2: 9–12.
Goltz, U.: CCS and Petri Nets. Chapter, Semantics of Systems of Concurrent Processes, LNCS, vol. 469, pp.
334–357, 1990.
Hao, K.: Open nets – A Model for Interative Concurrent Systems. Jounal of Northwest University, 27(6): 461–466,
1997.
Hoare, C.A.R.: Communicating Sequential Processes. Communications of ACM, 21(8), 666–677, 1978.
Karp, R., Miller, R.: Parallel Program Schemata. Journal of Computer and System Science, 147-195, 1969.
Koutny, M., Esparza, J., Best, E.: Operational semantics for the Petri box calculus. CONCUR’94, LNCS, vol. 836,
210–225, 1994
Kindler, E.: A compositional partial order semantics for Petri net components. Application and Theory of PetriNets, LNCS, vol.1248, 235–252, 1997
Kosaraju, S.: Decidability of reachability in vector addition systems. STOC, pp. 267–281, 1982.
Koutny, M., Best, E.: Operational and denotational semantics for the box algebra. Theoretical Computer Science,
211(1-2): 1-83, 1999.
Lambert, J.: A structure to decide reachability in Petri nets. Theoretical Computer Science, 99, 79-104, 1992.
Leroux, J., Schmitz, S.: Demystifying Reachabiity in Vector Addition Systems. LICS 2015, 2015.
Liu, G., Jiang, C., Zhou,M.: Interactive Petri Nets. IEEE Transactions on Systems, Man, and Cybernetics: Systems,
43(2), 291–302, 2013.
Mayr, E.: An algorithm for the general Petri net reachability problem. STOC, pp. 238-246, 1981.
Meseguer, J., Montanari, U.: Petri nets are monoids. Information and Computation, 88, 105–155, 1990.
Milner, R.: Communication and Concurrency. Prentice Hall, 1989.
Milner, R., Sangiorgi, D.: Barbed bisimulation. ICALP’92, LNCS, 685-695, 1992.
Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes. Information and Computation, 1–40 (Part I),
41–77 (Part II) , 1992.
Nielsen, M.: CCS and its relationship to net theory. Petri Nets: Applications and Relationships to Other Modelsof Concurrency. LNCS, vol. 255, 393–415,1987.
Nielsen, M., Priese, L., Sassone, V.: Characterizing Behavioural Congruences for Petri Nets. CONCUR 955, vol.
962, 175-189, 1995.
Park, D.: Concurrency and Automata on Infinite Sequences, Theoretical Computer Science, LNCS, vol. 104, 167–
183, 1981.
Peterson., J.: Petri Net Theory and the Modelling of Systems. Prentice Hall, 1981.
Priese, L., Wimmel, H.: A uniform approach to true-concurrency and interleaving semantics for Petri nets. Theoretical Computer Science, 206, 219-256, 1998.
Priese, L.: On the Concept of Simulation in Asynchronous, Concurrent Systems. P rogress in Cybernatics andSystems Research,(7), 85–92, 1978.
Rackoff, C.: The Covering and Boundedness Problems for Vector Addition Systems. T heoretical Computer Science,
223-231, 1978.
Sacerdote, G., Tenney, R.: The decidability of the reachability problem for vector addition systems. STOC, 61–76,
1977.
Winskel, G.: Event Structures, Petri Nets: Applications and Relationships to Other Models of Concurrency, LNCS,
vol. 255, 325–392, 1987.
Yu, Z., Cai, Y., Xu, H.: Petri net semantics for Pi Calculus. Control and Decision. 22(8): 864–868, 2007.