Introduction

Industry level standardisation is a prerequisite for interoperability between business processes of the enterprises in an industry. 1 Typical areas eligible for standardisation include communication, eg., the syntax of messages 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 common, 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.

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 secondary 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, Counterparties, 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 specifications 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 4In 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 Enterprise 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 communication 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 considered as a (minimum) set of operational requirements negotiated at the industry level. The implementation of the reference model, i.e., the synthesis of implementations provided by the individual enterprises, should be compliant with these requirements.

Compliance relates to communicating behaviour. We use labelled transition systems with silent actions to represent the behaviour of E-nets and I-nets, and branching bisimilarity to define compliance. Silent actions represent non-communicating behaviour. Bisimilarity is a well established approach 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 compliant 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) reference model and local implementation decisions left to enterprises. Secondly, many existing approaches appear to be mainly concerned with the verification 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 precise definition of E-nets and I-nets and their implementations. In Section 4 compliance is defined and we formulate the main theorem that global compliance can be verified locally. In Section 5 we introduce qualified branching bisimilarity for partitioned labelled transition systems. In Section 6 an outline 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 = a 1 • • • a m of elements a i ∈ L for i ∈ [m]

. If m = 0, then w is the empty sequence, denoted by λ. If a i = a for all i ∈ [m], then we may write w = a m . In particular, for all a ∈ L, we have that a 0 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 is a Petri net such that N and N have disjoint sets of nodes then N and N 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 µ, it may occur, leading to a new marking µ . This we write as

µ t − → µ with µ (p) = µ(p) − 1 whenever p ∈ • t \ t • ; µ (p) = µ(p) + 1 whenever p ∈ t • \ • t;

and µ (p) = µ(p) otherwise. We extend the notation µ [µ 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. Enterprise nets, to be defined next, are Petri nets that can communicate (asynchronously) 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, [T int , T inp , T out ], F, M ) such that T int , T inp , and T out are mutually disjoint sets; T int is the set of internal transitions of E, T inp its set of input transitions, and T out its set of output transitions; moreover, (P, T int ∪ T inp ∪ T out , F ), the underlying Petri net of E, is a Petri net with exactly one source place; finally M :

T inp ∪T out → M is the communication function of E. The triple (T inp , T out , M ) is the interface of E.

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 = {E i | i ∈ [n]} be a set of pairwise disjoint E-nets. Let, for each i ∈ [n],

T out,i be the set of output transitions of E i , T inp,i its set of input transitions, and

M i its communication function. A matching over V is a bijection ϕ : i∈[n] T out,i → j∈[n] T inp,j

such that whenever t ∈ T out,i and ϕ(t) ∈ T inp,j , for some i, j, then i = j and M i (t) = M j (ϕ(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 ∈ T out,i , i ∈ [n]} using the channel arcs from F (V, ϕ) = {(t, [t, ϕ(t)]) | t ∈ T out,i , i ∈ [n]} ∪ {([t, ϕ(t)], ϕ(t)) | t ∈ T out,i , i ∈ [n]}. Definition 3 (Industry net). Let n ≥ 2. Let V = {E i : i ∈ [n]} be a com- posable set of disjoint E-nets with E i = (P i , [T int,i , T inp,i , T out,i ], F i , M i ) for all i ∈ [n]

, and let ϕ be a matching over V . The Industry net, or Inet for short, over (V, ϕ), denoted I(V, ϕ), is the Petri net (P, T, F ) with

P = i∈[n] P i ∪ P (V, ϕ), T = i∈[n] T i , and F = i∈[n] F i ∪ F (V, ϕ). The Petri net (P (V, ϕ), T \ i∈[n] T int,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 Enets are connected through a channel place with a matching input (output, respectively) transition of another E-net.

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 (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 = {E i : 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 is an imple- mentation of E with respect to V if E is disjoint with all E-nets in V \ {E} and E and E have the same interface. Note that if E is an implementation of E, then W = (V \ {E}) ∪ {E } is composable and ϕ is a matching over W . Thus I(W, ϕ) is an I-net. Let V = {E i : i ∈ [n]} be a set of E-nets such that, for all i ∈ [n], E i is an implementation of E i ∈ V .

Since, by our assumption above, the E i are pairwise disjoint and because ϕ is a matching over V , it follows that also I(V , ϕ) is a well-defined Industry net. It is an (full) implementation of I(V, ϕ). Note that V can inherit the matching φ from V, because by Definition 4 their E-nets have the same interface.

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 ) ∈ δ, where q, q ∈ Q and a ∈ L, we may also write q a − → q . A path in T from q ∈ Q to q ∈ Q is a finite sequence (q 1 , a 1 , q 2 ), (q 2 , a 2 , q 3 ), . . . , (q m , a m , q m+1 ), where m ≥ 0, q = q 1 , q = q m+1 , and (q i , a i , q i+1 ) ∈ δ, for all i ∈ [m]. Such path may also be denoted as

(q 1 , a 1 • • • a m , q m+1 ) or as q 1 a1•••am − −−−− → q m+1 . If m =

0 the path is empty and q = q . Let L be a set of labels and l : L → L a function. Then l(δ) = {(q, l(a), q ) : (q, a, q

) ∈ δ}, 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, δ) 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, δ, q in ) (or T = (Q, L, S, δ, q in ), respectively) such that T = (Q, L, δ) is an LTS (or (Q, L, S, δ) is an LTS with silent actions, respectively) where q in ∈ 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 anI-net). Let n ≥ 2. Let V = {E i : i ∈ [n]} be a composable set of E-nets, with E i = (P i , [T int,i , T inp,i , T out,i ], F i , M i ) for all i ∈ [n]

