Morphisms on Marked Graphs Luca Bernardinello, Lucia Pomello, and Stefano Scaccabarozzi Dipartimento di Informatica, Sistemistica e Comunicazione, Università degli studi di Milano - Bicocca, Viale Sarca, 336 - Edificio U14 - I-20126 Milano, Italia luca.bernardinello@unimib.it Abstract. Many kinds of morphisms on Petri nets have been defined and studied. They can be used as formal techniques supporting refine- ment/abstraction of models. In this paper we introduce a new notion of morphism on marked graphs, a class of Petri nets used for the rep- resentation 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. Keywords: Petri nets, marked graphs, morphisms, model abstraction, preservation of behavioral properties 1 Introduction When working on concurrent and distributed systems, the dimensions and com- plexity 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, [1], [2], [3], [4] and [5]) several kinds of morphism on different classes of Petri nets have been introduced. In this paper we propose a new definition of morphism on marked graphs, a class of Petri nets often used for representing systems having deterministic behavior. These so called F -morphisms and the subclass of F̂ -morphisms constitute a formal instrument which can be used to obtain a kind of abstraction of marked graphs. Some kinds of morphisms defined in the literature, such as ↵-morphisms ([5]), allow to collapse part of the initial model on a single place or a single transition in order to obtain the abstract system. Differently, F̂ -morphisms map places on single places and transitions on single transitions, preserving the environment of each mapped element. Instead of collapsing portions of the detailed model into a single element, the abstraction is here obtained by “folding” cycles and 114 PNSE’14 – Petri Nets and Software Engineering identifying chains and cycles. Both these elements still remain in the reduced model. 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 unfold- ings. These notions will be used in the next chapters to study important aspects of F -morphisms. 2.1 Petri nets We first start introducing the notion of net as seen in [6], with some adjustements. Definition 1. A net is a triple N = (S, T, F ), where – S is a set of places, – T is a set of transitions such that S \ T = ;, – F is a set of directed arcs (flow relation), F ✓ (S ⇥ T ) [ (T ⇥ S). 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 • x = {y 2 S [ T | (y, x) 2 F } while its post-set is defined by 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 x•i 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 [ x•i 1 for each i (1  i  k). Such undirected path leads from x0 to L. Bernardinello et al.: Morphisms on Marked Graphs 115 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 . . . xk x0 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 8 >M (s) 1 if s 2 • t \ t• , < 0 M (s) = 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 t1 t2 tk M ! M1 ! ... ! Mk . ! In this case we write M ! Mk , where ! = t1 . . . tk . The empty sequence E is E enabled at any marking M and satisfies M ! 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 Behavioral properties 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 ([7]) which will be used in the next sections. 116 PNSE’14 – Petri Nets and Software Engineering Definition 3. A Petri net (N, M0 ) is said to be k-bounded or simply bounded 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. Definition 4. A Petri net (N, M0 ) is said to be live (or equivalently M0 is 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 Incidence matrix and structural invariants Definitions recalled in this section are taken from [7], with some adaptations. Definition 5. Let (N, M0 ) be a Petri net with n transitions and m places. Its incidence matrix A = [aij ] is an m ⇥ n matrix of integers and its typical entry is given by aij = a+ ij aij where a+ij = 1 if there is an arc of N going from transition j to its post-condition i, otherwise a+ij = 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. Definition 6. Let N be a net and let A be its incidence matrix. A vector I : 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. Definition 7. Let N be a net and let A be its incidence matrix. A vector J : T ! Z is a T-invariant for N iff it is a solution of: AJ T = 0. 2.4 Branching processes and unfoldings 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 [7]. From now on, we will only consider Petri nets such that, for every transition t, • t and t• are finite sets and, moreover, we assume them to be nonempty. Furthermore, we do not allow more than one token on a place in the initial marking. Such constraints do not result too restrictive with respect to the behavior of the studied systems. L. Bernardinello et al.: Morphisms on Marked Graphs 117 Definition 8. Let N = (S, T, F, M0 ) be a Petri net. For x, y 2 S [ T we say that x precedes y if there is a (possibly empty) directed path from x to y in N . N is finitary if for every y 2 S [ T the set {x 2 S [ T | x precedes y} is finite. 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 [8]. Intu- itively, a homomorphism from net N1 to net N2 formalizes the fact that N1 can be folded onto a part of N2 , or, in other words, that N1 can be obtained by partially unfolding a part of N2 . 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 = (S 0 , 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 [9], a notion of homomorphism between branching processes of the same net N is also defined. Injective homomorphisms define a partial order for the branching processes of N , called approximation. The set of the isomorphism classes of the branching processes of N , together with approximation, form a complete lattice. The least upper bound of such lattice is the unfolding of N . 118 PNSE’14 – Petri Nets and Software Engineering 3 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. Remark From now on, we only consider connected marked graphs without 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 ) = ; = (t•1 ), – 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 t•1 is an injective and surjective partial function from t•1 to t•2 , – for every s0 2 S2 X M02 (s0 ) = M01 (s). 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 [10]. The identity function 1N = (idS , idT ) is a F - morphism, where idS : S ! S and idT : T ! T are the total identity functions. The composition is associative. Hence, the family of F -morphisms, together with marked graphs, form a category which takes the name of Marked Graph System, denoted MGS. 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: L. Bernardinello et al.: Morphisms on Marked Graphs 119 Fig. 1 – 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 s•1 is a bijection from s•1 to s•2 . 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 s•1 is not a bijection from s•1 to s•2 , in fact we have that s•1 = ; = 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 cy- cles 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 [2], N -morphisms, corresponding to a kind of partial simulation. We want to do this since we will later show that we can always find a N -morphism be- tween the unfoldings of two marked graphs joined by a F̂ -morphism. First of all, N -morphisms are defined on elementary net systems, while F̂ -morphisms are defined on marked graphs. N -morphisms define a relation between the places of the joined systems, such that its inverse is a partial function. Differently, F̂ -morphisms allow two places to have the same image. Furthermore, for F̂ - morphisms the mapping between events is surjective, while N -morphisms do not require such constraint. The last main difference is that, if two places s and s0 of different elementary net systems are joined by a N -morphism, s belongs to the initial case of the first system if and only if s0 is in the initial case of the second one, whereas whith F̂ -morphism a place of the starting system contain- 120 PNSE’14 – Petri Nets and Software Engineering (a) (b) (c) Fig. 2 L. Bernardinello et al.: Morphisms on Marked Graphs 121 ing no tokens in the initial marking can be mapped on a place containing tokens. 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 ma- trices of, respectively, N1 and N2 . Let s0 2 S2 be a place of N2 such that (s ) = {s1 , s2 , . . . , sn }. For every transition t 2 T1 such that ⌧ (t) is defined, 1 0 the following equation holds: n X A1 (si , t) = A2 (s0 , ⌧ (t)). (1) i=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 (s ), if |• si | = 1 we denote tpre 1 0 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 (s ), j 6= i, we have A1 (sj , tpre ) = 0 and 1 0 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 dis- tinct columns t1 , . . . , tn of A1 such that A1 (si , ti ) = 1 or A1 (si , ti ) = 1, with si 2 (s ). Let t0 be the input or output transition of p0 ; it is easy to verify 1 0 that ⌧ (t ) = {t1 , . . . , tn }. This means that, if the pre-image of a place of N2 1 0 contains n elements, the pre-images of its input and output transitions also con- tain 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. 122 PNSE’14 – Petri Nets and Software Engineering 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 [9]. For this reason, from now on, we will only consider marked graphs with one technical restriction: in the initial marking there should not be more than one token on each place. 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 [9] the unfolding of a net N is formally defined as a pair (N 0 , ⇡), where N 0 is an occurrence net and ⇡ is a homomorphism from N 0 to N . An occurrence net containing no conflicts is called causal net, which is an acyclic marked graph. Let us now consider N -morphisms defined in [2] for elementary net systems, and compared to F̂ -morphisms in the previous subsection. Causal nets, used to represent the unfoldings of marked graphs, form a subclass of elementary net systems. This allows us to explicit the relationship between the behaviors of two marked graphs joined by a total F̂ -morphism. 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. ,⌧ N1 ! N2 x x ?⇡ ?⇡ ? 1 ? 2 ,⌘ N10 ! N20 In particular, 1 is an injective partial function and, if ( , ⌧ ) is total, ( , ⌘) is an isomorphism. The proof of this theorem can be found in [10], together with the necessary theoretical notions. Such proof uses an improved version of McMillan’s unfolding algorithm (see [11]) with some modifications. 4 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. L. Bernardinello et al.: Morphisms on Marked Graphs 123 4.1 Analysis of behavioral properties 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 = x1 x2 . . . xk x1 is a directed circuit of N1 , xi 2 S1 [ T1 , ( , ⌧ ) maps on a directed circuit of N2 . In [7] marked graphs are defined as Petri nets N = (S, T, F, M0 ) in which, for each s 2 S, it holds |• s| = |s• | = 1. Then, they prove that a marked graph N is live iff the initial marking places at least one token on each directed circuit in N . In this paper we consider a more general notion of marked graph: for each place s we have |• s|  1 and |s• |  1. It is well known (for example, see [7]) that, given a marked graph N such that |• s| = 1 for each place s, N is live if and only if the initial marking places at least one token on each directed circuit in N . (a) (b) 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. 124 PNSE’14 – Petri Nets and Software Engineering 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 !0 occurrence sequence of N2 enabled at M02 such that M02 ! M 0 and, for each s0 2 S2 , the following equation holds X M 0 (s0 ) = M (s). s2 1 (s0 ) 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 N1 is also bounded. 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. L. Bernardinello et al.: Morphisms on Marked Graphs 125 4.2 On structural invariants 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 . Fig. 4 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 I 2 = (↵1 ↵2 . . . ↵P ), with ↵j 2 N and P = |S2 |, is a S-invariant for 126 PNSE’14 – Petri Nets and Software Engineering N2 , then n times n times n times z }| { z }| { z }| { I 1 = (↵1 ↵1 . . . ↵1 ↵2 ↵2 . . . ↵2 . . . ↵P ↵P . . . ↵P 0 . . . 0) is a S-invariant for N1 . The previous theorem is proved in [10]. Let us now consider the F̂ -morphism ( , ⌧ ) : N1 ! N2 shown in Figure 4, having reduction factor n = 2. The incidence matrix of N1 is ordered as explained. I 2 = (11) is a S-invariant for N2 . The corresponding S-invariant for N1 is built by taking n times each single value of I 2 as the first components and adding 0s in the remaining positions. Thus, we obtain I 1 = (1111000). F̂ -morphisms reflect S-invariants but do not preserve them. The S-invariant I A = (0100111) for N1 in Figure 4 can not be used to build a corresponding S- invariant 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: I A assigns a different weights to the elements of 1 (s). I B , 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 T2 = (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 T2 to t, and we use 0s for the other transitions of N1 . So, we obtain J T1 = (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 [2]). We have finally shown that liveness, boundedness and T-invariants are preserved by such morphisms, while S-invariants are reflected. 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 [12], [13] for N̂ -morphisms. We also intend to extend the theory related to F -morphisms to other classes of Petri nets, such as persistent, free choice and Place/Transition Petri nets, thus applying such functions to systems having conflicts. Finally, we want to apply F̂ -morphisms to models representing real systems having deterministic behavior (such as, for L. Bernardinello et al.: Morphisms on Marked Graphs 127 example, manufacturing systems or cyclic processes) to formally analyze them by using a step-by-step approach based on different levels of refinement of the modelled system. Acknowledgement. This work was partially supported by MIUR and by MIUR-PRIN 2010/2011 grant ‘Automi e Linguaggi Formali: Aspetti Matematici e Applicativi’, code H41J12000190001. References 1. Desel, J., Merceron, A.: Vicinity respecting homomorphisms for abstracting system requirements. Transactions on Petri Nets and Other Models of Concurrency 4 (2010) 1–20 2. Nielsen, M., Rozenberg, G., Thiagarajan, P.S.: Elementary transition systems. Theor. Comput. Sci. 96(1) (1992) 3–33 3. Padberg, J., Urbásek, M.: Rule-based refinement of Petri nets: A survey. In Ehrig, H., Reisig, W., Rozenberg, G., Weber, H., eds.: Petri Net Technology for Communication-Based Systems. Volume 2472 of Lecture Notes in Computer Sci- ence., Springer (2003) 161–196 4. Winskel, G.: Petri nets, algebras, morphisms, and compositionality. Inf. Comput. 72(3) (1987) 197–238 5. Bernardinello, L., Mangioni, E., Pomello, L.: Local state refinement and composi- tion of elementary net systems: An approach based on morphisms. T. Petri Nets and Other Models of Concurrency 8 (2013) 48–70 6. Desel, J., Reisig, W.: Place/Transition Petri Nets. In Reisig, W., Rozenberg, G., eds.: Petri Nets. Volume 1491 of Lecture Notes in Computer Science., Springer (1996) 122–173 7. Murata, T.: Petri nets: Properties, analysis and applications. Proceedings of the IEEE 77(4) (April 1989) 541–580 8. Winskel, G.: Event structures. In Brauer, W., Reisig, W., Rozenberg, G., eds.: Ad- vances in Petri Nets. Volume 255 of Lecture Notes in Computer Science., Springer (1986) 325–392 9. Engelfriet, J.: Branching processes of Petri nets. Acta Inf. 28(6) (1991) 575–591 10. Bernardinello, L., Pomello, L., Scaccabarozzi, S.: Morphisms on Marked Graphs (Extended Version). http://www.mc3.disco.unimib.it/pub/bps2014ext.pdf (2014) 11. Esparza, J., Römer, S., Vogler, W.: An Improvement of McMillan’s Unfolding Algorithm. Formal Methods in System Design 20(3) (2002) 285–310 12. Bernardinello, L., Monticelli, E., Pomello, L.: On preserving structural and be- havioural properties by composing net systems on interfaces. Fundam. Inform. 80(1-3) (2007) 31–47 13. Pomello, L., Bernardinello, L.: Formal tools for modular system development. In Cortadella, J., Reisig, W., eds.: ICATPN. Volume 3099 of Lecture Notes in Computer Science., Springer (2004) 77–96