Local state refinement on Elementary Net Systems: an approach based on morphisms Luca Bernardinello, Elisabetta Mangioni, and Lucia Pomello Dipartimento di Informatica Sistemistica e Comunicazione, Università degli studi di Milano - Bicocca, Viale Sarca, 336 - Edificio U14 - I-20126 Milano, Italia mangioni@disco.unimib.it Abstract. In the design of concurrent and distributed systems, mod- ularity and refinement are basic conceptual tools. We propose a notion of refinement/abstraction of local states for a basic class of Petri Nets, associated with a new kind of morphisms. The morphisms, from a re- fined system to an abstract one, associate suitable subnets to abstract local states. The main results concern behavioural properties preserved and reflected by the morphisms. In particular, we focus on the condi- tions under which reachable markings are preserved or reflected, and the conditions under which a morphism induces a bisimulation between net systems. Keywords: Elementary Net Systems, morphisms, local state refinement 1 Introduction Refinement and composition of modules are among the basic conceptual tools of a system designer. Several formal approaches are available. One of the main challenges consists in developing languages and methods allowing to derive prop- erties of the refined system from properties of the abstract one. We propose an approach based on Petri nets, where the refinement of a model is supported by so-called α-morphisms on the class of Elementary Net Systems. We focus on the refinement of local states. Given a net N2 , interpreted as an abstract description of a system, the local states of N2 are replaced by subnets, giving a new net, say N1 , so that there is an α-morphism from N1 to N2 . Using morphisms to formalize the relation between a refined net and a more abstract one is not new. Most approaches, in Petri net theory, are based on transition refinement and, less frequently, on place refinement; for a survey, see [5]. Another survey paper, [9], describes a set of techniques which allow to refine transitions in Place/transition nets, so that the relation between the abstract net and its refinement is given by a morphism. There, the emphasis is on refinement rules that preserve specific behavioural properties, within the wider context of general transformation rules on nets. 142 PNSE’12 – Petri Nets and Software Engineering A very general class of morphisms, interpreted as abstraction of system re- quirements, with less focus on strict preservation of behavioural properties, is defined in [6]. The approach we present in this paper is similar in spirit to the refinement operation proposed in [8]. In that approach, refinement is defined on transition systems, but is strictly related to refinement of local states in nets, through the notion of region. α-morphisms can be seen as a special case of the morphisms introduced by Winskel in [13], as it will be formally shown in Section 5. Other morphisms introduced in the literature on the same line of Winskel morphisms, are the ones given in [12] and [1]. Our approach is motivated by the attempt to define a refinement opera- tion preserving behavioural properties on the basis of structural and only local behavioural constraints. The additional restrictions, with respect to general mor- phisms, aim, on one hand, to capture typical features of refinements, and on the other hand to ensure that some behavioural properties of the abstract model still hold in the refined model. Moreover, in [2], we use α-morphisms as a means supporting a composition operator defined through an interface, following the same approach proposed in [4]. In the rest of this section, the main ideas of refinement and related morphisms are explained by means of a simple example. In Section 2 we collect preliminary definitions related to Petri nets which are used in the rest of the paper. Section 3 contains the definition of α-morphisms and the main results of the paper: in particular, we show that reachable markings are preserved, we characterize the local conditions under which reachable markings are reflected, i.e.: under which the counterimage of reachable markings are reachable markings, and such that morphisms induce a bisimulation between the related net systems. In Section 5 we compare α-morphisms with Winskel’s morphisms. Finally, in Section 6 we discuss some critical issues in our approach and suggest possible developments. Most proofs are given in an extended version of the present paper [3]. 1.1 An example The example presented in this section aims at explaining, informally, how α- morphisms support refinement of local states in Elementary Net Systems. The morphism maps nodes of a refined system, N1 , on a more abstact one, N2 . The Elementary Net System shown in Fig. 1 represents an abstract view of the interaction between a student and an University secretariat office. A student may ask the office either to emit an English proficiency certificate or to admit her to the final exam. Note that, at this level of abstraction, the model does not distinguish a positive answer from a negative one. Suppose that the local state inspect_request corresponds to the actual inspection of the request by a Faculty board, which delivers the decision to the secretariat. We might want to refine formal_check, in order to distinguish two cases: positive answer and negative answer. L. Bernardinello et al.: Local state refinement 143 Fig. 1: Abstract view (N2 ) The actual decision has been taken in state inspect_request, so the refinement of formal_check requires splitting the event Faculty_decision, thus reflecting the choice between the two answers. The result of the refinement is shown in Fig. 2, Fig. 2: Refined model (N1 ) where the subnet refining formal_check is enclosed in a shaded oval. Note that the operation has required also splitting the outgoing transitions, in order to reflect the alternative outcomes. 2 Preliminary definitions In this section, we recall the basic definitions of net theory, in particular Ele- mentary Net Systems [11], and bisimulation [7]. We will use the symbol ↓ to denote the restriction of a function on a subset of its domain. 2.1 Petri Nets In net theory, models of distributed systems are based on objects called nets which specify local states, local transitions and the relations among them. A net is a triple N = (B, E, F ), where B is a set of conditions or local states, E is a 144 PNSE’12 – Petri Nets and Software Engineering set of events or transitions such that B ∩ E = ∅ and F ⊆ (B × E) ∪ (E × B) is the flow relation. We adopt the usual graphical notation: conditions are represented by circles, events by boxes and the flow relation by arcs. The set of elements of a net will be denoted by X = B ∪ E; we allow nets with isolated elements. The preset of an element x ∈ X is • x = {y ∈ X|(y, x) ∈ F }; the postset of x is x• = {y ∈ X|(x, y) ∈ F }; the neighbourhood of x is given by • x• = • x ∪ x• . These notations are extended to subsets of elements in the usual way. For any net N we denote the in-elements of N by N = {x ∈ XN : • x = ∅} and the out-elements of N by N = {x ∈ XN : x• = ∅}. A net is simple if for all x, y ∈ X, if • x = • y and x• = y • , then x = y. A net N 0 = (B 0 , E 0 , F 0 ) is a subnet of N = (B, E, F ) if B 0 ⊆ B, E 0 ⊆ E, and F = F ∩ ((B 0 × E 0 ) ∪ (E 0 × B 0 )). Given a subset of elements A ⊆ X, we say that 0 N (A) is the subnet of N identified by A if N (A) = (B ∩ A, E ∩ A, F ∩ (A × A)). A State Machine is a connected net such that each event e has exactly one input condition and exactly one output condition: ∀e ∈ E, |• e| = |e• | = 1. Elementary Net (EN) Systems are a basic system model in net theory. An Elementary Net System is a quadruple N = (B, E, F, m0 ), where (B, E, F ) is a net such that B and E are finite sets, self-loops are not allowed, isolated elements are not allowed, and the initial marking is m0 ⊆ B. The elements in the initial marking are interpreted as the conditions which are true in the initial state. A subnet of an EN System N identified by a subset of conditions A and all its pre and post events, N (A ∪ • A• ), is a Sequential Component of N if N (A ∪ • A• ) is a State Machine and if it has only one token in the initial marking. An EN System is covered by Sequential Components if every condition of the net belongs to at least a Sequential Component. In this case we say that the system is State Machine Decomposable (SMD). The behaviour of EN Systems is defined through the firing rule, which spec- ifies when an event can occur, and how event occurrences modify the holding of conditions, i.e. the state of the system. Let N = (B, E, F, m0 ) be an EN System, e ∈ E and m ⊆ B. The event e is enabled at m, denoted m [ei, if • e ⊆ m and e• ∩ m = ∅; the occurrence of e at m leads from m to m0 , denoted m [ei m0 , iff m0 = (m \ • e) ∪ e• . Let  denote the empty word in E ∗ . The firing rule is extended to sequences of events by setting m [i m and ∀e ∈ E, ∀w ∈ E ∗ , m [ewi m0 = m [ei m00 [wim00 ; w is called firing sequence. A subset m ⊆ B is a reachable marking of N if there exists a w ∈ E ∗ such that m0 [wi m. The set of all reachable markings of N is denoted by [m0 i. An EN System is contact-free if ∀e ∈ E, ∀m ∈ [m0 i: • e ⊆ m implies e• ∩ m = ∅. An EN System covered by Sequential Components is contact-free. An event is called dead at a marking m if it is not enabled at any marking reachable from m. A reachable marking m is called dead if no event is enabled at m. An Elementary Net System is deadlock-free if no reachable marking is dead. L. Bernardinello et al.: Local state refinement 145 2.2 Unfoldings The semantics of an EN System can be given as its unfolding. The unfolding is an acyclic net, possibly infinite, which records the occurrences of its elements in all possible executions. Definition 1. Let N = (B, E, F ) be a net, and let x, y ∈ X. We say that x and y are in conflict, denoted by x #N y, if there exist two distinct events ex , ey ∈ E such that ex F ∗ x, ey F ∗ y, and • ex ∩ • ey 6= ∅. Definition 2. An occurrence net is a net N = (B, E, F ) satisfying: 1. if e1 , e2 ∈ E, e1 • ∩ e2 • 6= ∅ then e1 = e2 ; 2. F ∗ is a partial order, 3. for any x ∈ X, {y : yF ∗ x} is finite; 4. #N is irreflexive, 5. the minimal elements with respect to F ∗ are conditions. A branching process of N is an occurrence net whose elements can be mapped to the elements of N . Definition 3. Let N = (B, E, F, m0 ) be an EN System, and Σ = (P, T, G) be an occurrence net. Let π : P ∪ T → B ∪ E be a map. The pair (Σ, π) is a branching process of N if: – π(P ) ⊆ B, π(T ) ⊆ E; – π restricted to the minimal elements of Σ is a bijection on m0 ; – for each t ∈ T , π restricted to • t is injective and π restricted to t• is injective; – for each t ∈ T , π(• t) = • (π(t)) and π(t• ) = (• π(t)). The unfolding of an EN System N , denoted by Unf (N ), is the maximal branching process of N , namely the unique branching process such that any other branching process of N is isomorphic to a subnet of Unf (N ). The map associated to the unfolding will be denoted u and called folding. 2.3 Bisimulations Bisimulation relations have been introduced as equivalence notions with respect to event observation [7]. We define the observability of events of a system by using a labelling function which associates the same label to different events, when viewed as equal by an observer, and the label τ to unobservable events. Definition 4. Let N = (B, E, F, m0 ) be an EN System, l : E → L ∪ {τ } be a labelling function where L is the alphabet of observable actions and τ 6∈ L the unobservable action. Let  denote the empty word both of E ∗ and L∗ . The function l is extended to a homomorphism l : E ∗ → L∗ in the following way: l() =  146 PNSE’12 – Petri Nets and Software Engineering ( ∗ l(e)l(w) if l(e) 6= τ ∀e ∈ E, ∀w ∈ E , l(ew) = l(w) if l(e) = τ The pair (N, l) is called Labelled EN System. Let m, m0 ∈ [m0 i and a ∈ L ∪ {} then: – a is enabled at m, denoted m (ai, iff ∃w ∈ E ∗ : l(w) = a and m [wi; – if a is enabled at m, then the occurrence of a can lead from m to m0 , denoted m (ai m0 , iff ∃w ∈ E ∗ : l(w) = a and m [wi m0 . We define weak bisimulation as a relation between reachable markings of Labelled EN Systems [10]. Definition 5. Let Ni = (Bi , Ei , Fi , mi0 ) be an EN System for i = 1, 2, with the labelling function li : Ei → L ∪ {τ }. Then (N1 , l1 ) and (N2 , l2 ) are weakly bisimilar, denoted (N1 , l1 ) ≈ (N2 , l2 ), iff ∃r ⊆ m10 × m20 such that: – (m10 , m20 ) ∈ r; – ∀(m1 , m2 ) ∈ r, ∀a ∈ L ∪ {} it holds ∀m01 : m1 (ai m01 ⇒ ∃m02 : m2 (ai m02 ∧ (m01 , m02 ) ∈ r and (vice versa) ∀m02 : m2 (ai m02 ⇒ ∃m01 : m1 (ai m01 ∧ (m01 , m02 ) ∈ r Such a relation r is called weak bisimulation. For short in the rest of the paper we will use the term bisimulation instead of weak bisimulation. 3 A class of morphisms In this section we present the formal definition of α-morphisms for State Machine Decomposable Elementary Net Systems (SMD-EN Systems), and discuss some of their properties, particularly with respect to the preservation of both structural and behavioural properties. We start by defining a more general class of morphisms, and then present the more specific restrictions. Definition 6. Let Ni = (Bi , Ei , Fi , mi0 ) be a SMD-EN System, for i = 1, 2. An ω-morphism from N1 to N2 is a total surjective map ϕ : X1 → X2 such that: 1. ϕ(B1 ) = B2 ; 2. ϕ(m10 ) = m20 ; 3. ∀e1 ∈ E1 , if ϕ(e1 ) ∈ E2 , then ϕ(• e1 ) = • ϕ(e1 ) and ϕ(e1 • ) = ϕ(e1 )• ; 4. ∀e1 ∈ E1 , if ϕ(e1 ) ∈ B2 , then ϕ(• e1 • ) = {ϕ(e1 )}; L. Bernardinello et al.: Local state refinement 147 We require that the map is total and surjective because N1 refines the abstract model N2 , and any abstract element must be related to its refinement. In particular, a subset of nodes can be mapped on a single condition b2 ∈ B2 ; in this case, we will call bubble the subnet identified by this subset, and denote it by N1 (ϕ−1 (b2 )); if more than one element is mapped on b2 , we will say that b2 is refined by ϕ. Definition 7. Let Ni = (Bi , Ei , Fi , mi0 ) be a SMD-EN System, for i = 1, 2. An α-morphism from N1 to N2 is an ω-morphism satisfying 5. ∀b2 ∈ B2 (a) N1 (ϕ−1 (b2 )) is an acyclic net; (b) ∀b1 ∈ N1 (ϕ−1 (b2 )), ϕ(• b1 ) ⊆ • b2 and (• b2 6= ∅ ⇒ • b1 6= ∅); (c) ∀b1 ∈ N1 (ϕ−1 (b2 )) , ϕ(b1 • ) = b2 • ; (d) ∀b1 ∈ ϕ−1 (b2 ) ∩ B1 , (b1 6∈ N1 (ϕ−1 (b2 )) ⇒ ϕ(• b1 ) = {b2 }) and (b1 6∈ N1 (ϕ−1 (b2 )) ⇒ ϕ(b1 • ) = {b2 }); (e) ∀b1 ∈ ϕ−1 (b2 ) ∩ B1 , there is a sequential component NSC of N1 such that b1 ∈ BSC and ϕ−1 (• b2 • ) ⊆ ESC . (a) Pre events of an in-condition (b) Post events of an out-condition Fig. 3: Pre and post event of a bubble As we can see in Fig. 3a and 3b, in-conditions and out-conditions have dif- ferent constraints, 5b and 5c respectively. As required by 5c, we do not allow that choices, which are internal to a bubble, constrain a final marking of that bubble: i.e., each out-condition of the bubble must have the same choices of the condition it refines. Instead, pre-events do not need this strict constraint (5b): hence it is sufficient only that pre-events of any in-condition are mapped on a subset of the pre-events of the condition it refines. For example, in this par- ticular case, we know that the choice between e1 and f1 of Figure 3a is made before the bubble, and this is implied also by the requirement 5e) on sequential components. Moreover, the conditions that are internal to a bubble must have pre-events and post-events which are all mapped to the refined condition b2 , as required by 5d. 148 PNSE’12 – Petri Nets and Software Engineering By requirement 5e, events in the neighbourhood of a bubble are not concur- rent, as their images. Within a bubble, there can be concurrent events; however, post events are in conflict, and firing one of them will empty the bubble, as shown in Lemma 1 below. The α-morphisms are closed by composition, the identity function on X is an α-morphism, and the composition is associative. Hence, the family of SMD-EN Systems together with α-morphisms forms a category. The partition of elements of N1 induced by an α-morphism ϕ : N1 → N2 defines the structure of a net: Definition 8. Let Ni = (Bi , Ei , Fi , mi0 ) be a SMD-EN System, for i = 1, 2. Let ϕ be an α-morphism from N1 to N2 . Then ϕ defines an equivalence relation on X1 , where the equivalence class of x ∈ X1 is [x] = {y ∈ X1 | ϕ(y) = ϕ(x)}. The quotient of N1 with respect to α is N1 /ϕ = (B1 /ϕ, E1 /ϕ, F1 /ϕ, m10 /ϕ), where – B1 /ϕ = {[x] : x ∈ X1 , ϕ(x) ∈ B2 }; – E1 /ϕ = {[x] : x ∈ X1 , ϕ(x) ∈ E2 }; – F1 /ϕ = {([x], [y]) : x, y ∈ X1 , x 6= y, ∃(x, y) ∈ F1 }; – m10 /ϕ = {[x] : x ∈ m10 }. By a simple verification [3], the quotient of N1 , N1 /ϕ, is a SMD-EN System isomorphic to N2 . 4 Properties preserved and reflected by α-morphisms Since we consider SMD-EN Systems, it is natural to ask whether α-morphisms preserve and reflect sequential components. Let ϕ be an α-morphism from N1 to N2 . We know that, if a condition b2 belongs to a sequential component, then also its pre- and post-events belong to the same sequential component. Hence, if b2 is refined by a bubble N1 (ϕ−1 (b2 )), by the requirement 5e) of α-morphisms any condition of the bubble belongs to a sequential component containing any event in ϕ−1 (• b2 • ). This allows one to say that the sequential components of N2 are reflected by ϕ, in the sense that the inverse image of a sequential component is covered by sequential components. Lemma 1. Let ϕ : N1 → N2 be an α-morphism. Let NSC2 be a sequential component of N2 . Then ϕ−1 (NSC2 ) is covered by sequential components, each one containing all the inverse image of the neigh- bourhood of each condition of NSC2 . Sequential components are not preserved, as we can see in Fig. 4. The se- quential component of N1 generated by {ϕ−1 (b1 ), b5−1 , b6−1 } is such that its image {b1 , b5 , b6 } is not a sequential component of N2 . The idea driving our interpretation of bubble is that the subnet corresponding to a condition “behaves” in the same way as the condition it refines. In a SMD- EN System, each condition at any time can be true or false. It is not possible that L. Bernardinello et al.: Local state refinement 149 Fig. 4: Two SMD-EN Systems related by an α-morphism this condition is partially true or partially false; hence, also the bubble should behave like this. The next lemma states that firing an output event of a bubble empties the bubble, and that no input event of a bubble is enabled whenever a token is inside the bubble. Lemma 2. Let ϕ : N1 → N2 be an α-morphism. Then:  1. Let e1 ∈ E1 , b2 ∈ B2 : e1 ∈ ϕ−1 (b2 • ); m1 , m01 ∈ m10 : m1 [e1 i m01 , then m01 ∩ ϕ−1 (b2 ) = ∅.  2. Let e1 ∈ E1 , b2 ∈ B2 : e1 ∈ ϕ−1 (• b2 ); m1 , m01 ∈ m10 : m1 [e1 i m01 then m1 ∩ ϕ−1 (b2 ) = ∅. Proof. Take a marking m1 in which a condition b1 ∈ ϕ−1 (b2 ) is marked. We know by Def. 7, point 5e) that there exists a sequential component SC of N1 such that b1 ∈ BSC and ϕ−1 (• b2 • ) ⊆ ESC . 1. By contradiction, take e1 ∈ ϕ−1 (b2 • ) such that b1 6∈ • e1 and m1 [e1 i; hence all its preconditions are marked. Since SC contains e1 , one of its preconditions belongs to SC as well as b1 , this is a contradiction because the sequential component has only one token. 2. By contradiction, take e1 ∈ ϕ−1 (• b2 ) such that m1 [e1 i; hence all its precon- ditions are marked. Since SC contains e1 , one of its preconditions belongs to SC as well as b1 , and this is a contradiction because the sequential com- ponent has only one token. t u Our morphisms can be seen like a special case of Winskel morphisms [13], as we shall prove in Section 5. Then, since Winskel morphisms preserve reachable markings, also α-morphisms do, as stated in the following. 150 PNSE’12 – Petri Nets and Software Engineering Proposition 1. Let  ϕ : N1 → N2 be an α-morphism.  Then if m1 ∈ m10 and m1 [ei m01 then ϕ(m1 ) ∈ m20 and – if ϕ(e) ∈ E2 then ϕ(m1 ) [ϕ(e)i ϕ(m01 ) else – (if ϕ(e) ∈ B2 then) ϕ(m1 ) = ϕ(m01 ). As for other morphisms in the literature, α-morphisms do not reflect reachable markings. This happens either when a condition is refined by a subnet leading to a block before reaching a marking enabling out-events, or whenever the re- finements of conditions “interfere” with each other so that, even if in each bubble a “final” local marking is reached, the global marking doesn’t enable any event. The second case is shown in Fig. 5: any event in each bubble can fire, but N1 has two deadlocks: {p3, p6} and {p4, p5}. The two above cases suggest to require Fig. 5: An α-morphism. both that any condition is refined by a subnet such that, when a final marking is reached, this one enables events which correspond to the post-events of the refined condition; and also that different refinements do not “interfere” with each other. The non interference is guaranteed when any event of N2 has at most a unique condition in its neighbourhood that is properly refined in N1 . In order to reflect the reachable markings we have to introduce local be- havioural constraints and this by considering the unfolding of subnets related to the bubbles. Then, we need to define the following auxiliary construction. Given an α-morphism ϕ : N1 → N2 , and a condition b2 ∈ B2 with its refine- ment N1 (ϕ−1 (b2 )), we define two new SMD-EN Systems. The first one, denoted S1 (b2 ), contains (a copy of) the subnet N1 (ϕ−1 (b2 )), its pre and post-events in E1 and two new conditions: bin 1 , which is pre of all the pre-events, and b1 , out which is post of all the post-events. The initial marking of S1 (b2 ) will be {b1 }. in The second system, denoted S2 (b2 ) contains b2 , its pre- and post-events and two new conditions: bin 2 , which is pre of all the pre-events, and b2 , which is post of out all the post-events. The initial marking of S2 (b2 ) will be {bin 2 }. L. Bernardinello et al.: Local state refinement 151 In Fig. 6 and 7 we show the two systems S1 (b2 ) and S2 (b2 ) for the nets showed in the initial example (Fig. 1 and 2), in Section 1, with b2 = formal_check. Fig. 6: S1 (formal_check) of Fig. 2. Fig. 7: S2 (formal_check) of Fig. 1. Definition 9. Let ϕ : N1 → N2 be an α-morphism and b2 ∈ B2 . Construct the SMD-EN Systems, S1 (b2 ) = (BS1 , ES1 , FS1 , mS1 0 ) and S2 (b2 ) = FS2 , mS2 (BS2 , ES2 , 0 ) in this way:  −1 (ϕ (b2 ) ∩ B1 ) ∪ {b1 } out if • b2 = ∅ BS1 = (ϕ−1 (b2 ) ∩ B1 ) ∪ {bin 1 } if b2 • = ∅   −1 (ϕ (b2 ) ∩ B1 ) ∪ {bin1 , b1 } otherwise out ES1 = (ϕ (b2 ) ∩ E1 ) ∪ ϕ ( b2 ) ∪ ϕ−1 (b2 • ); −1 −1 • FS1 = (F1 ∩ ((BS1 ∪ ES1 ) × (ES1 ∪ BS1 ))) ∪ FS1 in out ∪ FS1 , where FS1 = {(b1 , e) : e ∈ ϕ ( b2 )} and in in −1 • −1 FS1out =({(e, bout 1 ):e∈ϕ (b2 • )}; m10 ∩ ϕ−1 (b2 ) if • b2 = ∅ mS10 = {bin 1 } otherwise 152 PNSE’12 – Petri Nets and Software Engineering   {b2 , b2 } out if • b2 = ∅ BS2 = {b2 , bin 2 } if b2 • = ∅   {b2 , b2 , b2 } otherwise in out ES2 = • b2 • ; FS2 = (F2 ∩ ((BS2 ∪ ES2 ) × (ES2 ∪ BS2 ))) ∪ FS2 in ∪ FS2 out , where in FS2 = {(bin 2( , e) : e ∈ • b2 } and F out S2 = {(e, bout 2 ) : e ∈ b 2 • }; m 2 0 ∩ {b 2 } if • b2 = ∅ mS2 0 = {bin 2 } otherwise Define ϕS as a map from S1 (b2 ) to S2 (b2 ), which restricts ϕ to the elements of S1 (b2 ), and extends it with ϕS (bin1 ) = b2 and ϕ (b1 ) = b2 . in S out out Note that S1 (b2 ) and S2 (b2 ) are SMD-EN Systems and that ϕS is an α- morphism. Let ϕ : N1 → N2 be an α-morphism and ϕS : S1 (b2 ) → S2 (b2 ) as in Def. 9. By using ϕS , consider two labelling functions l1 and l2 such that the events in ES2 are all observable, i.e.: l2 is the identity function, and the invisible events of S1 (b2 ) are the ones mapped to conditions, i.e.: ( ϕS (e) if ϕS (e) ∈ ES2 ∀e ∈ ES1 : l1 (e) = τ otherwise Let Unf (S1 (b2 )) be the unfolding of S1 (b2 ) with u : Unf (S1 (b2 )) → S1 (b2 ) folding function. The following lemma shows that, if the map, ϕS ◦ u, obtained composing ϕS with u is an α-morphism, then S1 (b2 ) and S2 (b2 ) are bisimilar. Lemma 3. Let ϕ : N1 → N2 be an α-morphism, and ϕS as in Def. 9. Let Unf (S1 (b2 )) be the unfolding of S1 (b2 ) with u folding function. If ϕS ◦ u is  an α- morphism from Unf (S1 (b2 )) to S2 (b2 ), then r = {(m1 , ϕS (m1 )) : m1 ∈ mS1 0 } is a bisimulation, and (S1 (b2 ), l1 ) and (S1 (b2 ), l2 ) are bisimilar. In case the morphism corresponds to the refinement of a marked condition, we ask all the tokens of the corresponding bubble to be into in-conditions which are post-conditions of a pre-event, if it exists. System N1 is then called well marked with respect to ϕ. Definition 10. Let ϕ : N1 → N2 be an α-morphism. System N1 is well marked with respect to ϕ if for each b2 ∈ B2 one of the following conditions hold: – ϕ−1 (b2 ) ∩ m10 = ∅ or – if • b2 6= ∅ then there is e1 ∈ ϕ−1 (• b2 ) such that ϕ−1 (b2 ) ∩ m10 = e1 • or – if • b2 = ∅ then ϕ−1 (b2 ) ∩ m10 = ϕ−1 (b2 ) The following proposition states a set of conditions under which reachable mark- ings are reflected by α-morphisms. Proposition 2. Let ϕ : N1 → N2 be an α-morphism such that N1 is well marked w.r.t. ϕ and ϕS ◦ u be an α-morphism from Unf (S1 (b2 )) to S2 (b2 ) then, for all m2 ∈ m20 , there is m1 ∈ m10 such that ϕ(m1 ) = m2 . L. Bernardinello et al.: Local state refinement 153 Proof. We will actually show a slightly stronger property, namely that m1 can be chosen so that its intersection with the set of conditions in the bubble refining b2 only contains elements in (N1 (ϕ−1 (b2 ))) . The proof is by induction on the length of a firing sequence σ from m20 to m2 . Suppose |σ| = 0. Then m2 = m20 . By definition, ϕ(m10 ) = m20 . If b2 6∈ m20 , then m10 ∩ ϕ−1 (b2 ) = ∅. If b2 ∈ m20 , then we use Lemma 3 to reach in N1 a marking in the bubble of b2 that contains only out-conditions, and we are done. Suppose now |σ| = n+1. Then we can write σ = σ1 e2 , with m20 [σ1 im21 [e2 im2 . By the induction hypothesis, there is m11 ∈ [m10 i such that ϕ(m11 ) = m21 and m11 ∩ ϕ−1 (b2 ) ⊆ (N1 (ϕ−1 (b2 ))) . Since ϕ is surjective, there is at least one event in E1 that ϕ maps on e2 . If b2 6∈ • e2 , then there exists e1 ∈ ϕ−1 (e2 ) such that m11 [e1 i. If b2 ∈ • e2 , by Lemma 3 there exists e1 ∈ ϕ−1 (e2 ) such that m11 [e1 i. t u Let Ni = (Bi , Ei , Fi , mi0 ) be a SMD-EN System for i = 1, 2 and let ϕ : N1 → N2 be an α-morphism. By using ϕ, the labelling functions are defined such that E2 are all observable, i.e.: l2 is the identity function, and the invisible events of N1 are the ones mapped to conditions, i.e.: ( ϕ(e) if ϕ(e) ∈ E2 ∀e ∈ E1 : l1 (e) = τ otherwise From Prop. 1 and Prop. 2, it then follows that N1 and N2 are bisimilar. Proposition 3. Let ϕ : N1 → N2 be an α-morphism such that N1 is well marked and ϕS ◦ u is an α-morphism from Unf (S1 (b2 )) to S2 (b2 ) then, (N1 , l1 ) and (N2 , l2 ) are bisimilar (N1 , l1 ) ≈ (N2 , l2 ). Prop. 2 and Prop. 3 are stated in the case in which only one condition is refined, but they can be generalized to multiple refinements, provided that in the neighbourhood of each event of N2 there is, at most, one refined condition. The examples in Fig. 5 show why this constraint is required. 5 Relations with Winskel morphisms Let us now study the relation between ω-morphisms and Winskel morphisms, as defined in [13]. A Winskel morphism from N1 to N2 is a pair (η, β) with η : E1 →∗ E2 partial function and β : B1 → B2 finitary multirelation such that β(m10 ) = m20 and ∀e ∈ E : • (η(e)) = β(• e) and (η(e))• = β(e• ). Note that if η(e) is undefined, β(• e) and β(e• ) should be the empty set. Given an ω-morphism from N1 to N2 we associate to it a Winskel morphism. This is possible by adding or deleting conditions to N1 , if needed. These condi- tions are representations of the abstract conditions refined in N1 . The obtained net is canonical with respect to ϕ as in the following definition. 154 PNSE’12 – Petri Nets and Software Engineering Definition 11. Let ϕ : X1 → X2 be an ω-morphism from N1 to N2 . N1 is canonical with respect to ϕ if every bubble, ϕ−1 (b2 ) with b2 ∈ B2 , contains one condition, b1 ∈ ϕ−1 (b2 ) ∩ B1 , that satisfies the following constraints: – b1 ∈ m10 ⇔ b2 ∈ m20 ; – • b1 = ϕ−1 (• b2 ); – b1 • = ϕ−1 (b2 • ). We call that condition b1 representation of b2 , denoted rN1 (b2 ). If N1 is not canonical, it is always possible to construct its unique canonical version, N1C , by adding the missing representations, and marking them as their images, or by deleting the multiple ones. The corresponding morphism, ϕC , co- incides with ϕ, plus the mapping of the new conditions on the corresponding conditions of N2 . It is easy to verify that the canonical version of a system, with respect to an ω-morphism to another SMD-EN Systems, is unique up to isomorphisms. Proposition 4. ϕC is an ω-morphism from N1C to N2 . Take N1C , N2 and ϕC . Now, restrict ϕC to all the nodes of N1C that are not in a bubble ϕ−1 (b2 ), but for rN1 (b2 ), for some b2 ∈ B2 and call it (ϕC )rep . Proposition 5. ((ϕC )rep ↓ E1C , (ϕC )rep ↓ B1C ) is a Winskel morphism. Any α-morphism is an ω-morphism. Adding to N1 the representation of each condition does not modify the behaviour, because of the constraint on sequential components. Hence, the result stated here hold for α-morphisms. In this sense, we consider them as a special case of Winskel morphisms. 6 Conclusions We have presented a notion of morphism for a basic class of Petri nets with the aim of supporting refinement/abstraction of local states. The morphism, in fact, formalizes the relation between a refined net system and an abstract one, by replacing local states of the target net system with subnets. The main idea is that if one starts with an abstract model with some required behavioural prop- erties, then, by refining local states with subnets respecting some constraints, the refined net system will maintain the required behavioural properties. Indeed, the main results concern behavioural properties preserved and reflected by the morphisms. In particular, reachable markings are preserved, and we have charac- terized some conditions under which reachable markings are reflected, and under which the morphisms induce a bisimulation between net systems. Since bisimu- lation preserves deadlock freeness, this implies for example that, starting from a deadlock-free abstract system it is possible to refine it obtaining a system which is still deadlock-free. The constraints in order to preserve/reflect behavioural properties are structural and behavioural, where the behavioural ones are only local. On this morphism in [2], we have defined a notion of composition based on interface in the line of [4]. For what concerns future work, we plan to study the constraints under which this morphism can be defined for P/T nets and Coloured nets. L. Bernardinello et al.: Local state refinement 155 Acknowledgments Work partially supported by MIUR. References 1. Marek A. Bednarczyk and Andrzej M. Borzyszkowski. On concurrent realization of reactive systems and their morphisms. In Hartmut Ehrig, Gabriel Juhás, Julia Padberg, and Grzegorz Rozenberg, editors, Unifying Petri Nets, volume 2128 of Lecture Notes in Computer Science, pages 346–379. Springer, 2001. 2. Luca Bernardinello, Elisabetta Mangioni, and Lucia Pomello. Composition of ele- mentary net systems based on α-morphisms. In Proc. Workshop Componet 2012, Hamburg 2012. 3. Luca Bernardinello, Elisabetta Mangioni, and Lucia Pomello. Local state refine- ment on elementary net systems: an approach based on morphisms. Internal report (2012), available at http://www.mc3.disco.unimib.it/pub/bmp2012-def.pdf. 4. Luca Bernardinello, Elena Monticelli, and Lucia Pomello. On preserving struc- tural and behavioural properties by composing net systems on interfaces. Fundam. Inform., 80(1-3):31–47, 2007. 5. Wilfried Brauer, Robert Gold, and Walter Vogler. A survey of behaviour and equivalence preserving refinements of Petri nets. Advances in Petri Nets 1990, pages 1–46, 1991. 6. Jörg Desel and Agathe Merceron. Vicinity respecting homomorphisms for ab- stracting system requirements. Transactions on Petri Nets and Other Models of Concurrency, 4:1–20, 2010. 7. Robin Milner. Communication and concurrency. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1989. 8. Mogens Nielsen, Grzegorz Rozenberg, and P. S. Thiagarajan. Elementary transi- tion systems and refinement. Acta Inf., 29(6/7):555–578, 1992. 9. Julia Padberg and Milan Urbásek. Rule-based refinement of Petri nets: A survey. In Hartmut Ehrig, Wolfgang Reisig, Grzegorz Rozenberg, and Herbert Weber, editors, Petri Net Technology for Communication-Based Systems, volume 2472 of Lecture Notes in Computer Science, pages 161–196. Springer, 2003. 10. Lucia Pomello, Grzegorz Rozenberg, and Carla Simone. A survey of equivalence notions for net based systems. In Grzegorz Rozenberg, editor, Advances in Petri Nets: The DEMON Project, volume 609 of Lecture Notes in Computer Science, pages 410–472. Springer, 1992. 11. Grzegorz Rozenberg and Joost Engelfriet. Elementary net systems. In Wolfgang Reisig and Grzegorz Rozenberg, editors, Petri Nets, volume 1491 of Lecture Notes in Computer Science, pages 12–121. Springer, 1996. 12. Walter Vogler. Executions: A new partial-order semantics of Petri nets. Theor. Comput. Sci., 91(2):205–238, 1991. 13. Glynn Winskel. Petri nets, algebras, morphisms, and compositionality. Inf. Com- put., 72(3):197–238, 1987.