In the design of concurrent and distributed systems, modularity 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 refined 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 conditions under which reachable markings are preserved or reflected, and the conditions under which a morphism induces a bisimulation between net systems.
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 properties 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
[
A very general class of morphisms, interpreted as abstraction of system
requirements, with less focus on strict preservation of behavioural properties, is
defined in [
The approach we present in this paper is similar in spirit to the refinement
operation proposed in [
α-morphisms can be seen as a special case of the morphisms introduced by
Winskel in [
Our approach is motivated by the attempt to define a refinement operation preserving behavioural properties on the basis of structural and only local behavioural constraints. The additional restrictions, with respect to general morphisms, 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 [
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 [
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.
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, 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
In this section, we recall the basic definitions of net theory, in particular
Elementary Net Systems [
We will use the symbol ↓ to denote the restriction of a function on a subset of its domain. 2.1
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 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 = (B0, E0, F 0) is a subnet of N = (B, E, F ) if B0 ⊆ B, E0 ⊆ E, and F 0 = F ∩ ((B0 × E0) ∪ (E0 × B0)). Given a subset of elements A ⊆ X, we say that 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 specifies 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 [m0i.
An EN System is contact-free if ∀e ∈ E, ∀m ∈ [m0i: •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.
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 exF ∗x, eyF ∗y, and •ex ∩ •ey 6= ∅.
An occurrence net is a net N = (B, E, F ) satisfying: 1. if e1, e2 ∈ E, e1• ∩ e2• 6= ∅ then e1 = e2;
3. for any x ∈ X, {y : yF ∗x} is finite; 4. #N is irreflexive,
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.
– π(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
Bisimulation relations have been introduced as equivalence notions with respect
to event observation [
Let m, m0 ∈ [m0i 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 [
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 and (vice versa) ∀m01 : m1 (ai m01 ⇒ ∃m02 : m2 (ai m02 ∧ (m01, m02) ∈ r ∀m02 : m2 (ai m02 ⇒ ∃m01 : m1 (ai m01 ∧ (m01, m02) ∈ r
For short in the rest of the paper we will use the term bisimulation instead of weak bisimulation. 3
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)}; 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
As we can see in Fig. 3a and 3b, in-conditions and out-conditions have different 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 particular 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.
By requirement 5e, events in the neighbourhood of a bubble are not concurrent, 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 [
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 neighbourhood of each condition of NSC2.
Sequential components are not preserved, as we can see in Fig. 4. The sequential 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 SMDEN System, each condition at any time can be true or false. It is not possible that 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 ∈
m01 ∩ ϕ−1(b2) = ∅. 2. Let e1 ∈ E1, b2 ∈ B2: e1 ∈ ϕ−1(•b2); m1, m01 ∈ m1 ∩ ϕ−1(b2) = ∅. m10 : m1 [e1i m01, then m10 : m1 [e1i m01 then 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 [e1i; 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 [e1i; hence all its preconditions 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 component has only one token.
Our morphisms can be seen like a special case of Winskel morphisms [
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 refinements 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 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 behavioural 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 refinement 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: bi1n, which is pre of all the pre-events, and bo1ut, which is post of all the post-events. The initial marking of S1(b2) will be {bi1n}. The second system, denoted S2(b2) contains b2, its pre- and post-events and two new conditions: bi2n, which is pre of all the pre-events, and bo2ut, which is post of all the post-events. The initial marking of S2(b2) will be {bi2n}.
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. (m10 ∩ ϕ−1(b2) if •b2 = ∅ Definition 9. Let ϕ : N1 → N2 be an α-morphism and b2 ∈ B2.
Construct the SMD-EN Systems, S1(b2) = (BS1, ES1, FS1, m0S1) and S2(b2) = (BS2, ES2, FS2, m0S2) in this way:
(ϕ−1(b2) ∩ B1) ∪ {bo1ut} if •b2 = ∅ BS1 = (ϕ−1(b2) ∩ B1) ∪ {bi1n} if b2• = ∅
(ϕ−1(b2) ∩ B1) ∪ {bi1n, bo1ut} otherwise ES1 = (ϕ−1(b2) ∩ E1) ∪ ϕ−1(•b2) ∪ ϕ−1(b2•); FS1 = (F1 ∩ ((BS1 ∪ ES1) × (ES1 ∪ BS1))) ∪ FSin1 ∪ FSo1ut, where FSin1 = {(bi1n, e) : e ∈ ϕ−1(•b2)} and
FSo1ut = {(e, bo1ut) : e ∈ ϕ−1(b2•)};
if b2• = ∅ {b2, bi2n, bo2ut} otherwise ES2 = •b2•;
if •b2 = ∅ {bi2n} m0S2 = (m20 ∩ {b2} if •b2 = ∅
otherwise FSin2F=S2{=(bi2(nF, 2e)∩:(e(B∈S•2b∪2}EaSn2d) ×FSo(2uEt S=2 ∪{(Be,Sb2o2)u)t)) ∪:eF∈Sin2b∪2•F};So2ut, where
Define ϕS as a map from S1(b2) to S2(b2), which restricts ϕ to the elements of S1(b2), and extends it with ϕS(bi1n) = bin and ϕS(bo1ut) = bout. 2 2
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.: ∀e ∈ ES1 : l1(e) = (ϕS(e) if ϕS(e) ∈ ES2 τ 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 ∈ m0S1 } 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) ∩ m01 = e1• or – if •b2 = ∅ then ϕ−1(b2) ∩ m10 = ϕ−1(b2) The following proposition states a set of conditions under which reachable markings 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. 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 σ = σ1e2, with m20[σ1im21[e2im2. By the induction hypothesis, there is m11 ∈ [m10i 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 [e1i. If b2 ∈ •e2, by Lemma 3 there exists e1 ∈ ϕ−1(e2) such that m11 [e1i. tu
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 ∈ E1 : l1(e) = (ϕ(e) if ϕ(e) ∈ E2
τ 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
Let us now study the relation between ω-morphisms and Winskel morphisms, as
defined in [
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 conditions are representations of the abstract conditions refined in N1. The obtained net is canonical with respect to ϕ as in the following definition. 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: –– •b1b1∈=mϕ10−⇔1(•bb22)∈; m20; – 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, coincides 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
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
properties, 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
characterized some conditions under which reachable markings are reflected, and under
which the morphisms induce a bisimulation between net systems. Since
bisimulation 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 [