Many kinds of morphisms on Petri nets have been defined and studied. They can be used as formal techniques supporting refinement/abstraction of models. In this paper we introduce a new notion of morphism on marked graphs, a class of Petri nets used for the representation of systems having deterministic behavior. Such morphisms can indeed be used to represent a form of abstraction on marked graphs, consisting in folding cycles and identifying chains. We will then prove that systems joined by these morphisms show behavioral similarities.
Introduction When working on concurrent and distributed systems, the dimensions and complexity of a model may lead to difficulties in the analysis of its features and properties. For this reason it is useful to have formal techniques allowing the decomposition of the entire model into separate modules which can be studied separately, then being recomposed maintaining their properties. Another way to reduce the dimension and complexity of a model is to use a multilevel approach to its analysis: we start working on a very abstract version of the model, then proceed through different levels of refinement by adding details to the model.
In order to obtain such functionalities we can use morphisms on Petri nets. In
the literature (see, for example, [
Some kinds of morphisms defined in the literature, such as ↵ -morphisms ([
Such kind of abstraction preserves the behavior of the mapped part of the original system. This means that, whenever we apply a Fˆ-morphism on a system, all the sequences of actions executable in the reduced version can be found in the original model.
In the last part of this paper, an analysis of preserved and reflected behavioral properties and invariants of marked graphs joined by Fˆ-morphisms is performed.
In the next section, basic definitions related to Petri nets and their unfoldings are recalled. In Section 3 F - and Fˆ-morphisms are introduced together with their main features. Then the relationship between the unfoldings of two marked graphs joined by a Fˆ-morphism is explicated. Section 4 shows the results of the analysis of behavioral and structural properties preserved and reflected by Fˆmorphisms. The paper is closed by a short concluding section. 2
Preliminary definitions In this section we recall basic definitions about marked graph theory and unfoldings. These notions will be used in the next chapters to study important aspects of F -morphisms. 2.1
We first start introducing the notion of net as seen in [
All places and transitions are said to be elements of N . A net is finite if the set of elements is finite.
For an element x of S [ T , its pre-set is defined by while its post-set is defined by •x = {y 2 S [ T | (y, x) 2 F } x• = {y 2 S [ T | (x, y) 2 F }.
A directed path (path for short) in a net N is a nonempty sequence x0 . . . xk satisfying xi 2 xi• 1 for each i (1 i k). We say that this path leads from x0 to xk. The net is strongly connected if for each two elements x and y there exists a directed path leading from x to y.
An undirected path is a nonempty sequence x0 . . . xk of elements satisfying xi 2 •xi 1 [ xi• 1 for each i (1 i k). Such undirected path leads from x0 to xk. The net is weakly connected if, for each two elements x and y, there exists an undirected path leading from x to y. In this paper, we will call connected a weakly connected net.
A directed circuit is a directed path x0 . . . xkx0 such that, for each i, j 2 N, i, j k, i 6= j, xi 6= xj holds.
The states of a Petri net are defined by its markings. State changes are caused by the occurrences of transitions. A marking of a net N = (S, T, F ) is a mapping M : S ! N. A place s 2 S is marked by a marking M if M (s) > 0.
A transition t is enabled at a marking M if M marks every place in •t. Then t can occur. Its occurrence transforms M into the marking M 0, defined for each place s as
M 0(s) = 8 ><
M (s)
1 if s 2 •t \ t•,
M (s) + 1 if s 2 t• \ •t, >: M (s) otherwise.
t In this case we write M! M 0. Notice that a place in •t\ t• is marked whenever t is enabled but does not change its token count by the occurrence of t. A marking is called dead if it enables no transition of N . A net N together with an initial marking M0 constitutes a Petri Net System (also called place/transition system), denoted (N, M0).
Let M be a marking of a net. A finite sequence t1 . . . tk of transitions is called a finite occurrence sequence, enabled at M , if there are markings M1, . . . , Mk such that
M!t1 M1!t2 . . .!tk
Mk.
In this case we write M! ! Mk, where ! = t1 . . . tk. The empty sequence E is enabled at any marking M and satisfies M! E M . A marking M 0 is said to be reachable from a marking M if there exists a finite occurrence sequence ! such that M! ! M 0.
In this paper we will mainly work on a particular kind of Petri nets, the marked graphs.
Definition 2. A Petri net N = (S, T, F, M0) is a marked graph if, for every s 2 S, |•s| 1 and |s•| 1. 2.2
The presence of an initial marking M0 allows to identify the behavior of the Petri net system (N, M0), defined as the set of all markings reachable from M0 together with the set of occurences of each transition which make the global state of the system change.
Properties of a net depending on the initial marking are known as behavioral
properties of the net. We now introduce some behavioral properties ([
if the number of tokens in each place does not exceed a finite number k for any marking reachable from M0, i.e., M (s) k for every place s and every reachable marking M . (N, M0) is said to be safe if it is 1-bounded.
While boundedness implies the presence of a finite number of global states for a finite net, liveness ensures that every event can potentially occur in the future.
said to be a live marking for N ) if, no matter which marking has been reached from M0, it is possible to ultimately fire any transition of the net by progressing through some further firing sequence. 2.3
Definitions recalled in this section are taken from [
+ aij = aij aij where ai+j = 1 if there is an arc of N going from transition j to its post-condition i, otherwise ai+j = 0, while aij = 1 if there is an arc to transition j from its pre-condition i, otherwise aij = 0.
Some properties of a Petri net can be studied through the incidence matrix and its invariants. A S-invariant associates weights to places in a way such that the weighted sum of tokens is the same in all reachable markings.
S ! Z is a S-invariant for N iff it is a solution of: IA = 0.
T-invariants allow to identify possible cyclic behaviors in a Petri net.
T ! Z is a T-invariant for N iff it is a solution of: AJ T = 0. 2.4
The behavior of a Petri net N can be represented in different ways. One of these
is to use the so called unfolding of N . In order to understand what the unfolding
of a net is, we first need to introduce some formal definitions. The theoretical
notions we will relate in this subsection are all taken from [
The relation precedes defines a partial order on S [ T , and Min(N ) is the set of minimal elements of that partial order. We now introduce the notion of conflict.
Definition 9. Let N = (S, T, F, M0) be a Petri net. For x1, x2 2 S [ T , x1 and x2 are in conflict, denoted x1 # x2, if there exist distinct transitions t1, t2 2 T such that •t1 \ •t2 6= ; and ti precedes xi, for i = 1, 2. For x 2 S [ T , x is in self-conflict if x # x.
The concept of conflict is used to define occurrence net.
Definition 10. An occurrence net is a finitary acyclic net N = (S, T, F, M0) such that – for every s 2 S, |•s| 1, – no transition t 2 T is in self-conflict, and – M0 = Min(N ).
We now define a particular kind of morphism called “folding” in [
Definition 11. Let Ni = (Si, Ti, Fi, M0i) be nets, i = 1, 2. A homomorphism from N1 to N2 is a mapping h : S1 [ T1 ! S2 [ T2 such that – h(S1) ✓ S2 and h(T1) ✓ T2, – for every t 2 T1, the restriction of h to •t is a bijection between •t and •h(t), and similarly for t• and h(t)•, and – the restriction of h to M01 is a bijection between M01 and M02.
The notions of homomorphism and occurrence net are necessary to formally define branching processes.
Definition 12. Let N = (S, T, F, M0) be a net. A branching process of N is a pair (N 0, ⇡ ), where N 0 = (S0, T 0, F 0, M00 ) is an occurrence net and ⇡ is a homomorphism from N 0 to N , such that, for every t1, t2 2 T , if •t1 = •t2 and ⇡ (t1) = ⇡ (t2), then t1 = t2.
In [
A new class of morphisms on marked graphs In this section we introduce a new kind of morphism on marked graphs, the F -morphisms. We will then focus on a subclass of such morphisms, the Fˆmorphisms, analysing some interesting features of theirs. Finally, we will study the relationship between the unfoldings of two marked graphs joined by a Fˆmorphism. In this paper we only consider a particular kind of marked graphs.
self-loops.
It is now possible to introduce the main notion of this work.
Definition 13. Let Ni = (Si, Ti, Fi, M0i), i = 1, 2, be two marked graphs. A F -morphism from N1 to N2 is a pair (, ⌧ ), where : S1 ! S2 and ⌧ : T1 ! T2 are partial surjective functions, such that: – if ⌧ (t1) is undefined, then (•t1) = ; = (t1•), – if ⌧ (t1) = t2, then the restriction of to •t1 is an injective and surjective partial function from •t1 to •t2 and, similarly, the restriction of to t1• is an injective and surjective partial function from t1• to t2•, – for every s0 2 S2
M02(s0) =
M01(s).
X s2 1(s0)
We define the composition of two F -morphisms ( 1, ⌧ 1) : N1 ! N2 and ( 2, ⌧ 2) : N2 ! N3 by using the notion of composition of functions, i.e., ( 1, ⌧ 1) ( 2, ⌧ 2) = ( 2 1, ⌧ 2 ⌧ 1) : N1 ! N3. F -morphisms are closed by composition. Theorem 1. Let Ni = (Si, Ti, Fi, M0i) be marked graphs for i = 1, . . . , 3. Let ( i, ⌧ i), i = 1, 2, be F -morphisms from Ni to Ni+1. The function (, ⌧ ) : N1 ! N3, where = 2 1 and ⌧ = ⌧ 2 ⌧ 1 is a F -morphism.
This theorem is proved in [
With these morphisms we allow to map chains on cycles, as shown in Figure 1, representing an example of F -morphism from N1 to N2. The labels suggest the arrows of the morphism. Notice that the cardinality of the pre-images of the elements labelled by 1, b and 2 of N2 is one, while the place labelled by ac has two elements in its pre-image.
By adding a further constraint to the definition of F -morphisms, we get a subclass of morphisms which preserve cycles and chains.
Definition 14. Let Ni = (Si, Ti, Fi, M0i) be marked graphs for i = 1, 2. A Fˆmorphism from N1 to N2 is a F -morphism (, ⌧ ) with the following restriction: – for all s1 2 S1 such that (s1) = s2, the restriction of ⌧ to •s1 is a bijection from •s1 to •s2 and, similarly, the restriction of ⌧ to s1• is a bijection from s1• to s2•.
It is easy to see that Fˆ-morphisms are closed by composition. In fact, since we already know that a Fˆ-morphism (, ⌧ ) is a F -morphism, it is sufficient to prove that the additional constraint that characterizes Fˆ-morphisms is preserved by composition. We prove it simply by observing that the composition of two bijections is also a bijection.
The example in Figure 1 shows a F -morphism (, ⌧ ) which is not a Fˆmorphism: let s1 be the place of N1 labelled with c and let (s1) = s2 (therefore, s2 is the place of N2 labelled with ac). The restriction of ⌧ to s1• is not a bijection from s1• to s2•, in fact we have that s1• = ; 6 = s•. 2
In Figure 2 three examples of Fˆ-morphisms are shown: the first two of them, (( 1, ⌧ 1) : N1 ! N2 and ( 2, ⌧ 2) : N3 ! N4, respectively, Figure 2a and Figure 2b), allow us to observe that, using Fˆ-morphisms, it is possible to compress cycles and to identify chains; in the last one, (( 3, ⌧ 3) : N5 ! N6, Figure 2c), an identification of cycles is represented.
Let us now compare Fˆ-morphisms with another kind of morphisms defined
in [
We now show some interesting features of Fˆ-morphisms.
Theorem 2. Let Ni = (Si, Ti, Fi, M0i) be marked graphs, for i = 1, 2, joined by a Fˆ-morphism (, ⌧ ) : N1 ! N2. Let A1 and A2 be the incidence matrices of, respectively, N1 and N2. Let s0 2 S2 be a place of N2 such that 1(s0) = {s1, s2, . . . , sn}. For every transition t 2 T1 such that ⌧ (t) is defined, the following equation holds: n X A1(si, t) = A2(s0, ⌧ (t)). i=1 (1) Proof. In order to prove the theorem, we need to compare the incidence matrices of N1 and N2. Let Ai, i = 1, 2, be the incidence matrices of, respectively, N1 and N2. Because of the structure of a marked graph, it is possible to say that every row of Ai contain one 1 or -1 value or both of them, while the remaining entries of that row contain 0 values. Let us now consider n distinct places s1, . . . , sn of N1, such that (si) = s0, 1 i n. For each si 2 1(s0), if |•si| = 1 we denote tpre the input transition of |si| and, similarly, if |si•| = 1, we denote tpost the input transition of |si|. So, if such entries exist, A1(si, tpre) = 1 and A1(si, tpost) = 1. For definition of Fˆ-morphism, A2(s0, ⌧ (tpre)) = 1 and A2(s0, ⌧ (tpost)) = 1. Furthermore, since we consider marked graphs without self-loops and defines an injective and surjective partial function between the pre-conditions of transitions joined by ⌧ , for each sj 2 1(s0), j 6= i, we have A1(sj , tpre) = 0 and A1(sj , tpost) = 0. This proof about one generic s0 place of N2 can be extended to all the places of N2: so the theorem is proved.
The previous theorem allows us to introduce another interesting feature of Fˆ-morphisms. Intuitively, if two marked graphs N1 and N2 are joined by a Fˆmorphism (, ⌧ ) : N1 ! N2, the pre-images of any element of N2 contain the same number n of elements.
Theorem 3. For i = 1, 2, let Ni = (Si, Ti, Fi, M0i) be marked graphs and let (, ⌧ ) : N1 ! N2 be a Fˆ-morphism. Every x 2 P2 [ T2 has pre-image containing the same number n of elements.
Proof. Let Ai, i = 1, 2, be the incidence matrices of, respectively, N1 and N2. For every place s0 2 S2, if | 1(s0)| = n, then it is possible to find n distinct columns t1, . . . , tn of A1 such that A1(si, ti) = 1 or A1(si, ti) = 1, with si 2 1(s0). Let t0 be the input or output transition of p0; it is easy to verify that ⌧ 1(t0) = {t1, . . . , tn}. This means that, if the pre-image of a place of N2 contains n elements, the pre-images of its input and output transitions also contain n elements. We can extend this proof to every place of N2, thus proving the theorem.
We call n the reduction factor of (, ⌧ ). The Fˆ-morphism shown in Figure 2b has reduction factor 2, while the one in Figure 2c has reduction factor 3. 3.1
Fˆ-morphisms and behavioral relationships
We now want to show the relationship between the behaviors of two marked
graphs joined by a Fˆ-morphism. In this paper we assume that the behavior of
a system can be entirely described by means of its unfolding, according to the
definition given in [
Marked graphs are used to model deterministic systems. The absence of
choices in the behavior of deterministic systems can be used to observe that
the unfolding of a marked graph does not contain conflicts. In [
Let us now consider N -morphisms defined in [
Theorem 4. For i = 1, 2, let Ni = (Si, Ti, Fi, M0i) be marked graphs joined by a Fˆ-morphism (, ⌧ ) : N1 ! N2 and let (N10 , ⇡ 1) and (N20 , ⇡ 2) be, respectively, the unfoldings of N1 and N2. Then, there exists a N -morphism (, ⌘ ) : N10 ! N20 which makes the following diagram commute.
N!1 x ?? ⇡ 1 N!10 ,⌧ ,⌘
N2 x ?? ⇡ 2 N20
an isomorphism.
The proof of this theorem can be found in [
Fˆ-morphisms and their properties In this section we want to analyze some properties about liveness, boundedness, safeness, S and T-invariants of two marked graphs N1 and N2, joined by a Fˆmorphism (, ⌧ ) : N1 ! N2. We will first analyze behavioral properties and then structural invariants.
First of all, it is useful to observe that directed circuits are preserved by Fˆmorphisms. Intuitively, this means that, given two marked graphs N1 and N2 and a Fˆ-morphism (, ⌧ ) : N1 ! N2, if = x1x2 . . . xkx1 is a directed circuit of N1, xi 2 S1 [ T1, (, ⌧ ) maps on a directed circuit of N2.
In [
Fig. 3
The previous remarks allow to prove that Fˆ-morphisms preserve liveness. Theorem 5. For i = 1, 2, let Ni = (Si, Ti, Fi, M0i) be two marked graphs joined by a Fˆ-morphism (, ⌧ ) : N1 ! N2. If N1 is live, then N2 is also live.
Generally, liveness is not reflected by Fˆ-morphisms. In Figure 3a an example of Fˆ-morphism from N1 to N2 is shown. N2 is a live net, while N1 is not live: transitions labelled with 5 and 6 are never enabled.
Since we proved that there is a N -morphism between the unfoldings of two marked graphs joined by a Fˆ-morphism, it is easy to observe that Fˆ-morphisms also preserve occurrence sequences.
Theorem 6. Let Ni = (Si, Ti, Fi, M0i), i = 1, 2, be two marked graphs joined by a Fˆ-morphism (, ⌧ ) : N1 ! N2. Let ! = t1 . . . tk, be an occurrence sequence of N1 enabled at the initial marking M01. Therefore !0 = ⌧ (t1) . . . ⌧ (t2) is an occurrence sequence of N2 enabled at M02.
From the definition of Fˆ-morphism, it follows immediately that, if two marked graphs N1 and N2 are joined by a Fˆ-morphism (, ⌧ ) : N1 ! N2, for each place s of N2, the sum of the number of tokens placed by the initial marking of N1 in the elements of the pre-image of s is equal to the number of tokens placed by the initial marking of N2 in s. It is possible to extend this condition to every reachable marking of the two systems.
Theorem 7. For i = 1, 2, let Ni = (Si, Ti, Fi, M0i) be two marked graphs joined by a Fˆ-morphism (, ⌧ ) : N1 ! N2. Let ! = t1 . . . tk be an occurrence sequence of N1 enabled at M01 such that M01! ! M . Then, !0 = ⌧ (t1) . . . ⌧ (tk) is an occurrence sequence of N2 enabled at M02 such that M02 !!0 s0 2 S2, the following equation holds
M 0(s0) =
X s2 1(s0)
M (s).
Using Theorem 7 it is easy to prove that boundedness is preserved by Fˆmorphisms.
Theorem 8. For i = 1, 2, let Ni = (Si, Ti, Fi, M0i) be two marked graphs joined by a Fˆ-morphism (, ⌧ ) : N1 ! N2. If N1 is bounded, then N2 is also bounded. So Fˆ-morphisms preserve boundedness but, generally, they do not reflect it. The Fˆ-morphism from N1 to N2 represented in Figure 3a does not preserve boundedness: N2 is a 1-bounded net, while in N1 the places labelled with e and f can be filled with an infinite number of tokens.
Note that the reflection of boundedness is obtained if (, ⌧ ) is total. Theorem 9. For i = 1, 2, let Ni = (Si, Ti, Fi, M0i) be two marked graphs joined by a Fˆ-morphism (, ⌧ ) : N1 ! N2 such that is total. If N2 is bounded, then
Proof. Each place of N1 is mapped on a place of N2. If N2 is bounded, by theorem 7 it is easy to see that N1 is also bounded.
Notice that, in general, safeness (1-boundedness) is not preserved. Let us consider the example shown in Figure 3b: there is a Fˆ-morphism from N3 to N4 and, while N1 is a safe net, N2 is 2-bounded.
We now focus on some properties about S and T-invariants of two marked graphs N1 and N2 joined by a Fˆ-morphism (, ⌧ ) : N1 ! N2. It is possible to prove that Fˆ-morphisms reflect S-invariants. In order to obtain such result, we need to order the rows of the incidence matrix A1 of N1 in the following way. Let A2 be the incidence matrix of N2 and let n be the reduction factor of ( ). Given the first row of A2, representing the place s of N2, let us consider the n rows of A1 corresponding to places of N1 mapped by on s. We will put such rows in the first n positions of the matrix. The same procedure can be used to order the remaining rows of A1. The rows corresponding to places not mapped by will occupy the last positions of A1. Theorem 10. For i = 1, 2, let Ni = (Si, Ti, Fi, M0i) be two marked graphs joined by a Fˆ-morphism (, ⌧ ) : N1 ! N2. Let A1, A2 and n be, respectively, the incidence matrices of N1 and N2, ordered as seen before, and the reduction factor of (, ⌧ ). If I2 = (↵ 1↵ 2 . . . ↵ P ), with ↵ j 2 N and P = |S2|, is a S-invariant for
The previous theorem is proved in [
Fˆ-morphisms reflect S-invariants but do not preserve them. The S-invariant IA = (0100111) for N1 in Figure 4 can not be used to build a corresponding Sinvariant for N2. It is impossible to assign to each place of N2 the weight of the elements of its pre-image. For example, let s be the place of N2 labelled with bd: IA assigns a different weights to the elements of 1(s). IB, built by assigning to each place of N2 the sum of the weights of the elements of its pre-image, is not a S-invariant of N2.
Regarding T-invariants, we observe that, in marked graphs, an occurrence sequence leads back to the initial marking if and only if it fires every transition an equal number of times. Then, since Fˆ-morphisms are surjective, by Theorem 7 they preserve T-invariants.
In general, T-invariants are not reflected by Fˆ-morphisms. For instance, let us consider the example in Figure 4. J 2T = (11) is a T-invariant for N2. For each transition t of N2, we assign to the elements of its pre-image the weight given by J 2T to t, and we use 0s for the other transitions of N1. So, we obtain J 1T = (011110), which is not a T-invariant for N1. 5
Remarks and conclusions
We have introduced F - and Fˆ-morphisms, new kinds of morphisms on marked
graphs, a basic class of Petri nets. These morphisms can be used as a formal
technique to deal with a kind of abstraction on marked graphs, consisting in the
folding of cycles and the identification of chains. We have also proved that the
unfoldings of two systems joined by a Fˆ-morphism are joined by a N -morphism
(see [
We now plan to define a new operation for the composition of marked graphs
driven by Fˆ-morphisms mapping the components on a net which works as an
interface, similarly to what described in [