On the synthesis of industry level process models from enterprise level process models Pieter Kwantes and Jetty Kleijn LIACS, Leiden University, P.O.Box 9512 NL-2300 RA Leiden, The Netherlands {p.m.kwantes,h.c.m.kleijn}@liacs.leidenuniv.nl Abstract. In this paper we provide a framework to specify the synthesis of a comprehensive (industry level) process model from a set of lower level (enterprise) process models. This framework allows us to verify that the resulting model is compliant with a given blueprint (reference model), using local checks only. The reference model describes the intended interactions between the enterprise processes in accordance with industry standards. We propose an approach that allows to check compliance locally per enterprise without requiring information from other enterprise models. This implies in particular that there is no need for individual enterprises to disclose internal design information to the public domain. In our general set-up, we use Petri nets as a modelling framework for our process models and labelled transition systems with silent actions as their semantics. Branching bisimilarity of their transition systems is here the criterion for compliance of process models. Keywords: business process modelling, Petri net, industry and enterprise level, synthesis, verification, (partitioned) labelled tran- sition system, qualified branching bimilarity 1 Introduction Industry level standardisation is a prerequisite for interoperability between business processes of the enterprises in an industry. 1 Typical areas eli- gible for standardisation include communication, eg., the syntax of mes- sages exchanged between business processes, and the flow of control of this communication, i.e., who sends which messages in which order to whom.2 1 We use the term “industry” here rather loosely to include, eg., any group of enterprises involved in the supply chain for a particular good or service. 2 Industry level institutions for message syntax standardisation are quite com- mon, eg., SWIFT for Financial services [23], HL7 for Health care [14], Roset- taNet for the electronics industry [12], EDSN for the Dutch energy market [7] to name just a few. 6 Interoperability between business processes is therefore dependent on the compliance of these business processes with industry standards. The flow of control at the industry level emerges from the interaction of business processes at the enterprise level. However, the design (and verification) of business processes at the enterprise level is typically the exclusive domain of the enterprise in question. To align the design of (enterprise level) business processes with the required behaviour emerging at the industry level, poses a significant and costly coordination problem for the enterprises involved. As an example, consider the settlement of a transaction on the sec- ondary capital market (eg., buying or selling of a security). This is an industry level process that emerges from the interaction of several business processes at the enterprise level like those of Investors, Brokers, Counter- parties, Custodians and Banks, but there could be (many) more depending on the nature of the transaction. Such interaction typically involves the bilateral asynchronous exchange of standardized messages between these enterprise level processes 3 . This is where the coordination problem arises. First of all because there is no central authority to ensure that (enterprise level) implementation decisions are compliant with the requirements, i.e., the intended flow of control, at the industry level. Moreover the specifi- cations of these requirements are often informal and/or incomplete. Any approach aiming to solve this problem should take into account that, as a rule, implementation decisions are taken locally, at the enterprise level. We cannot, in general, assume the presence of an entity with the authority to align these local decisions with global requirements 4 In this paper we demonstrate how this problem could be solved by outlining an approach to establish an enterprise’s (local) compliance with a (global) industry level reference model on basis of local checks. Petri nets provide the modelling framework for our process models with labelled transition systems with silent actions as their semantics. We introduce En- terprise nets (E-nets) that can exchange messages with other E-nets, to represent enterprise process models and Industry nets (I-nets), composed of communicating E-nets, to represent process models at the industry level. A publicly available I-net reflecting the intended flow of control of commu- nication for a particular industry level process, serves as a reference model for enterprises participating in that process, but is not concerned with how enterprises organise themselves internally. This reference model can be con- sidered as a (minimum) set of operational requirements negotiated at the 3 eg., XML messages, meeting the ISO20022 standard, exchanged over the SWIFT-network. 4 Although in many cases industry level institutions, like the ones mentioned earlier, have emerged to facilitate the negotiation of certain industry level stan- dards. 7 industry level. The implementation of the reference model, i.e., the syn- thesis of implementations provided by the individual enterprises, should be compliant with these requirements. Compliance relates to communicating behaviour. We use labelled tran- sition systems with silent actions to represent the behaviour of E-nets and I-nets, and branching bisimilarity to define compliance. Silent actions rep- resent non-communicating behaviour. Bisimilarity is a well established ap- proach for relating behaviours in this set up [1, 22]. Branching bisimilarity is the finest bismilarity relation that ignores differences in non-communicating behaviour while respecting its branching structure [8, 9]. This appears to be a good point to start our investigation into the notion of compliance, which is defined in more detail later on. To reflect their modular structure, we introduce labelled transition systems with a partition of their labels, as an additional semantic model for I-nets. This leads to a notion of qualified branching bisimilarity, suitable for such transition systems. This auxiliary notion facilitates the proof that — indeed — compliance can be verified locally. Consequently, we arrive at the main result that, when combining enterprise models into an industry level process model that should be com- pliant with a given blueprint, local compliance checks suffice. Our approach is an original contribution to existing approaches towards local verification of compliant global behaviour. First of all, it includes a modelling framework with a strong built in separation of concerns between global (domain specific) requirements laid down in an (industry level) refer- ence model and local implementation decisions left to enterprises. Secondly, many existing approaches appear to be mainly concerned with the verifica- tion of general correctness properties (like deadlock freeness, soundness, or accordance) while here we are particularly concerned with the verification of domain specific requirements as laid down in the global reference model. The paper is organised as follows. In Sections 2 and 3, we provide a pre- cise definition of E-nets and I-nets and their implementations. In Section 4 compliance is defined and we formulate the main theorem that global com- pliance can be verified locally. In Section 5 we introduce qualified branching bisimilarity for partitioned labelled transition systems. In Section 6 an out- line is given for the proof of our main result as presented in Section 4. Finally, related work is discussed in Section 7, while Section 8 forms the conclusion of the paper. 2 Enterprise nets and Industry nets N = {0, 1, 2, · · · } is the set of natural numbers. Given a natural number n ≥ 1, we denote the set {j ∈ N | 1 ≤ j ≤ n} by [n]. Let L be a set. Then L∗ is the set consisting of all finite sequences w = a1 · · · am of elements 8 ai ∈ L for i ∈ [m]. If m = 0, then w is the empty sequence, denoted by λ. If ai = a for all i ∈ [m], then we may write w = am . In particular, for all a ∈ L, we have that a0 is the empty sequence. A Petri net is a triple N = (P, T, F ), where P is a finite set of places, T is a finite set of transitions such that (P ∩T ) = ∅, and F ⊆ (P ×T )∪(T ×P ) is a set of arcs (flow relation). We refer to the elements of P ∪ T as the nodes of N . If N 0 is a Petri net such that N and N 0 have disjoint sets of nodes then N and N 0 are called disjoint. Let N = (P, T, F ) be a Petri net. Then • x = {y | (y, x) ∈ F } and • x = {y | (x, y) ∈ F } are the preset and the postset respectively, of the node x ∈ P ∪ T . A place p ∈ P such that • p = ∅ is a source place of N . A marking of N is a function µ : P → N. Let t ∈ T and µ a marking of N . Then t is enabled at µ if µ(p) > 0 for all p ∈ • t. If t is enabled at µ, t it may occur, leading to a new marking µ0 . This we write as µ → − µ0 with µ (p) = µ(p) − 1 whenever p ∈ t \ t ; µ (p) = µ(p) + 1 whenever p ∈ t• \ • t; 0 • • 0 t and µ0 (p) = µ(p) otherwise. We extend the notation µ → − µ0 to sequences λ wt w ∈ T ∗ as follows: µ − → µ for all µ and µ −→ µ0 for markings µ, µ0 of N , w w ∈ T and t ∈ T , whenever there is a marking µ00 such that µ − ∗ → µ00 and t w µ00 → − µ0 . If µ −→ µ0 , for some w ∈ T ∗ , we say that µ0 is reachable from µ. [µi is the set of markings reachable from µ. The marking µ of N such that, for all p ∈ P , µ(p) = 1 if p is a source place and µ(p) = 0 otherwise, is the default initial marking of N . Let M be the set of message types fixed throughout this paper. Enter- prise nets, to be defined next, are Petri nets that can communicate (asyn- chronously) through the occurrence of output and input transitions with matching message types. They have a single source place, resembling the notion of workflow-nets in that respect, but without a designated final marking. Composition of these lower level nets results in a higher level net with multiple source places. We are particularly interested in the global communicating behaviour that emerges from bilateral interactions between local processes. Definition 1 (Enterprise net). An Enterprise net, E-net for short, is a tuple E = (P, [Tint , Tinp , Tout ], F, M ) such that Tint , Tinp , and Tout are mutually disjoint sets; Tint is the set of internal transitions of E, Tinp its set of input transitions, and Tout its set of output transitions; moreover, (P, Tint ∪ Tinp ∪ Tout , F ), the underlying Petri net of E, is a Petri net with exactly one source place; finally M : Tinp ∪Tout → M is the communication function of E. The triple (Tinp , Tout , M ) is the interface of E. 9 We assume that the E-nets that constitute an Industry net (defined below) are disjoint, i.e., their underlying Petri nets are disjoint. Moreover the input and output transitions of these nets can be matched. Definition 2 (Matching). Let n ≥ 2. Let V = {Ei | i ∈ [n]} be a set of pairwise disjoint E-nets. Let, for each i ∈ [n], Tout,i be the set of output tran- sitions of Ei , Tinp,i its set of input transitions,Sand Mi its communication S function. A matching over V is a bijection ϕ : i∈[n] Tout,i → j∈[n] Tinp,j such that whenever t ∈ Tout,i and ϕ(t) ∈ Tinp,j , for some i, j, then i 6= j and Mi (t) = Mj (ϕ(t)). A set V of mutually disjoint E-nets is said to be composable if there exists a matching over V . Note that not every such V is composable; and if it is, there may exist more than one matching over this set. Given a composable set V as specified in Definition 2, and a matching ϕ over V , the nets in V are connected through (new) channel places from the set P (V, ϕ) = {[t, ϕ(t)] | t ∈ Tout,i , i ∈ [n]} using the channel arcs from F (V, ϕ) = {(t, [t, ϕ(t)]) | t ∈ Tout,i , i ∈ [n]} ∪ {([t, ϕ(t)], ϕ(t)) | t ∈ Tout,i , i ∈ [n]}. Definition 3 (Industry net). Let n ≥ 2. Let V = {Ei : i ∈ [n]} be a com- posable set of disjoint E-nets with Ei = (Pi , [Tint,i , Tinp,i , Tout,i ], Fi , Mi ) for all i ∈ [n], and let ϕ be a matching over V . The Industry net, or I- net for S short, over (V, ϕ), denoted S I(V, ϕ), is theSPetri net (P, T, F ) with P = i∈[n] Pi ∪ P (V, ϕ), T = i∈[n] Ti , and F = i∈[n] Fi ∪ F (V, ϕ). S The Petri net (P (V, ϕ), T \ i∈[n] Tint,i , F (V, ϕ)) is the communication sub- net of I(V, ϕ). Note that I-nets are (communication-)closed systems, in the sense that all transitions that occur as an output (input) transition in one of the E- nets are connected through a channel place with a matching input (output, respectively) transition of another E-net. 3 Implementations We assume the existence of a publicly available I-net reflecting the intended flow of control of communication for a particular industry level process and serving as a reference model for the enterprises that will participate in that process. The idea is that each of these enterprises provides a local implementation of one of the E-nets in the reference model. The aim of the reference model however is not concerned with how they are organised internally. It only prescribes the communication requirements at a global 10 (industry) level and the local implementations (E-nets themselves) should obey these requirements. To ensure that all implementations “fit together” (match) as prescribed by the reference model, each should have the same interface as the E-net it implements. We assume moreover that the E-nets of different enterprises are always disjoint (eg., by proper indexing). Let n ≥ 2. Let V = {Ei : i ∈ [n]} be a composable set of E-nets and let ϕ be a matching over V . Let I(V, ϕ) be a reference model. Definition 4 (Implementation). Let E ∈ V . An E-net E 0 is an imple- mentation of E with respect to V if E 0 is disjoint with all E-nets in V \ {E} and E and E 0 have the same interface. Note that if E 0 is an implementation of E, then W = (V \ {E}) ∪ {E 0 } is composable and ϕ is a matching over W . Thus I(W, ϕ) is an I-net. Let V 0 = {Ei0 : i ∈ [n]} be a set of E-nets such that, for all i ∈ [n], Ei0 is an implementation of Ei ∈ V . Since, by our assumption above, the Ei0 are pairwise disjoint and because ϕ is a matching over V 0 , it follows that also I(V 0 , ϕ) is a well-defined Industry net. It is an (full) implementation of I(V, ϕ). Note that V 0 can inherit the matching φ from V, because by Definition 4 their E-nets have the same interface. 4 Compliance To define compliance, a notion of behaviour is needed. We use labelled transition systems to represent behaviour and branching bisimilarity as a measure of behavioural equivalence. A labelled transition system, LTS for short, is a tuple T = (Q, L, δ), where Q is a set of states, L is a set of (action) labels, and δ ⊆ Q × L × Q is a transition relation. Rather than (q, a, q 0 ) ∈ δ, where q, q 0 ∈ Q and a ∈ L, a we may also write q − → q0 . A path in T from q ∈ Q to q 0 ∈ Q is a finite sequence (q1 , a1 , q2 ), (q2 , a2 , q3 ), . . . , (qm , am , qm+1 ), where m ≥ 0, q = q1 , q 0 = qm+1 , and (qi , ai , qi+1 ) ∈ δ, for all i ∈ [m]. Such path may also be denoted as (q1 , a1 a ···am · · · am , qm+1 ) or as q1 −−1−−− → qm+1 . If m = 0 the path is empty and q = q 0 . Let L be a set of labels and l : L → L0 a function. Then l(δ) = {(q, l(a), q 0 ) : 0 (q, a, q 0 ) ∈ δ}, l(L) = {l(a) | a ∈ L} and l(T ) = (Q, l(L), l(δ)). In our process model we will hide internal actions and therefore we need the concept of a silent action. For technical reasons we introduce LTSs with more than one silent action. An LTS with silent actions is a tuple T = (Q, L, S, δ) where S ⊆ L is a set of specified silent actions. All notions and notations introduced for labelled transition systems carry over to LTSs with silent actions in the obvious way. Note that every LTS T = (Q, L, δ) 11 can be interpreted as an LTS with an empty set of silent actions (Q, L, ∅, δ). Moreover, our labelled transition systems will often be equipped with a designated initial state. Thus, an initialized LTS (with silent actions) is a tuple T = (Q, L, δ, qin ) (or T = (Q, L, S, δ, qin ), respectively) such that T = (Q, L, δ) is an LTS (or (Q, L, S, δ) is an LTS with silent actions, respectively) where qin ∈ Q is a designated initial state. We are now ready to introduce the labelled transition systems associated with an Industry net. Definition 5 (Transition System of an I-net). Let n ≥ 2. Let V = {Ei : i ∈ [n]} be a composable set of E-nets, with Ei = (Pi , [Tint,i , Tinp,i , Tout,i ], Fi , Mi ) for all i ∈ [n], ϕ a matching over V and µin the default initial marking of I(V, ϕ) = (P, T, F ). – LT S(V, ϕ) = ([µin i, T, ∅, δ, µin ), where δ = {(µ, t, µ0 ) | µ ∈ [µin i, t ∈ t T, µ →− µ0 in I(V, ϕ)}, is the initialized labelled transition system of I(V, ϕ).  S τ if t ∈ i∈[n] Tint,i – Let λV,τ : T → T ∪ {τ } be defined as λV,τ (t) = t otherwise Then λV,τ (LT S(V, ϕ)) = ([µin i, λV,τ (T ), {τ }, λV,τ (δ), µin ), is the ini- tialized labelled transition system with silent action τ of I(V, ϕ). The labelled transition system associated with the Industry net I(V, ϕ) is its marking graph with the default initial marking as initial state. Note that since each Enterprise net has exactly one source place, the Industry net has n source places, all initially marked with one token. In λV,τ (LT S(V, ϕ)), the labels of the internal transitions of the Enterprise nets constituting V , are made silent using the special symbol τ . Branching bisimilarity as a criterion for behavioural equivalence based on labelled transitions systems with a single silent action was introduced in [9]. A detailed proof that branching bisimilarity is an equivalence relation is provided in [5]. The definitions of branching bisimilarity provided in both papers are slightly different, but as explained there, they are equivalent. For the purpose of this paper, it is more convenient to follow the definition from [5]. Definition 6 (Branching bisimilarity). Let T = (Q, L, {τ }, δ) be an LTS with a unique silent action τ . Then 1. R ⊆ Q × Q is a branching bisimulation for T if - for all (p0 , q0 ) ∈ R and a ∈ L, the following holds: a (a) If p0 − → p1 in T , then a = τ and (p1 , q0 ) ∈ R or τk a there exists a path q0 −→ q1 − → q2 in T , such that k ≥ 0, (p0 , q1 ) ∈ R and (p1 , q2 ) ∈ R; 12 a (b) If q0 − → q1 in T , then a = τ and (p0 , q1 ) ∈ R or τk a there exists a path p0 −→ p1 − → p2 in T , such that k ≥ 0, (p1 , q0 ) ∈ R and (p2 , q1 ) ∈ R. 2. If (p, q) ∈ Q × Q, then p and q are branching bisimilar in T , denoted p ≈bb q, whenever there is a branching bisimulation R ⊆ Q × Q for T such that (p, q) ∈ R. 3. Two initialised labelled transition systems with τ as silent action, T1 = (Q1 , L, {τ }, δ1 , q1,in ) and T2 = (Q2 , L, {τ }, δ2 , q2,in ) such that Q1 ∩Q2 = ∅, are branching bisimilar if there exists a branching bisimulation R ⊆ Q1 × Q2 such that (q1,in , q2,in ) ∈ R. To establish whether an implementation of a reference Industry net is correct, the communicating behaviour of the implementation has to be compared with the communicating behaviour of the reference model. Definition 7 (Global compliance). Let n ≥ 2. Let V = {Ei : i ∈ [n]} be a composable set of E-nets and ϕ a matching over V . Let I(V 0 , ϕ) be an implementation of I(V, ϕ). Then I(V 0 , φ) is compliant with I(V, φ), denoted I(V 0 , φ) ' I(V, φ), if λV 0 ,τ (LT S(V 0 , φ)) ≈bb λV,τ (LT S(V, φ)). A problem here is that we cannot investigate the behaviour of the full implementation as such. The reason being that in general enterprises are reluctant to disclose information about the implementation of their internal operations to the public domain. Each enterprise has knowledge of its own operations, but not of the operations of the other enterprises. So we must assume that the full set of implementations of the enterprise nets is not known. What can be done locally however, is to investigate the behaviour of each local E-net implementation by comparing it with the behaviour of the corresponding original E-net in the reference model. To make this comparison we should consider these behaviours in the same context. We can accomplish this by replacing the E-net in the reference model with its local implementation. Definition 8 (Local compliance). Let n ≥ 2. Let V = {Ei : i ∈ [n]} be a composable set of E-nets and ϕ a matching over V . Let i ∈ [n] and Ei0 an implementation of Ei with respect to V . Let V i = (V \ {Ei }) ∪ {Ei0 }. – Then I(V i , ϕ) is the local replacement of Ei in I(V, ϕ) by Ei0 . – Ei0 is compliant with I(V, ϕ), denoted Ei0 ∼ I(V, ϕ), if λV i ,τ (LT S(V i , ϕ)) ≈bb λV,τ (LT S(V, ϕ)), for all i ∈ [n] We now claim as our main result that if local compliance is established for all local replacements of enterprise nets in the reference model, then global compliance of the full implementation follows. More formally, the following theorem holds: 13 Theorem 1. Let n ≥ 2. Let V = {Ei : i ∈ [n]} be a composable set of E-nets, ϕ a matching over V , and V 0 = {Ei0 : i ∈ [n]} where for all i ∈ [n], Ei0 an implementation of Ei with respect to V . Then I(V 0 , φ) ' I(V, φ) if Ei0 ∼ I(V, φ) for all i ∈ [n]. To prove this result, we introduce in Section 5 the new, auxiliary no- tion of qualified branching bisimilarity. This facilitates our reasoning about the equivalence of modular process specifications. In general, this concept of bisimilarity, as it is based on the distinction between different silent actions, does not coincide with branching bisimilarity. For the transition systems defined by I-nets, it can be shown however that it leads to the same equivalence classes. We will use this result to give a rough outline of the proof of Theorem 1 in Section 5. 5 Qualified branching bisimilarity Before we can introduce the new variant of branching bisimilarity, we need a modification of labelled transition systems that reflect the modular spec- ification of I-nets. A partitioned labelled transition system, or PLTS , is a tuple TP = (Q, [L1 , . . . , Ln ], δ), such that theS Li are nonempty, pairwise disjoint sets of (action) labels and T = (Q, i∈[n] Li , δ) is a labelled tran- sition system. We refer to TP as the partitioned labelled transition system derived from T and [L1 , . . . , Ln ]; and to T as the underlying labelled tran- sition system of TP . All terminology and notation introduced for labelled transition systems carry over to partitioned labelled transition systems. As with labelled transition systems we can add silent actions and an initial state to the specification of a partitioned labelled transition system. S This leads to tuples of the form (Q, [L1 , . . . , Ln ], S, δ, qin ) with S ⊆ i∈[n] Li . Definition 9 (Partitioned transition system of a I-net). Let n ≥ 2. Let V = {Ei : i ∈ [n]} be a composable set of E-nets and ϕ a matching over V . Let µin be the default initial marking of I(V, ϕ) = (P, T, F ). – Let, for all i ∈ [n], Ni = (Pi , Ti , Fi ) be the underlying Petri net of Ei . Then PLT S(I(V, ϕ)) = ([µin i, [T1 , . . . , Tn ], ∅, δ, µin ), the PLTS derived from LT S(V, ϕ) and [T1 , . . . , Tn ], is the initialized partitioned labelled transition system of I(V, ϕ). – Let, for each i ∈ [n], Tint,i be the set of internal actions of Ei . Let S = {(τ, i) | i ∈ [n]} be a set of n new (silent action) labels, S where (τ, i) is associated with Ei , for i ∈ [n]. Let `V,S : T → (T \ i∈[n] Tint,i ) ∪ S be defined as (τ, i) if t ∈ Tint,i for some i ∈ [n] `V,S (t) = t otherwise 14 Then `V,S (PLT S(I(V, ϕ))) = ([µin i, [`(T1 ), . . . , `(Tn )], S, `(δ), µin ), is the initialized labelled transition system with silent actions S of I(V, ϕ). In what follows, we write PLT S(V, ϕ) rather than PLT S(I(V, ϕ)). The specification of the transition system PLT S(V, ϕ)) provides a par- tition of its labels according to the enterprise nets from V . Moreover, the labels of the internal transitions of each Enterprise net Ei ∈ V are made silent using a dedicated symbol (τ, i). The following notion of branching bisimilarity requires that in each sim- ulation all actions (silent and non-silent ones) come from the same subset of labels. Definition 10 (Qualified branching bisimulation). Let n ≥ 2. Let T = (Q, [L1 , · · · , Ln ], S, δ) be a PLTS with silent actions. Let, for all i ∈ [n], Si = Li ∩ S. Then 1. R ⊆ Q × Q is a qualified S branching bisimulation for T if - for all (p0 , q0 ) ∈ R and a ∈ i∈[n] Li , the following holds: a (a) if p0 − → p1 , then a ∈ S and (p1 , q0 ) ∈ R or w a a ∈ Li for some i ∈ [n] and there exists a path q0 − → q1 − → q2 in T such that w ∈ Si∗ , (p0 , q1 ) ∈ R and (p1 , q2 ) ∈ R; a (b) if q0 − → q1 , then a ∈ S and (p0 , q1 ) ∈ R or w a a ∈ Li for some i ∈ [n] and there exists a path p0 − → p1 − → p2 in T such that w ∈ Si∗ , (p1 , q0 ) ∈ R and (p2 , q1 ) ∈ R. 2. Let p, q ∈ Q. Then p and q are qualified branching bisimilar in T , de- noted p ≈qb q, whenever there exists a qualified branching bisimulation R ⊆ Q × Q for T such that (p, q) ∈ R. 3. Two initialised partitioned labelled transition systems with silent actions T1 = (Q1 , [L1 , . . . , Ln ], S, δ1 , q1,in ) and T2 = (Q2 , [L1 , . . . , Ln ], S, δ2 , q2,in ) such that Q1 ∩ Q2 = ∅, are qualified branching bisimilar, denoted T1 ≈qb T2 , if q1,in and q2,in are qualified branching bisimilar in (Q1 ∪ Q2 , [L1 , . . . , Ln ], S, δ1 ∪ δ2 ). Branching bisimilarity does not imply qualified branching bisimilarity. Con- sider Figure 1. Let L1 = {a1 }, L2 = {a2 , τ2 }, L = L1 ∪ L2 and S = {τ2 }. Let T1 = ({p1 , p2 }, L, S, {(p1 , a1 , p2 )}, p1 ) and T2 = ({q1 , q2 , q3 }, L, S, {(q1 , τ2 , q2 ), (q2 , a1 , q3 )}, p1 ) be two initialized LTS s (with silent action τ = τ2 ). Then the dotted lines in Figure 1 represent a branching bisim- ulation between T1 and T2 . Now let T1,P = ({p1 , p2 }, [L1 , L2 ], S, {(p1 , a1 , p2 )}, p1 ) be the initial- ized PLTS with silent actions derived from T1 and [L1 , L2 ] and T2,P = ({q1 , q2 , q3 }, [L1 , L2 ], S, {(q1 , τ2 , q2 ), (q2 , a1 , q3 )}, p1 ) the initialized PLTS 15 p1 q1 p2 q2 q3 Fig. 1: ≈bb does not imply ≈qb with silent actions derived from T2 and [L1 , L2 ]. Then it is not possible to find a qualified branching bisimulation between T1,P and T2,P because a1 and τ2 are from different subsets of labels. However there is a strong relationship between branching bisimilarity and qualified branching bisimi- larity for labelled transition systems of I-nets which is captured in Theorem 2. Theorem 2 (≈bb and ≈qb for I-nets). Let n ≥ 2. Let V = {Ei : i ∈ [n]} and V 0 = {Ei0 : i ∈ [n]} be composable sets of E-nets. Let ϕ be a matching over V and ϕ0 a matching over V 0 . Let S = {(τ, i) | i ∈ [n]} be a set of n new action labels, with for all i ∈ [n], (τ, i) associated with Ei in V and with Ei0 in V 0 . Then λV,τ (LT S(V, ϕ)) ≈bb λV 0 ,τ (LT S(V 0 , ϕ)) if and only if `V,S (PLT S(V, ϕ)) ≈qb `V 0 ,S (PLT S(V 0 , ϕ)). The if direction of Theorem 2 follows directly from Definitions 5, 6, 9 and 10. To prove the only-if direction is however more involved. The basic idea is as follows (we sketch the qualified simulation of `V,S (PLT S(V, ϕ)) by `V 0 ,S (PLT S(V 0 , ϕ))). From λV,τ (LT S(V, ϕ)) ≈bb λV 0 ,τ (LT S(V 0 , ϕ)) it follows that when a transition labelled a from an Enterprise net Ei ∈ V is simulated by a sequence wa in λV 0 ,τ (LT S(V 0 , ϕ)), then w can be any combination of silent actions from various E-nets in V 0 . Because of the modularity of I-nets and the Petri net semantics it is then possible to first execute the transitions underlying the occurrences in w from Ei0 (labelled by (τ, i)). These form a sequence w0 and it can be shown that qualified branching bisimilarity is preserved after w0 a. 6 Outline of proof of Theorem 1 In this section we sketch a proof of Theorem 1. For the sake of convenience we repeat the statement here: Theorem 1 Let n ≥ 2. Let V = {Ei : i ∈ [n]} be a composable set of E-nets, ϕ a matching over V , and V 0 = {Ei0 : i ∈ [n]} where for all i ∈ [n], 16 Ei0 is an implementation of Ei with respect to V . Then I(V 0 , φ) ' I(V, φ) if, for all i ∈ [n], Ei0 is locally compliant with I(V, ϕ). Let us assume that, for all i ∈ [n], Ei0 is locally compliant with I(V, ϕ), that is λV i ,τ (LT S(V i , ϕ)) ≈bb λV,τ (LT S(V, ϕ)), see Definition 8. Recall that V i = (V \ {Ei }) ∪ {Ei0 }. From Theorem 2 we have `V,S (PLT S(V, ϕ)) ≈qb `V i ,S (PLT S (V i , ϕ)) for all i ∈ [n]. We will argue next how from this we can deduce that `V,S (PLT S(V, ϕ)) ≈qb `V 0 ,S (PLT S(V 0 , ϕ)). The theorem then follows from Theorem 2. Let µin and µ0in be the default initial markings of I(V, ϕ) and I(V 0 , ϕ), respectively. For all i ∈ [n], µiin denotes the default initial marking of I(V i , ϕ) and Ri ⊆ [µin i × [µiin i is a qualified branching bisimulation be- tween `V,S (PLT S(V, ϕ)) and `V i ,S (PLT S(V i , ϕ)). In addition, we define relations Zi for all i ∈ [n], consisting of all pairs of markings (µi , µ0 ) in [µiin i × [µ0in i such that µi (p) = µ0 (p) for all places p shared by I(V i , φ) and I(V 0 , φ). Note that I(V i , φ) and I(V 0 , φ) share all and only the places of Ei0 and the channel places P (V 0 , ϕ). As a consequence, if (µi , µ0 ) ∈ Zi for some i ∈ [n], then every transition t of Ei0 enabled at µi in I(V i , φ) is also enabled at µ0 in I(V 0 , φ) and vice t t versa; moreover, if µi → − µi1 in I(V i , φ) and µ0 → − µ01 in I(V 0 , φ), then also i 0 5 (µ1 , µ1 ) ∈ Zi (property A) . T Finally, we define the relation R by R = i∈[n] Ri ◦ Zi . We briefly con- sider the steps followed to establish that R is a qualified branching bisim- ulation between `V,S (PLT S(V, ϕ)) and `V 0 ,S (PLT S(V 0 , ϕ)), as desired. See Figure 2 for an illustration. The large squares in Figure 2 represent the transition systems associated with the I-nets considered. The smaller squares represent E-nets. It is easy to see that (µin , µ0in ) ∈ R. Assume (µ, µ0 ) ∈ R. Let, for all i ∈ [n], µi be such that (µ, µi ) ∈ Ri and (µi , µ0 ) ∈ Zi . a Let µ − → µ1 in `V,S (PLT S(V, ϕ)). Then there is a unique Ej such that a = `V,S (t) for some transition t of Ej . Since Rj is a qualified branching bisimulation between `V,S (PLT S(V, ϕ)) a and `V j ,S (PLT S(V j , ϕ)), it follows that µ − → µ1 can be simulated from µj w a in `V j ,S (PLT S(V j , ϕ)), as described in Definition 10, by µj − → µj1 −→ µj2 where wa is a sequence of zero or more transitions from Ej0 such that (µ, µj1 ) ∈ Rj and (µ1 , µj2 ) ∈ Rj . Then, by property A, we can conclude that 0 5 This holds for t ∈ Tint,i because Ei0 is shared between I(V i , φ) and I(V 0 , φ) and for t ∈ Ti \ Tint,i because I(V i , φ) and I(V 0 , φ) have the same communication 0 0 subnet. 17 Rj Ri R Zi Zj Fig. 2: R is a qualified branching bisimulation w a µ0 − → µ02 in `V 0 ,S (PLT S(V 0 , ϕ)) with (µj1 , µ01 ) ∈ Zj and (µj2 , µ02 ) ∈ → µ01 − Zj . Hence (µ, µ01 ) ∈ Rj ◦ Zj and (µ1 , µ02 ) ∈ Rj ◦ Zj . For all i 6= j, we can apply a similar reasoning and conclude that w0 a a sequence µi −→ µi1 − → µi2 (with w0 a a sequence from Ej ∈ V i ) in `V i ,S (PLT S(V , ϕ)) such that (µ, µi1 ) ∈ Ri and (µ1 , µi2 ) ∈ Ri . Since the i transitions involved in the simulation are not from Ei0 ∈ V i , it follows that (µi1 , µ01 ) ∈ Zi and (µi2 , µ02 ) ∈ Zi and so (µ1 , µ01 ) ∈ Ri ◦ Zi and (µ2 , µ02 ) ∈ Ri ◦ w a Zi . Consequently µ0 − → µ01 − → µ02 in `V 0 ,S (PLT S(V 0 , ϕ)) with (µ, µ01 ) ∈ R and (µ1 , µ02 ) ∈ R. a To prove the other direction, assume that (µ, µ0 ) ∈ R and µ0 − → µ01 0 in `V 0 ,S (PLT S(V , ϕ)). Again, we can identify the unique E-net with the transition t such that `V 0 ,S (t) = a and then follow a similar pattern as before. Note that qualified branching bisimulation is crucial for the conclusion that, for all i ∈ [n], the relation Zi is respected by each step in the simula- tion. 18 7 Related work The ideas underlying the concepts of E-nets, I-nets, and compliance belong to a well-established branch of research concerned with composing systems into larger correctly functioning (concurrent) systems (see, eg., [10] for an overview). In [13] Petri nets are studied equipped with distinguished input and output labels (I/O Petri nets) indicating their possibilities to communicate with other I/O Petri nets. An asynchronous composition operator intro- duces new channels for the communication between the composed nets. The transition system semantics of these nets is compositional and the composition of transition systems preserves channel properties. Composi- tion of local workflows is considered in [20]. The open workflow nets of [21] are Petri nets with interface places enabling the communication with other open workflow nets. The composition of Petri nets as considered in [20, 21] and also in [2] (open workflow nets) all combine local Petri nets extended with interface places which enables them to communicate with other Petri nets. In our approach, similarly to the approach in [13], local Petri nets do not have in- terface places but they can communicate via distinguished input and output labels. As mentioned in [13], the advantage of this approach is that it leads to a better separation of concerns: eg., the designer of a local Petri net does not have to consider whether it will be used in a synchronous or in an asyn- chronous environment later on; this should be a concern for the designer of the global Petri net. An overview of research on inter-organisational workflows is given in [4]. Much of this work is concerned with the construction of inter-organisational workflows. The Public-To-Private(P2P)approach in [3] is concerned with the construction of local workflows as subclasses of global workflows. In- heritance preserving transformations should then guarantee compliance of a local implementation (“compliance by construction”). In [6] refinement of local states of a Petri net is supported by behaviour preserving morphisms between the Petri net and its refinement. Weak bisimilarity is used as the criterion for the preservation of behaviour. The approach in [2] assumes a collaborative workflow, a multi-party contract between the participants, represented as an open workflow net and serving as a reference model. Then, a local implementation (called private view ) is in accordance with the open net included in the reference model (the public view ) if they both operate correctly (without deadlocks and terminating correctly) in the same context. Accordance can be checked locally and is compositional, i.e., if all private views are in accordance with the public view, then the overall collaborative workflow is guaranteed to 19 be deadlock-free and terminating correctly. It should be noted here that accordance is a weaker notion than compliance as considered in this paper: compliance implies accordance, but the converse does not always hold. In [18, 16, 17] Symbolic Observation Graphs (SOG) are used to repre- sent the behaviour of enterprise level business processes such that critical design information is kept private. It is shown that deadlock-freeness [18] and soundness [16] of inter-enterprise level business processes can then be verified using the composition of these enterprise level SOG’s. In [17] this approach is extended to include sharing of resources, asynchronous com- munication between enterprise level business processes and the verification of specific workflow properties using Linear Temporal Logic. 8 Conclusion We have introduced I-nets as a means to capture global requirements con- cerning communication while leaving design decisions concerning internal operations to the local level. Compliance is then defined as branching bisim- ilarity between the labelled transition system of the original (global) refer- ence model and the labelled transition system of its implementation (emerg- ing from the local implementations). The use of qualified branching bisimi- larity simplified the proof of our main theorem, Theorem 1, that local com- pliance for all local implementations implies global compliance for the global implementation. This provides a formal underpinning for an approach that allows verification of global compliance by checking local compliance only. To our knowledge this is a new result in the current approaches towards local verification of compliant global behaviour (see also the previous sec- tion on related work). In particular, our result is not comparable to the congruence results for branching bisimilarity in process algebras by which branching bisimilar processes when inserted in the same context, yield again branching bisimilar processes [11]. First of all, we did not formally intro- duce an algebra, but — more importantly — compliance does not assume or guarantee that the local processes (from the reference model and an implementation) are branching bisimilar. In [19], the industry level requirements are captured in a reference model, then projected onto the enterprise level, and subsequently trans- lated into an LTL formula. To verify that the transition system of the local replacement satisfies the LTL-formula, model checking is used. In this ap- proach, the context information in the reference model is filtered out by the projection step. Furthermore, it requires the extra step to translate the requirements laid down in the (projected) reference model into an LTL formula, which is not required in the approach presented in this paper. 20 Our approach relies essentially on well-established concepts and results in the field of Petri nets, labelled transition systems and branching bisim- ilarity. This may allow implementation of automated support for our ap- proach using already existing high performance tools incorporating proven technology like LT Smin [15] with only minor changes, for checking local compliance of E-nets. This will be the subject of future work. References 1. van der Aalst, W.M.P., Basten, T.: Inheritance of workflows: an approach to tackling problems related to change. Theor. Comput. Sci. 270(1-2), 125–203 (2002), https://doi.org/10.1016/S0304-3975(00)00321-2 2. van der Aalst, W.M.P., Lohmann, N., Massuthe, P., Stahl, C., Wolf, K.: Mul- tiparty contracts: Agreeing and implementing interorganizational processes. Comput. J. 53(1), 90–106 (2010), https://doi.org/10.1093/comjnl/bxn064 3. van der Aalst, W.M.P., Weske, M.: The P2P approach to interorganizational workflows. In: Advanced Information Systems Engineering, 13th Interna- tional Conference, CAiSE 2001, Interlaken, Switzerland, June 4-8, 2001, Pro- ceedings. pp. 140–156 (2001), http://dx.doi.org/10.1007/3-540-45341-5_ 10 4. van der Aalst, W.M.P., Weske, M.: Reflections on a decade of interorganiza- tional workflow research. In: Seminal Contributions to Information Systems Engineering, 25 Years of CAiSE, pp. 307–313 (2013), http://dx.doi.org/ 10.1007/978-3-642-36926-1_24 5. Basten, T.: Branching bisimilarity is an equivalence indeed! Inf. Process. Lett. 58(3), 141–147 (1996), http://dx.doi.org/10.1016/0020-0190(96) 00034-8 6. Bernardinello, L., Mangioni, E., Pomello, L.: Local state refinement and composition of elementary net systems: An approach based on morphisms. Trans. Petri Nets and Other Models of Concurrency 8, 48–70 (2013), https: //doi.org/10.1007/978-3-642-40465-8_3 7. EDSN: Marktfacilitering. https://www.edsn.nl/ (Mar 2018) 8. van Glabbeek, R.J.: The linear time-branching time spectrum (extended ab- stract). In: CONCUR ’90, Theories of Concurrency: Unification and Exten- sion, Amsterdam, The Netherlands, August 27-30, 1990, Proceedings. pp. 278–297 (1990), http://dx.doi.org/10.1007/BFb0039066 9. van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisim- ulation semantics. J. ACM 43(3), 555–600 (1996), http://doi.acm.org/10. 1145/233551.233556 10. Gomes, L., Barros, J.P.: Structuring and composability issues in petri nets modeling. IEEE Trans. Industrial Informatics 1(2), 112–123 (2005), https: //doi.org/10.1109/TII.2005.844433 11. Gorrieri, R., Versari, C.: Introduction to Concurrency Theory: Transition Systems and CCS. Springer International Publishing, Cham (2015), https: //doi.org/10.1007/978-3-319-21491-7_1 21 12. GS1US: Rosettanet. http://www.rosettanet.org/ (Feb 2018) 13. Haddad, S., Hennicker, R., Møller, M.H.: Channel properties of asyn- chronously composed petri nets. In: Application and Theory of Petri Nets and Concurrency - 34th International Conference, PETRI NETS 2013, Mi- lan, Italy, June 24-28, 2013. Proceedings. pp. 369–388 (2013), http://dx. doi.org/10.1007/978-3-642-38697-8_20 14. HL7: Health level seven international. http://www.hl7.org/ (Feb 2018) 15. Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: Ltsmin: High-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Anal- ysis of Systems. pp. 692–707. Springer Berlin Heidelberg, Berlin, Heidelberg (2015) 16. Klai, K., Desel, J.: Checking soundness of business processes compositionally using symbolic observation graphs. In: Giese, H., Rosu, G. (eds.) Formal Techniques for Distributed Systems - Joint 14th IFIP WG 6.1 International Conference, FMOODS 2012 and 32nd IFIP WG 6.1 International Conference, FORTE 2012, Stockholm, Sweden, June 13-16, 2012. Proceedings. Lecture Notes in Computer Science, vol. 7273, pp. 67–83. Springer (2012), https: //doi.org/10.1007/978-3-642-30793-5_5 17. Klai, K., Ochi, H.: A bottom-up approach to check the correctness of interor- ganisational workflows. In: 2015 International Symposium on Theoretical As- pects of Software Engineering, TASE 2015, Nanjing, China, September 12-14, 2015. pp. 7–14. IEEE Computer Society (2015), https://doi.org/10.1109/ TASE.2015.18 18. Klai, K., Tata, S., Desel, J.: Symbolic abstraction and deadlock-freeness ver- ification of inter-enterprise processes. In: Dayal, U., Eder, J., Koehler, J., Reijers, H.A. (eds.) Business Process Management, 7th International Con- ference, BPM 2009, Ulm, Germany, September 8-10, 2009. Proceedings. Lec- ture Notes in Computer Science, vol. 5701, pp. 294–309. Springer (2009), https://doi.org/10.1007/978-3-642-03848-8_20 19. Kwantes, P.M., Gorp, P.V., Kleijn, J., Rensink, A.: Towards compliance verification between global and local process models. In: Graph Transfor- mation - 8th International Conference, ICGT 2015, Held as Part of STAF 2015, L’Aquila, Italy, July 21-23, 2015. Proceedings. pp. 221–236 (2015), http://dx.doi.org/10.1007/978-3-319-21145-9_14 20. Martens, A.: On compatibility of web services. Petri Net Newsletter pp. 12–20 21. Massuthe, P., Reisig, W., Schmidt, K.: An Operating Guideline Ap- proach to the SOA. Humboldt-Universitat zu Berlin, Mathematisch- Naturwissenschaftliche Fakultat II, Institut fur Informatik (2005) 22. Milner, R.: Communication and concurrency. PHI Series in computer science, Prentice Hall (1989) 23. S.W.I.F.T.: Iso20022 universal financial industry message scheme. http:// www.iso20022.org (Mar 2015) 22