, ϕ a matching over V and µ in the default initial marking of I(V, ϕ) = (P, T, F ).

-LT S(V, ϕ) = ([µ in , T, ∅, δ, µ in ), where δ = {(µ, t, µ ) | µ ∈ [µ in , t ∈ T, µ t − → µ in I(V, ϕ)}, is the initialized labelled transition system of I(V, ϕ). -Let λ V,τ : T → T ∪ {τ } be defined as λ V,τ (t) = τ if t ∈ i∈[n] T int,i t otherwise Then λ V,τ (LT S(V, ϕ)) = ([µ in , λ V,τ (T ), {τ }, λ V,τ (δ), µ in ),

is the initialized 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 (p 0 , q 0 ) ∈ R

and a ∈ L, the following holds: (a) If p 0 a − → p 1 in T , then a = τ and (p 1 , q 0 ) ∈ R or there exists a path q 0

τ k −→ q 1 a − → q 2 in T , such that k ≥ 0, (p 0 , q 1 ) ∈ R and (p 1 , q 2 ) ∈ R; (b) If q 0 a − → q 1 in

T , then a = τ and (p 0 , q 1 ) ∈ R or there exists a path p 0

τ k −→ p 1 a − → p 2 in T , such that k ≥ 0, (p 1 , q 0 ) ∈ R and (p 2 , q 1 ) ∈ 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,

T 1 = (Q 1 , L, {τ }, δ 1 , q 1,in ) and T 2 = (Q 2 , L, {τ }, δ 2 , q 2,in ) such that Q 1 ∩Q 2 = ∅, are branching bisimilar if there exists a branching bisimulation R ⊆ Q 1 × Q 2 such that (q 1,in , q 2,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 = {E i : i ∈ [n]} be a composable set of E-nets and ϕ a matching over V . Let I(V , ϕ) be an implementation of I(V, ϕ). Then I(V , φ) is compliant with I(V, φ), denoted I(V , φ) I(V, φ), if λ V ,τ (LT S(V , φ)) ≈ 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 = {E i : i ∈ [n]} be a composable set of E-nets and ϕ a matching over V . Let i ∈ [n] and E i an implementation of E i with respect to V . Let V i = (V \ {E i }) ∪ {E i }. -Then I(V i , ϕ) is the local replacement of E i in I(V, ϕ) by E i . -E i is compliant with I(V, ϕ), denoted E i ∼ 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:

Theorem 1. Let n ≥ 2. Let V = {E i : i ∈ [n]

} be a composable set of E-nets, ϕ a matching over V , and V = {E i : i ∈ [n]} where for all i ∈ [n], E i an implementation of E i with respect to V . Then I(V , φ)

I(V, φ) if E i ∼ I(V, φ) for all i ∈ [n].

To prove this result, we introduce in Section 5 the new, auxiliary notion 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.

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 specification of I-nets. A partitioned labelled transition system, or PLTS , is a tuple T P = (Q, [L 1 , . . . , L n ], δ), such that the L i are nonempty, pairwise disjoint sets of (action) labels and T = (Q, i∈[n] L i , δ) is a labelled transition system. We refer to T P as the partitioned labelled transition system derived from T and [L 1 , . . . , L n ]; and to T as the underlying labelled transition system of T P . 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. This leads to tuples of the form (Q, [L 1 , . . . , L n ], S, δ, q in ) with S ⊆ i∈[n] L i . Definition 9 (Partitioned transition system of a I-net). Let n ≥ 2. Let V = {E i : 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], N i = (P i , T i , F i ) be the underlying Petri net of E i . Then PLT S(I(V, ϕ)) = ([µ in , [T 1 , . . . , T n ], ∅, δ, µ in ), the PLTS derived from LT S(V, ϕ) and [T 1 , . . . , T n ], is the initialized partitioned labelled transition system of I(V, ϕ). -Let, for each i ∈ [n], T int,i be the set of internal actions of E i . Let S = {(τ, i) | i ∈ [n]} be a set of n new (silent action) labels, where (τ, i) is associated with E i , for i ∈ [n]. Let V,S : T → (T \ i∈[n] T int,i ) ∪ S be defined as V,S (t) = (τ, i) if t ∈ T int,i for some i ∈ [n] t otherwise

Then V,S (PLT S(I(V, ϕ))) = ([µ in , [ (T 1 ), . . . , (T n )], 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 partition of its labels according to the enterprise nets from V . Moreover, the labels of the internal transitions of each Enterprise net E i ∈ V are made silent using a dedicated symbol (τ, i).

The following notion of branching bisimilarity requires that in each simulation 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, [L 1 , • • • , L n ], S, δ) be a PLTS with silent actions. Let, for all i ∈ [n], S i = L i ∩ S. Then 1. R ⊆ Q × Q is a qualified branching bisimulation for T if -for all (p 0 , q 0 ) ∈ R and a ∈ i∈[n] L i , the following holds: (a) if p 0 a − → p 1 , then a ∈ S and (p 1 , q 0 ) ∈ R or a ∈ L i for some i ∈ [n] and there exists a path q 0 w − → q 1 a − → q 2 in T such that w ∈ S * i , (p 0 , q 1 ) ∈ R and (p 1 , q 2 ) ∈ R; (b) if q 0 a − → q 1 ,

then a ∈ S and (p 0 , q 1 ) ∈ R or a ∈ L i for some i ∈ [n] and there exists a path p 0 w − → p 1 a − → p 2 in T such that w ∈ S * i , (p 1 , q 0 ) ∈ R and (p 2 , q 1 ) ∈ R. 2. Let p, q ∈ Q. Then p and q are qualified branching bisimilar in T , denoted p ≈ qb q, whenever there exists a qualified branching bisimulation R ⊆ Q × Q for T such that (p, q) ∈ R.

Two initialised partitioned labelled transition systems with silent actionsT 1 = (Q 1 , [L 1 , . . . , L n ], S, δ 1 , q 1,in ) and T 2 = (Q 2 , [L 1 , . . . , L n ], S, δ 2 , q 2,in ) such that Q 1 ∩ Q 2 = ∅, are qualified branching bisimilar, denoted T 1 ≈ qb T 2 , if q 1,

in and q 2,in are qualified branching bisimilar in

(Q 1 ∪ Q 2 , [L 1 , . . . , L n ], S, δ 1 ∪ δ 2 ).

Branching bisimilarity does not imply qualified branching bisimilarity. Consider Figure 1.

Let L 1 = {a 1 }, L 2 = {a 2 , τ 2 }, L = L 1 ∪ L 2 and S = {τ 2 }. Let T 1 = ({p 1 , p 2 }, L, S, {(p 1 , a 1 , p 2 )}, p 1

) and T 2 = ({q 1 , q 2 , q 3 }, L, S, {(q 1 , τ 2 , q 2 ), (q 2 , a 1 , q 3 )}, p 1 ) be two initialized LTS s (with silent action τ = τ 2 ). Then the dotted lines in Figure 1 represent a branching bisimulation between T 1 and T 2 . Now let T 1,P = ({p 1 , p 2 }, [L 1 , L 2 ], S, {(p 1 , a 1 , p 2 )}, p 1 ) be the initialized PLTS with silent actions derived from T 1 and [L 1 , L 2 ] and T 2,P = ({q 1 , q 2 , q 3 }, [L 1 , L 2 ], S, {(q 1 , τ 2 , q 2 ), (q 2 , a 1 , q 3 )}, p 1 ) the initialized PLTS p 1 p 2 q 1 q 2 q 3 Fig. 1: ≈ bb does not imply ≈ qb with silent actions derived from T 2 and [L 1 , L 2 ]. Then it is not possible to find a qualified branching bisimulation between T 1,P and T 2,P because a 1 and τ 2 are from different subsets of labels. However there is a strong relationship between branching bisimilarity and qualified branching bisimilarity 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 = {E i : i ∈ [n]} and V = {E i : i ∈ [n]} be composable sets of E-nets. Let ϕ be a matching over V and ϕ a matching over V . Let S = {(τ, i) | i ∈ [n]} be a set of n new action labels, with for all i ∈ [n], (τ, i) associated with E i in V and with E i in V . Then λ V,τ (LT S(V, ϕ)) ≈ bb λ V ,τ (LT S(V , ϕ)) if and only if V,S (PLT S(V, ϕ)) ≈ qb V ,S (PLT S(V , ϕ)).

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 ,S (PLT S(V , ϕ))). From λ V,τ (LT S(V, ϕ)) ≈ bb λ V ,τ (LT S(V , ϕ)) it follows that when a transition labelled a from an Enterprise net E i ∈ V is simulated by a sequence wa in λ V ,τ (LT S(V , ϕ)), then w can be any combination of silent actions from various E-nets in V . 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 E i (labelled by (τ, i)). These form a sequence w and it can be shown that qualified branching bisimilarity is preserved after w a.

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 = {E i : i ∈ [n]} be a composable set of E-nets, ϕ a matching over V , and V = {E i : i ∈ [n]} where for all i ∈ [n], E i is an implementation of E i with respect to V . Then I(V , φ) I(V, φ) if, for all i ∈ [n], E i is locally compliant with I(V, ϕ).

Let us assume that, for alli ∈ [n], E i 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 \ {E i }) ∪ {E i }.

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 ,S (PLT S(V , ϕ)). The theorem then follows from Theorem 2.

Let µ in and µ in be the default initial markings of I(V, ϕ) and I(V , ϕ), respectively. For all i ∈ [n], µ i in denotes the default initial marking of

I(V i , ϕ) and R i ⊆ [µ in × [µ i

in is a qualified branching bisimulation between V,S (PLT S(V, ϕ)) and V i ,S (PLT S(V i , ϕ)).

In addition, we define relations Z i for all i ∈ [n], consisting of all pairs of markings (µ i , µ ) in [µ i in × [µ in such that µ i (p) = µ (p) for all places p shared by I(V i , φ) and I(V , φ). Note that I(V i , φ) and I(V , φ) share all and only the places of E i and the channel places P (V , ϕ).

As a consequence, if (µ i , µ ) ∈ Z i for some i ∈ [n], then every transition t of E i enabled at µ i in I(V i , φ) is also enabled at µ in I(V , φ) and vice versa; moreover, if

µ i t − → µ i 1 in I(V i , φ) and µ t − → µ 1 in I(V , φ

), then also (µ i 1 , µ 1 ) ∈ Z i (property A) 5 . Finally, we define the relation R by R = i∈[n] R i • Z i . We briefly consider the steps followed to establish that R is a qualified branching bisimulation between V,S (PLT S(V, ϕ)) and V ,S (PLT S(V , ϕ)), 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 , µ in ) ∈ R. Assume (µ, µ ) ∈ R. Let, for all i ∈ [n], µ i be such that (µ,

µ i ) ∈ R i and (µ i , µ ) ∈ Z i . Let µ a − → µ 1 in V,S (PLT S(V, ϕ)).

Then there is a unique E j such that a = V,S (t) for some transition t of E j .

Since R j is a qualified branching bisimulation between V,S (PLT S(V, ϕ)) and V j ,S (PLT S(V j , ϕ)), it follows that µ a − → µ 1 can be simulated from µ j in V j ,S (PLT S(V j , ϕ)), as described in Definition 10, by

µ j w − → µ j 1 a − → µ j 2

where wa is a sequence of zero or more transitions from E j such that (µ, µ j 1 ) ∈ R j and (µ 1 , µ j 2 ) ∈ R j . Then, by property A, we can conclude that For all i = j, we can apply a similar reasoning and conclude that a sequence

R j R R i Z j Z iµ i w −→ µ i 1 a − → µ i 2 (with w a a sequence from E j ∈ V i ) in V i ,S (PLT S(V i , ϕ)) such that (µ, µ i 1 ) ∈ R i and (µ 1 , µ i 2 ) ∈ R i .

Since the transitions involved in the simulation are not from E i ∈ V i , it follows that (µ i 1 , µ 1 ) ∈ Z i and (µ i 2 , µ 2 ) ∈ Z i and so (µ

1 , µ 1 ) ∈ R i • Z i and (µ 2 , µ 2 ) ∈ R i • Z i . Consequently µ w − → µ 1 a − → µ 2 in V ,S (PLT S(V , ϕ)) with (µ, µ 1 ) ∈ R and (µ 1 , µ 2 ) ∈ R.

To prove the other direction, assume that (µ, µ ) ∈ R and µ a − → µ 1 in V ,S (PLT S(V , ϕ)). Again, we can identify the unique E-net with the transition t such that V ,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 Z i is respected by each step in the simulation.

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 introduces 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. Composition 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 interface 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 asynchronous 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. Inheritance 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 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 represent 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 communication between enterprise level business processes and the verification of specific workflow properties using Linear Temporal Logic.

Conclusion

We have introduced I-nets as a means to capture global requirements concerning communication while leaving design decisions concerning internal operations to the local level. Compliance is then defined as branching bisimilarity between the labelled transition system of the original (global) reference model and the labelled transition system of its implementation (emerging from the local implementations). The use of qualified branching bisimilarity simplified the proof of our main theorem, Theorem 1, that local compliance 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 section 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 introduce 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 translated into an LTL formula. To verify that the transition system of the local replacement satisfies the LTL-formula, model checking is used. In this approach, 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.