Property-Preserving Transformations of Elementary Net Systems Based on Morphisms? Luca Bernardinello2 , Irina Lomazova1 , Roman Nesterov1,2 , Lucia Pomello2 1 National Research University Higher School of Economics, 20 Myasnitskaya Ulitsa, 101000 Moscow, Russia 2 Dipartimento di Informatica, Sistemistica e Comunicazione, Università degli Studi di Milano-Bicocca, Viale Sarca 336 - Edificio U14, I-20126 Milano, Italia Abstract. Structural transformations that preserve properties of formal models of concurrent systems make their verification easier. We define structural transformations that allow to abstract and refine elementary net systems. Relations between abstract models and their refinements are formalized using morphisms. Transformations proposed in this paper induce morphisms between elementary net systems as well as preserve their behavioral properties. We also show application of the proposed transformations to the construction of a correct composition of interact- ing workflow net components. Keywords: Petri nets, transformations, abstraction, refinement, mor- phisms 1 Introduction Petri nets is a convenient formalism for modeling concurrent systems as well as for proving their important behavioral properties1 . Due to the well-known state explosion problem, there are various structural techniques developed in Petri net theory. The main advantage of structural techniques is the possibility to verify behavioral properties of Petri nets without computing their reachable markings. Structural Petri net transformations that preserve classical properties like boundedness, liveness, covering by place invariants make verification of parallel systems easier. On the one hand, starting from a sophisticated model, it is possi- ble to apply reduction transformations preserving properties of the initial model and then verify properties using a simplified model. On the other hand, having a simple abstract model, it is possible to apply refinement transformations that yield a more detailed model reflecting properties of an initial abstraction. Petri net transformations have been first described in several works (see, for example, [5,6,14,15,21]), where the authors have defined simple yet powerful ? Copyright c 2020 for this paper by its authors. Use permitted under Creative Com- mons License Attribution 4.0 International (CC BY 4.0). 1 This work is supported by MIUR and the Basic Research Program at the National Research University Higher School of Economics. 50 Luca Bernardinello, Irina Lomazova, Roman Nesterov, Lucia Pomello local structural reductions and extensions, s.t. liveness, boundedness (safeness), covering by place invariants, home state and proper termination can be preserved by corresponding transformations. A class of free choice Petri nets [11] is also widely adopted to model parallel systems for their structural constraints on conflicts. The work [9] gives a com- plete set of reduction/synthesis transformations that allows to obtain every live and bounded free choice net. Within the framework of bipolar synchronization schemes [10] strictly related to free choice Petri nets, the authors have also de- fined a set of local reduction and synthesis rules that yield only well behaved synchronization schemes. Another series of works [8,18] is devoted to the use of graph transformations in a categorical setting (the double-pushout approach). These transformations are applied to model and analyze behavior of re-configurable systems. Place [20] and, more generally, resource (sub-marking) [12] bisimulation are also powerful tools to reduce graphs of Petri net graphs preserving their observ- able behavior. These techniques are based on reducing places and resources in Petri nets if they produce bisimilar behavior. Petri net morphisms give a natural yet rigid framework to formalize struc- tural property-preserving relations [7,13,22]). In particular, in [17], morphisms inducing bisimulations have been discussed. For elementary net systems (EN systems) [3,19] – a basic class of models in net theory – α-morphisms have been introduced in [2]. They help to formalize relations between abstract models and their refinements. Moreover, α-morphisms preserve behavioral properties (reachable markings) as well as reflect them under specific local requirements. However, direct application of the definition of α- morphisms is rather difficult. Thus the main purpose of this paper is to define a set of local abstrac- tion/refinement transformations for EN systems. A local transformation acts only on a specific subnet, while the rest of the EN system remains unchanged. We consider EN systems with labeled transitions, where labels specify interac- tions with the environment. We present transformation rules preserving labeled transitions and minimizing unlabeled ones. These transformations are such that an initial net and a transformed net are related by an α-morphism, and their be- havioral properties including reachable markings and, especially, deadlocks are preserved. Interestingly enough, it is also shown that simple Petri net transfor- mations described earlier also yield corresponding α-morphisms. In addition, we demonstrate two cases of applying transformations defined in our study. Abstraction transformations are used in the context of building a correct composition of interacting workflow nets according to an approach de- scribed in [4]. Its correctness is based on abstracting component models with the help of α-morphisms. Refinement transformations are exploited to refine formal models of abstract interaction patterns [16] that give ready-to-use solutions to organize correct interactions of components in complex parallel systems. This paper is organized as follows. The next section gives the basic definitions. In Section 3, we define local abstraction and refinement transformations for EN Property-Preserving Transformations 51 systems, s.t. they induce α-morphisms. Section 4 discusses application of defined transformations to the problem of constructing correct systems with interacting workflow net components, whereas Section 5 concludes the paper. 2 Preliminaries Here we provide the basic definitions used in the paper. Let A, B be two sets. A function f from A to B is denoted by f : A → B. The set of all finite non-empty sequences over A is denoted by A+ . The set A∗ = A+ ∪ {} is the set of all finite sequences over A, where  is the empty sequence. A net is a triple N = (P, T, F ), where P and T are disjoint sets of places and transitions respectively, and F ⊆ (P × T ) ∪ (T × P ) is the flow relation. Places are depicted by circles, transitions are depicted by boxes, and a flow relation is shown by arcs. Let N = (P, T, F ) be a net. The preset of x ∈ P ∪ T is the set • x = {y ∈ P ∪ T | (y, x) ∈ F }. The postset of x ∈ P ∪ T is the set x• = {y ∈ P ∪ T | (x, y) ∈ F }. The neighborhood of x ∈ P ∪ T is the set • x• = • x ∪ x• . N is P-simple iff ∀p1 , p2 ∈ P : • p1 = • p2 and p1 • = p2 • implies that p1 = p2 . We consider nets without self-loops, s.t. ∀t ∈ T : |• t| ≥ 1 and |t• | ≥ 1. T, F ) be a net, and Y ⊆ P ∪ T . Then • Y = y∈Y • y, Y • = S S Let •N = (P, • • • • y∈Y y , and Y = Y ∪ Y . N (Y ) denotes the subnet of N generated by Y , i.e., N (Y ) = (P ∩ Y, T ∩ Y, F ∩ (Y × Y )). The set N (Y ) = {y ∈ Y | • y = ∅} is the input border, and the set N (Y ) = {y ∈ Y | y • = ∅} is the output border of a subnet N (Y ). A marking in a net N = (P, T, F ) is a subset of its places m ⊆ P . A marking m has a contact if ∃t ∈ T : • t ⊆ m and t• ∩ m 6= ∅. An elementary net system (EN system) is a tuple N = (P, T, F, m0 ), where m0 ⊆ P is the initial marking. A marking m is shown by putting black dots inside places belonging to m. A state machine is a connected net N = (P, T, F ), s.t. ∀t ∈ T : |• t| = |t• | = 1. The subnet of an EN system N = (P, T, F, m0 ) generated by C ⊆ P and • C • , i.e., N (C ∪ • C • ), is a sequential component of N iff it is a state machine and it has a single token in its initial marking. An EN system N = (P, T, F, m0 ) is covered by sequential components if every place in N belongs to at least one sequential component. Then N is called state machine decomposable (SMD). The firing rule defines the behavior of a net system. A marking m in an EN system N = (P, T, F, m0 ) enables a transition t ∈ T , denoted m[ti, iff • t ⊆ m and t• ∩ m = ∅. When an enabled transition t fires, N evolves to a new marking m0 = m \ • t ∪ t• , denoted m[tim0 . A sequence w ∈ T ∗ is a firing sequence of N iff m0 [t1 im1 [t2 i . . . mn−1 [tn imn and w = t1 . . . tn . Then we write m0 [wimn . The set of all firing sequences of N is denoted by FS(N ). A marking m in an EN system N = (P, T, F, m0 ) is reachable iff ∃w ∈ FS(N ) : m0 [wim. The set of all markings reachable from a marking m is denoted by [mi. It can be easily checked that reachable markings in an SMD-EN system 52 Luca Bernardinello, Irina Lomazova, Roman Nesterov, Lucia Pomello are free from contacts. A reachable marking m is a deadlock if it does not enable any transition. A deadlock m in an SMD-EN system N = (P, T, F, m0 ) can be characterized from a structural point of view. Let t ∈ T , s.t. • t ∩ m 6= ∅, and p ∈ P , s.t. p ∈ • t and p ∈ / m. There is a sequential component N (C ∪ • C • ) of N containing p, i.e., • p ∈ C. Let p0 = m ∩ C. Then either (p0 ) = ∅ and we are done, or we take a 0 0 • transition t ∈ (p ) and repeat the same step we have done for t. This procedure will finish either in a place with an empty postset or in a transition it started with. Intuitively, a deadlock is a poor synchronization of sequential components in N , where they are “waiting” for each other. For instance, the EN system shown in Fig. 1 has two deadlocks {p1 , p4 } and {p2 , p3 }, where the left and the right sequential components are waiting for each other since conflicts have been resolved independently. Fig. 1. Deadlock as poorly synchronized sequential components Abstraction/refinement relations between SMD-EN systems are formalized using α-morphisms introduced in [2]. Below we give the formal definition and briefly discuss the main intuition behind α-morphisms. Definition 1. Let Ni = (Pi , Ti , Fi , mi0 ) be an SMD-EN system, Xi = Pi ∪ Ti with i = 1, 2, where X1 ∩ X2 = ∅. An α-morphism from N1 to N2 is a total surjective map ϕ : X1 → X2 , also denoted ϕ : N1 → N2 , s.t.: 1. ϕ(P1 ) = P2 . 2. ϕ(m10 ) = m20 . • 3. ∀t1 ∈ T1 : if ϕ(t1 ) ∈ T2 , then ϕ(• t1 ) = • ϕ(t1 ) and ϕ(t1 • ) = ϕ(t1 ) . • • 4. ∀t1 ∈ T1 : if ϕ(t1 ) ∈ P2 , then ϕ( t1 ) = {ϕ(t1 )}. 5. ∀p2 ∈ P2 : (a) N1 (ϕ−1 (p2 )) is an acyclic net. (b) ∀p1 ∈ N1 (ϕ−1 (p2 )) : ϕ(• p1 ) ⊆ • p2 and if • p2 6= ∅, then • p1 6= ∅. (c) ∀p1 ∈ N1 (ϕ−1 (p2 )) : ϕ(p1 • ) = p2 • . (d) ∀p1 ∈ P1 ∩ ϕ−1 (p2 ) : p1 ∈/ N1 (ϕ−1 (p2 )) ⇒ ϕ(• p1 ) = p2 and p1 ∈ −1 / N1 (ϕ (p2 )) ⇒ ϕ(p1 • ) = p2 . (e) ∀p1 ∈ P1 ∩ ϕ−1 (p2 ) : there is a sequential component N 0 = (P 0 , T 0 , F 0 ) in N1 , s.t. p1 ∈ P 0 , ϕ−1 (• p2 • ) ⊆ T 0 . Property-Preserving Transformations 53 By definition, an α-morphism allows one to substitute a place in an abstract net system N2 with an acyclic subnet in N1 . The main motivation behind the use of α-morphisms is the ability to ensure that behavioral properties of an abstract model hold in its refinement. Requirements imposed by Definition 1 lead to the following observation. If a subnet in N1 refines a place in N2 , then this subnet should behave exactly as an abstract place does. More precisely, (a) no tokens are left in a subnet refining a place after firing a transition in a postset of an output border; (b) no transitions are enabled in the preset of an input border of a subnet refining a place whenever a token is inside a subnet. Main properties preserved and reflected by α-morphisms have been studied in [2]. We will mention them further in the paper where necessary. Figure 2, borrowed from [4], shows an example of α-morphism, where N1 is a refinement of an abstract net system N2 . The subnet N1 (ϕ−1 (p2 )) in N1 refines the place p2 in N2 , and transitions g and h are split in N1 . Fig. 2. An α-morphism ϕ : N1 → N2 3 Structural Transformations of SMD-EN Systems Direct application of Definition 1 to abstract and refine EN systems may be difficult. In this paper, we consider the use of structural transformations of EN systems that induce corresponding α-morphisms. The main purpose of our study is to develop a system of local abstraction/refinement transformations of EN systems and to study properties of these transformations. It is easy to see that an EN system can have several possible abstractions depending on the detail level. To reduce this ambiguity, we add labels to some transitions in EN-systems. Labeled transitions model actions through which an EN system communicates with its environment. Transformations preserve la- beled transitions and minimize the number of local transitions corresponding to the internal behavior of an EN system. Specifically, we plan to apply local transformations to construct a correct composition of synchronously and asyn- 54 Luca Bernardinello, Irina Lomazova, Roman Nesterov, Lucia Pomello chronously interacting workflow nets as described in [4], where labeled transitions in workflow nets model component synchronizations and message exchange. Let N = (P, T, F, m0 ) be an SMD-EN system, and Λ be an alphabet of com- munication action names. A transition labeling function is a surjective function h : T → Λ ∪ {τ }, where τ is the special label of a local action. We define structural transformation rules inducing α-morphisms between initial and transformed EN systems. A transformation rule is a structure ρ = (L, cL , R, cR ), where: 1. L is the left part of a rule that is a subnet in an EN system to be transformed. 2. cL – flow relation and transition labeling constraints imposed on L that define applicability of a rule to an EN system. 3. R is the right part of a rule that is a subnet replacing L in a net system. 4. cR – flow relation, marking, transition labeling constraints imposed on R. Constraints cL and cR are necessary to construct an α-morphism between the initial and the transformed EN system. Thus, a transformation rule ρ = (L, cL , R, cR ) is applicable to an SMD-EN system N = (P, T, F, m0 ) if there exists a subnet in N isomorphic to L satisfying structural and labeling constraints cL . Let N = (P, T, F, m0 ) be an SMD-EN net system, and ρ = (L, cL , R, cR ) be a transformation rule applicable to N . Let N (XL ) be the subnet of N , generated by XL ⊆ P ∪ T , such that it is isomorphic to L. Then we say that ρ is applicable to the subnet N (XL ) in N . Application of ρ to N includes the following steps: 1. Remove the subnet N (XL ) from N . 2. Add the subnet corresponding to the right part R of ρ to N connecting it with the neighborhood •XL• . 3. Make necessary changes, i.e., relabel transitions and add tokens to places, in an inserted subnet according to cR . Correspondingly, the effect of applying ρ to a subnet N (XL ) in N isomorphic to the left part of ρ is denoted by ρ(N, XL ) = (P 0 , T 0 , F 0 , m00 ) with a new transition labeling function h0 : T 0 → Λ. 3.1 Abstraction Rules In this section, we define five simple abstraction rules. They help to abstract SMD-ED systems with labeled transitions. Abstraction rules induce α-morphisms and, correspondingly, preserve reachable markings and deadlocks of models. For what follows, let N = (P, T, F, m0 ) be an SMD-EN system with a tran- sition labeling function h : T → Λ ∪ {τ }. A1: Place simplification – applicability constraints: two places p1 , p2 ∈ P in N with the same neighbor- hood (• p1 = • p2 and p1 • = p2 • ) as shown in Fig. 3(a). Property-Preserving Transformations 55 – transformation: fusion of p1 and p2 into a single place p12 , s.t. • p12 = • p1 = • p2 , p12 • = p1 • = p2 • and p12 ∈ m00 ⇔ (p1 ∈ m0 and p2 ∈ m0 ). – α-morphism ϕA1 : N → N 0 , where N 0 = ρA1 (N, {p1 , p2 }), maps places p1 and p2 in N to a place p12 in N 0 . For other nodes in N , ϕA1 is the identity mapping between N and N 0 . Place simplification is one of the most basic Petri net transformations. It has been discussed earlier in [14] (cf. “fusion of parallel places”) and in [5] (cf. “sim- plification of redundant places”). A2: Transition simplification – applicability constraints: two transitions t1 , t2 ∈ T in N with the same neigh- borhood and label (• t1 = • t2 , t1 • = t2 • and h(t1 ) = h(t2 )) as demonstrated in Fig. 3(b)). – transformation: fusion of t1 and t2 into a single transitions t12 , s.t. • t12 = • t1 = • t2 , t12 • = t1 • = t2 • and h0 (t12 ) = h(t1 ) = h(t2 ). – α-morphism ϕA2 : N → N 0 , where N 0 = ρA2 (N, {t1 , t2 }), maps transitions t1 and t2 in N to a transition t12 in N 0 . For other nodes in N , ϕA2 is the identity mapping between N and N 0 . Transition simplification (without labeling constraints) has also been mentioned in [14] (cf. “fusion of parallel transitions”). (a) abstraction rule A1 (b) abstraction rule A2 Fig. 3. Place and transition simplification A3: Local transition elimination – applicability constraints: a transition t ∈ T in N , s.t. h(t) = τ and: 1. • t = {p1 } and t• = {p2 }; 2. p1 • = • p2 = {t}; 3. • p1 6= ∅ or p2 • 6= ∅. 4. • p1 ∩ p2 • = ∅. – transformation: fusion of t, p1 and p2 into a single place p12 , s.t. • p12 = • p1 , p12 • = p2 • and p12 ∈ m00 ⇔ (p1 ∈ m0 or p2 ∈ m0 ). – α-morphism ϕA3 : N → N 0 , where N 0 = ρA3 (N, {p1 , t, p2 }), maps t, p1 and p2 in N to a single place p12 in N 0 . For other nodes in N , ϕA3 is the identity mapping between N and N 0 . 56 Luca Bernardinello, Irina Lomazova, Roman Nesterov, Lucia Pomello Figure 4 shows left and right parts of this rule as well as construction of the α-morphism ϕA3 . Applicability constraints of ρA3 are aimed to avoid generating isolated places and self-loops in ρA3 (N, {p1 , t, p2 }). A similar transition transfor- mation called “pre-fusion” has been discussed in [5], where it has been expressed as fusion of two transitions connected by a place. Fig. 4. Abstraction rule A3: local transition elimination The abstraction rules defined above can be easily generalized: to sets of places and transitions (for ρA1 and ρA2 respectively) or to a ”chain” of local transitions (for ρA3 ). We propose to apply a simple abstraction rule several times rather than to complicate left parts of rules together with their applicability constraints. A4: Postset-empty place simplification – applicability constraints: two places p1 and p2 in N , s.t. p1 • = p2 • = ∅ and: 1. • p1 ∩ • p2 = ∅; 2. ∀C ⊆ P : if N (C∪• C • ) is a sequential component, then p1 ∈ C ⇔ p2 ∈ C. – transformation: fusion of p1 and p2 into a single place p12 , s.t. • p12 = • p1 ∪ • p2 , p12 • = p1 • = p2 • and p12 ∈ m00 ⇔ (p1 ∈ m0 or p2 ∈ m0 ) as illustrated in Fig. 5. – α-morphism ϕA4 : N → N 0 , where N 0 = ρA4 (N, {p1 , p2 }), maps p1 and p2 in N to a single place p12 in N 0 . For other nodes in N , ϕA4 is the identity mapping between N and N 0 . It is necessary to check that there are no sequential components distinguishing p1 and p2 in order to preserve state machine decomposability after transformation. Therefore we also satisfy the requirement 5e of Definition 1. Fig. 5. Abstraction rule A4: Postset-empty place simplification In the following rule ρA5 , we fuse two transitions that have the same postset and disjoint presets as opposed to the abstraction rule ρA2 . Applicability con- straints of this rule do not allow us to lose deadlocks present in an initial EN Property-Preserving Transformations 57 system by abstracting it. The problem of losing deadlocks is the consequence of the fact that α-morphisms do not reflect reachable markings without additional restrictions as described in [2]. In the setting of our study, this means that an in- verse image of a reachable marking that enables transitions in an abstract model may be a deadlock in an initial EN system. Let us illustrate the problem of losing deadlocks by the following example. The net system shown in Fig. 1 has two deadlocks {p1 , p4 } and {p2 , p3 }. These deadlocks are caused by the fact that conflicts are resolved independently by two sequential components. Suppose that the two transitions t1 and t2 in the postsets of p1 , . . . , p4 have the same label. Then, according to the definition of α-morphisms, it is possible to fuse p1 with p2 , p3 with p4 and t1 with t2 correspondingly. The image t0 of t1 and t2 will have two places in its preset, and there will be the reachable marking {p12 , p34 } in a transformed net system enabling t0 . However, there is an inverse image of the marking {p12 , p34 }, e.g., the deadlock {p1 , p4 } that does not enable an inverse image of t0 . Correspondingly, we impose constraints on places in the presets of two tran- sitions to be fused, s.t. if there is a deadlock containing places in the presets of both transitions, then it should not be possible to fuse these transitions. A5: Preset-disjoint transition simplification – applicability constraints: two transitions t1 and t2 , s.t. h(t1 ) = h(t2 ) and: 1. • t1 ∩ • t2 = ∅ and |• t1 | = |• t2 |; 2. t1 • = t2 • ; 3. ∀a ∈ • t1 ∀b ∈ • t2 ∃C ⊆ P : a, b ∈ C, N (C ∪ • C • ) is a sequential compo- nent. – transformation: fusion of t1 and t2 into a single transition t12 with h0 (t12 ) = h(t1 ) = h(t2 ), t12 • = t1 • = t2 • and • t12 = {(a, b) | a ∈ • t1 , b ∈ • t2 , g(a) = b}, where g : • t1 → • t2 is a bijection. As for the initial marking m00 in ρA5 (N, {t1 , t2 }), we have ∀(a, b) ∈ • t12 : (a, b) ∈ m00 ⇔ ((a ∈ m0 and b ∈ / m0 ) or (a ∈ / m0 and b ∈ m0 )). – α-morphism ϕA5 : N → N 0 , where N 0 = ρA5 (N, {t1 , t2 }), maps t1 and t2 to t12 in N 0 as well as pairs of places in • t1 and • t2 corresponding to each other by g, and for other nodes in N , ϕA5 is the identity mapping. In Fig. 6, we provide left and right parts of the abstraction rule ρA5 . Fig. 6. Abstraction rule A5: Preset-disjoint transition simplification 58 Luca Bernardinello, Irina Lomazova, Roman Nesterov, Lucia Pomello The third requirement of ρA5 makes sure that any place in • t1 is in conflict with any place in • t2 . Then it is easy to check that if there is a reachable marking in N with a token in • t1 , then there cannot be a token in • t2 at the same time. Application of this abstraction rule involves pairwise place fusion in • t1 and • t2 . According to the third requirement on sequential components, we define a bijection g : • t1 → • t2 and fuse places in • t1 and • t2 corresponding by g. Let us consider a more detailed example of applying the abstraction rule ρA5 . Two transitions t1 and t2 in a net system N1 shown in Fig. 7 are candidates to be fused, since they have the same label λ and share the same postset. We need to check whether places in • t1 and • t2 are connected by sequential components (for short, SC): 1. p1 and p3 are in the SC generated by C = {s4 , s1 , p1 , p3 , p5 } and • C • . 2. p2 and p3 are in the SC generated by C = {s4 , s2 , p2 , p3 , p5 } and • C • . 3. p2 and p4 are in the SC generated by C = {s5 , s3 , p2 , p4 , p5 } and • C • . 4. p1 and p4 together do not belong to any SC. Indeed, there is a deadlock {p1 , s2 , p4 }, s.t. it contains places both from • t1 and from • t2 . Thus, t1 and t2 cannot be fused without losing the deadlock. Fig. 7. A net system to check applicability constraints of ρA5 It is worth mentioning that application of the rule ρA5 can also be straight- forwardly extended to the case when transitions t1 and t2 have shared places in their presets. Now we discuss the main properties of the simple abstraction rules. We denote the set of abstraction rules by AR = {ρA1 , ..., ρA5 }. By construction, application of an abstraction rule induce an α-morphism from an initial SMD-EN system towards a transformed one. Proposition 1. Let ρ ∈ AR, s.t. ρ is applicable to a subnet N (XL ) in N . Then there is an α-morphism ϕρ : N → ρ(N, XL ). Corollary 1. Let ρ1 , ρ2 ∈ AR, s.t. ρ2 is applicable to a subnet in ρ1 (N, XL ) gen- erated by XL0 . Then there is an α-morphism ϕρ2 ◦ ϕρ1 : N → ρ2 (ρ1 (N, XL ), XL0 ). Property-Preserving Transformations 59 The important property is whether the order of applying abstraction rules matter when at least two abstraction rules are applicable to the same net system. In this case, we distinguish when two abstraction rules (applicable to the same net system) coincide or differ. Proposition 2. Let ρ1 , ρ2 ∈ AR, s.t. ρ1 is applicable to a subnet N (XL1 ) in N , ρ2 is applicable to a subnet N (XL2 ) in N and XL1 6= XL2 . Then 1. If ρ1 = ρ2 , then the effect of applying ρ2 to ρ1 (N, XL1 ) is isomorphic to the effect of applying ρ1 to ρ2 (N, XL2 ). 2. If ρ1 6= ρ2 and XL1 ∩ XL2 = ∅, then ρ2 (ρ1 (N, XL1 ), XL2 ) = ρ1 (ρ2 (N, XL2 ), XL1 ). According to the structural characterization of a deadlock in an SMD net system and to the structural requirements of abstraction rules, we conclude that if there is a deadlock in an initial net system, then the image of this deadlock is also a deadlock in a transformed net system. In proving this statement, we also rely on the fact that α-morphisms preserve reachable markings and transition firings [2], i.e. an image of a reachable marking in a refined EN system is also a reachable marking which, moreover, enables any image of enabled transitions in a refined model. Proposition 3. Let ρ ∈ AR, s.t. ρ is applicable to a subnet N (XL ) in N . Let m ∈ [m0 i be a deadlock in N . Then ϕρ (m) is a deadlock in ρ(N, XL ). • Proof. Let N 0 = ρ(N, XL ). If m• = ∅, then, by Definition 1, ϕρ (m) = ∅. Thus, ϕρ (m) is a deadlock in N 0 . If ∃t ∈ T : • t ∩ m 6= ∅, then the proof is done by contradiction. Suppose that ϕρ (m) is not a deadlock. Then either ϕρ (t) = ϕρ (m), i.e., a transition t and • t• is mapped to a single place, or • ϕρ (t) ⊆ ϕρ (m), i.e. a marking ϕρ (m) enables ϕρ (t) in N 0 . A transition t cannot be mapped to a place by ϕρ since |• t| > 1, because there are places in • t, s.t. • t ∩ m 6= ∅ and there is at least one place p ∈ • t, s.t. p ∈/ m. If a marking ϕρ (m) enables ϕρ (t) in N 0 , then t is fused with another transition t0 by ρ, s.t. • t0 ∩ m 6= ∅. This fusion is not allowed by the abstraction rule ρA5 , then it is a contradiction. 3.2 Refinement Rules In this section, we define four simple refinement rules. They allow one to refine a given SMD-EN system. Three out of four proposed refinement rules are the inverse of abstraction rules discussed in the previous section. Refinement rules also induce α-morphisms. The main difference here is that the direction of α- morphisms is the opposite to the direction of a transformation. For what follows, let N = (P, T, F, m0 ) be an SMD-EN system with a tran- sition labeling function h : T → Λ ∪ {τ }. Recall also that the effect of applying a transformation rule ρ to N is denoted by ρ(N, XL ) = (P 0 , T 0 , F 0 , m00 ) with a new transition labeling function h0 : T 0 → Λ ∪ {τ }, where XL ⊆ P ∪ T and N (XL ) is a corresponding subnet in N transformed by ρ. 60 Luca Bernardinello, Irina Lomazova, Roman Nesterov, Lucia Pomello R1: Place duplication – applicability constraints: a place p in N . – transformation: split p into two places p1 and p2 , s.t. • p1 = • p2 = • p, p1 • = p2 • = p• and (p1 ∈ m00 and p2 ∈ m00 ) ⇔ p ∈ m0 (see Fig. 8(a)). – α-morphism ϕR1 : N 0 → N , where N 0 = ρR1 (N, {p}), maps places p1 and p2 in N 0 to a single place p in N . For other nodes in N 0 , ϕR1 is the identity mapping between N 0 and N . R2: Transition duplication – applicability constraints: a transition t in N . – transformation: split t into two transitions t1 and t2 , s.t. • t1 = • t2 = • t and t1 • = t2 • = t• (see Fig. 8(b)). – α-morphism ϕR2 : N 0 → N , where N 0 = ρR2 (N, {t}), maps transitions t1 and t2 in N 0 to a single transition t in N . For other nodes in N 0 , ϕR2 is the identity mapping between N 0 and N . (a) refinement rule R1 (b) refinement rule R2 Fig. 8. Place and transition duplication R3: Local transition introduction – applicability constraints: a place p in N . – transformation: substitution of p with a transition t (see Fig. 9), s.t.: 1. • t = {p1 } and t• = {p2 }; 2. p1 • = • p2 = {t}; 3. • p1 = • p and p2 • = p• ; 4. p1 ∈ m00 ⇔ p ∈ m0 . – α-morphism ϕR3 : N 0 → N , where N 0 = ρ3 (N, {p}), maps t, p1 and p2 in N 0 to a single place p in N . For other nodes in N 0 , ϕR3 is the identity mapping between N 0 and N . The refinement rules ρR1 , ρR2 and ρR3 , similar to their abstraction counter- parts ρA1 , ρA2 and ρA3 , can be easily generalized. Property-Preserving Transformations 61 Fig. 9. Refinement rule R3: local transition introduction R4: Place split – applicability constraints: a place p in N , s.t. |• p| > 1. – transformation: split p into two places p1 and p2 (see Fig. 10), s.t.: 1. • p1 ⊂ • p and • p2 ⊂ • p; 2. • p1 ∩ • p2 = ∅ and • p1 ∪ • p2 = • p; 3. |p1 • | = |p2 • | = |p• |, and there is a bijection fi : pi • → p• with i = 1, 2, s.t. if fi (x) = b for x ∈ pi • and b ∈ p• , then h0 (x) = h(b); 4. • (pi • ) \ {pi } = • (p• ) \ {p} with i = 1, 2; 5. if p ∈ m0 , then p1 ∈ m00 ⇔ p2 ∈ / m00 . – α-morphism ϕR4 : N → N , where N 0 = ρR4 (N, {p}), maps places p1 and 0 p2 in N 0 to a single place p in N . For other nodes in N 0 , ϕR4 is the identity mapping between N 0 and N . While splitting a place p in N , we also split its neighborhood between p1 and p2 in ρR4 (N, {p}). According to constraints 1 and 2, the preset of p is divided into two disjoint, proper and non-empty subsets. According to constraints 3 and 4, the postsets of p1 and p2 are exactly two copies of the postset of p, s.t. labels of transitions are also preserved. Moreover, by constraint 4, if there are other input places to the postset of p in N , then they are also input places to the postsets of p1 and p2 in ρR4 (N, {p}). These requirements on splitting the neighborhood of p in N are based on the requirements 5b and 5c of Definition 1 (α-morphisms). Fig. 10. Refinement rule R4: place split We continue by discussing the main properties of the proposed refinement rules. Let RR = {ρR1 , . . . , ρR4 } be the set of refinement rules. By construction, application of the refinement rules induces an α-morphisms from a transformed SMD-EN system to an initial SMD-EN system. This also 62 Luca Bernardinello, Irina Lomazova, Roman Nesterov, Lucia Pomello follows from the fact that rules ρR1 , ρR2 and ρR3 are the inverse of the abstraction rules ρA1 , ρA2 and ρA3 respectively. Proposition 4. Let ρ ∈ RR, s.t. ρ is applicable to a subnet N (XL ) in N . Then there is an α-morphism ϕρ : ρ(N, XL ) → N . Corollary 2. Let ρ1 , ρ2 ∈ RR, s.t. ρ2 is applicable to a subnet in ρ1 (N, XL ) gen- erated by XL0 . Then there is an α-morphism ϕρ2 ◦ ϕρ1 : ρ2 (ρ1 (N, XL ), XL0 ) → N . Similarly to the abstraction rules, we also observe that application of the refinement rules does not introduce “new” deadlocks to transformed models, i.e., any deadlock in a refined EN system is an image of a deadlock already present in an initial abstract EN system. Proposition 5. Let ρ ∈ RR, s.t. ρ is applicable to a subnet N (XL ) in N . Let m0 ∈ [m00 i be a deadlock in ρ(N, XL ). Then ϕρ (m0 ) is a deadlock in N . Proof. Follows from the structural characterization of a deadlock in an SMD-EN system and from the fact that application of the refinement rules, that results in splitting places (thus generating new images of reachable markings in an initial model N ), fully preserves their neighborhoods. 4 Use of Transformations for Workflow Net Composition In this section, we demonstrate application of transformations defined in the pre- vious section to a correct composition of interacting workflow net components. Workflow nets have both initial and final markings. We follow an approach to a correct composition of generalized workflow nets (GWF-nets) described in [4], and the correctness of this approach is achieved through the use of α- morphisms. GWF-nets interact by synchronizations and by sending/receiving messages through asynchronous channels. GWF-net interactions are specified using transition labels. Below we recall main formal definitions. In our paper, we consider workflow nets covered by sequential components. As mentioned in [1], state machine decomposability is a basic feature that bridges structural and behavioral properties of workflow nets. Definition 2. A generalized workflow net (GWF-net) is an SMD-EN system N = (P, T, F, m0 , mf ), where: 1. • m0 = ∅. 2. mf ⊆ P , s.t. mf 6= ∅ and mf • = ∅. 3. ∀x ∈ P ∪ T ∃s ∈ m0 ∃f ∈ mf : (s, x) ∈ F ∗ and (x, f ) ∈ F ∗ , where F ∗ is the reflexive transitive closure of F . Soundness is the main correctness property of workflow nets. Definition 3. A GWF-net N = (P, T, F, m0 , mf ) is sound iff: Property-Preserving Transformations 63 1. ∀m ∈ [m0 i : mf ∈ [mi. 2. ∀m ∈ [m0 i : m ⊇ mf ⇒ m = mf . 3. ∀t ∈ T ∃m ∈ [m0 i : m[ti. The composition of two GWF-nets N1 and N2 is a GWF-net denoted by N1 ~ N2 , s.t. it is fully defined according to transition labels: (a) fusion of transitions with a common synchronous label, (b) addition of a place for an asynchronous channel between two transitions with complement asynchronous labels (sending and receiving). The main result of [4] on composition correctness is formulated in the fol- lowing proposition. Proposition 6. Let R1 , R2 and A1 , A2 be four sound GWF-nets, s.t. ϕi : Ri → Ai is an α-morphism with i = 1, 2. If A1 ~ A2 is sound, then R1 ~ R2 sound. Thus, the composition of two detailed GWF-net R1 ~ R2 is sound if the com- position of their abstractions A1 ~ A2 is sound. Intuitively, A1 ~ A2 models an abstract protocol of interactions (also referred to as an interaction pattern) be- tween detailed GWF-net components. We use transformation rules to construct corresponding α-morphisms as shown in the two following subsections. 4.1 Abstraction of Interacting Workflow Net Components Here we show application of abstraction rules to build abstract representations of interacting GWF-net components. Fro example, we construct the α-morphism shown in Fig. 2 step by step. Transitions e1 , e2 , f1 , f2 , g1 , g2 , h1 , h2 in N1 are considered to be labeled by names of communication actions from Λ, s.t. h(e1 ) = h(e2 ), h(f1 ) = h(f2 ), h(g1 ) = h(g2 ) and h(h1 ) = h(h2 ), whereas transitions y1 , . . . , y7 in N1 are local. Firstly, local transitions y1 , . . . , y5 can be eliminated using the rule ρA3 for five times. After collapsing these local transitions, we simplify places p1 and p2 (the rule ρA1 ) that are generated from eliminating local transitions y4 and y5 correspondingly. Figure 11 gives a concise illustration of these transformations. Now local transitions y7 and y8 are also eliminated using the rule ρA3 twice (see the transformation 3 in Fig. 12). Unfortunately, the fourth transformation shown in Fig. 12 cannot be obtained using the existing simple abstraction rules. We fuse transitions f1 and f2 , h1 and h2 , g1 and g2 preserving their labels as well as we fuse places p3 and p4 , p5 and p6 in the neighborhood of these transitions. Intuitively, this may bee seen as an example of a direct application of Definition 1 by constructing appropriate fusions. We plan to investigate possible local transformations behind this in the future. Finally, we simplify transitions e1 and e2 (abstraction rule ρA2 ) and obtain the target abstract EN system previously shown in Fig. 2. To construct the cor- responding map between models, we need to compose all α-morphisms induced by applied abstraction rules and by a direct application of Definition 1. 64 Luca Bernardinello, Irina Lomazova, Roman Nesterov, Lucia Pomello Fig. 11. Abstracting a GWF-net: steps 1 and 2 Fig. 12. Abstracting a GWF-net: steps 3 and 4 4.2 Refinement of Interaction Patterns In this section, we apply the refinement rules defined in the previous section and solve the inverse problem: the construction of a detailed system model that preserves properties of an initial abstract model. As described above, a composition of abstract representations of interacting GWF-net components models an interaction pattern GWF-net components com- municate according to. In [16], typical interaction patterns for asynchronously communicating GWF-net components have been discussed. Abstract interaction patterns provide generic solutions that can be used to model and verify compo- nent interactions in large-scale distributed systems. Accordingly, a formal model of an abstract interaction pattern is a composition of GWF-nets. Consider a pattern shown in Fig. 13 (refer to “Send-Receive” interaction pattern in [16]). It models a message exchange between two components: the left sends a message to the right, while the right sends a response back to the left. We aim to construct a possible refinement of this pattern using simple rules. Figure 14 gives a concise illustration for building a possible refinement of the “Send-Receive“ interaction pattern. We describe applied refinement rules below. Property-Preserving Transformations 65 Fig. 13. “Send-Receive” asynchronous interaction pattern Fig. 14. Refinement of the interaction pattern from Fig. 13 Firstly, we duplicate the place p1 (rule ρR1 ) and introduce a local transition instead of the place p2 (rule ρR3 ). Secondly, we also introduce local transitions instead of copies of the place p1 , and we duplicate the transition t2 (rule ρR2 ). The last transformation shown in Fig. 14 is the split of the place p3 according to the refinement rule ρR4 . Refinement process may be continued until the target detail level is achieved. 5 Conclusion In this paper, we have studied the problem of abstracting and refining elemen- tary net systems with the help of α-morphisms. Direct construction of these morphisms is a complicated task. To solve it, we have proposed a set of ab- straction/refinement transformation rules. Step-wise application of these trans- formations rules induces corresponding α-morphisms between initial and trans- formed models. Some of the transformations (the abstraction rules A1-A3 and their refinement counterparts) have been already discussed in the literature, while the others are new and have been developed in accordance with the def- inition of α-morphisms. We note that applicability constraints of the proposed transformation rules can be efficiently computed. Moreover, locality of abstrac- tion/refinement transformation rules proposed in our study allows us to preserve 66 Luca Bernardinello, Irina Lomazova, Roman Nesterov, Lucia Pomello and reflect not only reachable markings, but also deadlocks. Thus structural con- straints of transformation rules make impossible to lose or introduce deadlocks in models. In addition, we have demonstrated how transformation rules can be applied to compose models of interacting workflow net components. There are several open theoretical questions that we intend to study in future. It is planned to extend transformations defined in the paper with more liberal yet controlled ways of introducing concurrency rather than by duplicating places only, e.g., it is possible to consider introduction and detection of implicit places. In this light, it is also rather interesting to study the completeness problem, for instance, to establish whether transformations allows to generate all possible refinements of a given abstract EN system preserving its properties. Moreover, we also plan to characterize properties of irreducible EN systems. References 1. van der Aalst, W.M.P.: Workflow verification: Finding control-flow errors using Petri-net-based techniques. In: van der Aalst, W., Desel, J., Oberweis, A. (eds.) Business Process Management: Models, Techniques, and Empirical Studies. LNCS, vol. 1806, pp. 161–183. Springer, Heidelberg (2000) 2. Bernardinello, L., Mangioni, E., Pomello, L.: Local state refinement and composi- tion of elementary net systems: An approach based on morphisms. In: Koutny, M., van der Aalst, W., Yakovlev, A. (eds.) ToPNoC VIII. LNCS, vol. 8100, pp. 48–70. Springer, Heidelberg (2013) 3. Bernardinello, L., De Cindio, F.: A survey of basic net models and modular net classes. In: Rozenberg, G. (ed.) Advances in Petri Nets 1992. LNCS, vol. 609, pp. 304–351. Springer, Heidelberg (1992) 4. Bernardinello, L., Lomazova, I., Nesterov, R., Pomello, L.: Soundness-preserving composition of synchronously and asynchronously interacting workflow net com- ponents (2020), https://arxiv.org/pdf/2001.08064.pdf 5. Berthelot, G.: Checking properties of nets using transformations. In: Rozenberg, G. (ed.) Advances in Petri Nets 1985. LNCS, vol. 222, pp. 19–40. Springer, Heidelberg (1986) 6. Berthelot, G., Roucairol, G.: Reduction of Petri-nets. In: Mazurkiewicz, A. (ed.) Mathematical Foundations of Computer Science 1976. LNCS, vol. 45, pp. 202–209. Springer, Heidelberg (1976) 7. Desel, J., Merceron, A.: Vicinity respecting homomorphisms for abstracting system requirements. In: Jensen, K., Donatelli, S., Koutny, M. (eds.) ToPNoC IV. LNCS, vol. 6550, pp. 1–20. Springer, Heidelberg (2010) 8. Ehrig, H., Hoffmann, K., Padberg, J.: Transformations of Petri nets. Electronic Notes in Theoretical Computer Science 148(1), 151–172 (2006) 9. Esparza, J., Silva, M.: Top-down synthesis of live and bounded free choice nets. In: Rozenberg, G. (ed.) Advances in Petri Nets 1991. LNCS, vol. 524, pp. 118–139. Springer, Heidelberg (1991) 10. Genrich, H., Thiagarajan, P.: A theory of bipolar synchronisation schemes. Theo- retical Computer Science 30(3), 241–318 (1984) 11. Hack, M.: Analysis of production schemata by Petri nets. TR-94. MIT, Boston (1972) Property-Preserving Transformations 67 12. Lomazova, I.A.: Resource equivalences in Petri nets. In: van der Aalst, W., Best, E. (eds.) Application and Theory of Petri Nets and Concurrency. LNCS, vol. 10258, pp. 19–34. Springer, Heidelberg (2017) 13. Mikolajczak, B., Z., W.: Conceptual modeling of concurrent systems through step- wise abstraction and refinement using Petri net morphisms. In: Song, I., Liddle, S., Ling, T., Scheuermann, P. (eds.) Conceptual Modeling - ER 2003. LNCS, vol. 2813, pp. 433–445 (2003) 14. Murata, T.: Petri nets: Properties, analysis and applications. Proceedings of the IEEE 77(4), 541–580 (1989) 15. Murata, T., Suzuki, I.: A method for stepwise refinement and abstraction of petri nets. Journal of Computer and System Sciences 27(1), 51–76 (1983) 16. Nesterov, R., Lomazova, I.: Asynchronous interaction patterns for mining multi- agent system models from event logs. In: Lomazova, I., Kalenkova, A., Yavorsky, R. (eds.) Proceedings of the MACSPro Workshop 2019. CEUR Workshop Proceed- ings, vol. 2478, pp. 62–73. CEUR-WS.org (2019) 17. Nielsen, M., Winskel, G.: Petri nets and bisimulations. Theoretical Computer Sci- ence 153, 211–244 (1996) 18. Padberg, J., Urbášek, 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: Advances in Petri Nets. LNCS, vol. 2472, pp. 161– 196. Springer, Heidelberg (2003) 19. Rozenberg, G., Engelfriet, J.: Elementary net systems. In: Reisig, W., Rozenberg, G. (eds.) Lectures on Petri Nets I: Basic Models: Advances in Petri Nets. LNCS, vol. 1491, pp. 12–121. Springer, Heidelberg (1998) 20. Schnoebelen, P., Sidorova, N.: Bisimulation and the reduction of Petri nets. In: Nielsen, M., Simpson, D. (eds.) Application and Theory of Petri Nets 2000. LNCS, vol. 1825, pp. 409–423. Springer, Heidelberg (2000) 21. Valette, R.: Analysis of Petri nets by stepwise refinements. Journal of Computer and System Sciences 18(1), 35–46 (1979) 22. Winskel, G.: Petri nets, algebras, morphisms, and compositionality. Information and Computation 72(3), 197–238 (1987)