Declarative Choreographies and Liveness

Choreographies are an important tool for the development of highly distributed applications. Using an “Alice-talks-to-Bob” notation, they permit to abstract away details of a distributed implementation and focus on how the different components interact. This has been a fundamental driver for the adoption of choreographies in industry standards such as Message Sequence Charts (MSC) [21], UML Sequence Diagrams [31], WS-CDL, and BPMN Choreography Notation [30]. Moreover, choreography notations have been used in a range of application areas, including web-service development [6, 7], synthesis of protocol behaviour [25], monitoring [3], parallel programming [26] and cyber-physical systems [27]. Paired with static analysis techniques (e.g., behavioural type systems), they are capable of deriving distributed (endpoint) implementations where endpoints generated from a choreography ascribe to all and only the behaviors defined by it. In practice, choreographies have “graduated” from the academic world, and several industrial programming languages implementing choreographies exist, e.g., [7, 19, 22].

A central aspect of choreography languages is the notion of interaction. An interaction is a first class citizen in any choreography language and, as a minimum, it collects information regarding the sender, the receivers, and the action used to synchronize participants. In Fig. 1, we show an exemplary BPMN choreography, based on a variant of the Buyer-Seller protocol [6]. The choreography involves three participants, a Buyer, a Seller and a Shipper. After asking the Seller for a quote and getting the reply, the Buyer may either Accept, Reject or Ask again. If the Buyer accepts, the Seller sends an Order to the Shipper, which subsequently sends the detailed confirmation directly to the Buyer.

BPMN Choreography for Buyer-Seller-Shipper example.

Full size image

The second aspect considered in the design of choreography languages is the ordering of interactions. Typically, choreography languages are seen as imperative programs as the BPMN choreography above, that describe how interactions should occur. Any other flow not explicitly written in the language is considered forbidden. It has been observed that imperative notations are often insufficiently flexible for modelling business processes [1, 33]. An imperative notation focuses on describing a small number of ideal flows through a process. Adding more flows to represent edge cases and less common solutions to the model tends to increase its complexity significantly. While this approach works for processes where the ideal case is all we are interested in, this does not suffice for knowledge and case work: knowledge workers tend to deal with highly variant scenarios for which they need to determine unique solutions. For instance, in the choreography above, we may in practice really want the liveness property, that a Quote is eventually followed by a decision, but that the Sellers can provide new quotes or the Buyer can ask again, any finite number of times, before accepting or rejecting a quote. The present imperative choreography languages do not allow to specify such general liveness property.

In the present paper, we propose using the declarative Dynamic Condition Response (DCR) graph notation [9, 14, 28, 29, 34] as a formal declarative notation for both choreographies and end-point specifications, allowing the specification of both safety and general liveness properties. The DCR graphs notation has been developed for the formalisation and digitalisation of collaborative, adaptive case management processes. The notation is both supported by a range of formal techniques, and serves as the formal base for the industrial (dcrgraphs.net) design and simulation tool. During the recent years, the DCR graphs technology has been employed in major industrial case management systems used in the public sector in Denmark. DCR graphs have been extended to include both data [35], time [18] and sub-processes [9]. In the present paper we consider only the core notation, which is expressive enough to represent both regular and omega-regular languages [9] as well as so-called true concurrency [10]. This means that we provide the first choreography model supporting end-point projection and general liveness properties. Definition and simulation of DCR graphs is supported by the on-line DCR Workbench [12] available at http://dcr.tools/forte19. DCR diagrams in this paper were all produced using the workbench.

One of the important reasons for using choreography languages is their correctness-by-design guarantees. Message-passing distributed systems consist of communicating endpoints whose behaviours are defined in terms of input/output actions. So if the choreography is to be implemented by a message-passing distributed system, it is necessary to translate choreographies into code that can be executed by these endpoints. Such a translation is referred to as an endpoint projection. The endpoint projection, paired with the global properties of the choreography, warrants the safety of the distributed execution of the endpoints (e.g. deadlock-freedom). A catch of this approach is, however, that the choreography language often allows specifications that are not well-formed, meaning that it is not possible to realise the choreography as the composition of end-point processes. A key result for any choice of choreography language and end-point language is therefore to provide criteria for the choreography to be well-formed.

A core property is that of local causality. Intuitively, local causality means that if a participant initiates an interaction, it must not have direct dependencies (or causal relationships) to interactions in which this participant is not involved. The criteria for end-point projectability is, however, highly dependent of the chosen languages. In BPMN 2.0.2 it is formulated as a constraint on sequencing

“The Initiator of a Choreography Activity MUST have been involved (as Initiator or Receiver) in the previous Choreography Activity.”

as well as a number of more complex constraints on the use of so-called branching gateways in BPMN for choices. Proving the correctness of such criteria requires a formal semantics, which is not yet provided for BPMN Choreographies, but for similar notations [5]. In the present paper, we will build upon the formal semantics and theory of safe projections [17, 18] for DCR graphs to provide end-point projections for DCR choreographies.

Summary of Contributions: We provide a general end-point projection result for: (1) a declarative choreography model, (2) that can represent general omega-regular liveness properties [9], (3) supports a broad range of extensions such as dynamic process spanning and refinement [9], true-concurrency semantics [10] and time [18], and (4) is supported by both academic and industrial design and simulation tools.

In this section we first define the general concept of interactions, which are common to previous work on choreographies. We then recall the model of Dynamic Condition Response (DCR) graphs.

2.1 Interactions

Assume a fixed set of actions \(\mathsf {A}\), ranged over by a, b, c and a fixed set of roles \(\mathsf {R}\), ranged over by \(r,r',r_1,r_2,...\) (referred to as participants in [5]).

Definition 1

An interaction is a triple \((a, r \rightarrow R)\), in which the action \(a\in \mathsf {A}\) is initiated by the role r and received by the roles \(R\subset _{\mathsf {fin}} \mathsf {R}\backslash \{r\}\), i.e a finite set of roles distinct from r. Define \(\mathsf {Initiator}((a, r \rightarrow R))=r\). We use the shorthand \((a, r \rightarrow r')\) for interactions between two participants \((a, r \rightarrow \{r'\})\). We denote by \(\mathsf {IA}\) the set of all interactions.

We proceed to define projections of interactions to actions for end-point processes. End-point processes describe the view of the process from a single participant r synchronising with the other participants via messages on channels: For each interaction \((a, r \rightarrow R)\) in the choreography, there will be channels \((a, r \rightarrow r')\) from r to \(r'\) for each \(r'\in R\). To ease the definition of projections and avoid introducing new notation, we describe actions for an end-point also as interactions. That is, for the end-point process at role r, we use the interaction \((a, r \rightarrow R')\) to represent the action \(!(a, r \rightarrow R')\) for sending a message on the channels \((a, r \rightarrow r')\) for all participants \(r'\in R'\). The interaction \((a, r' \rightarrow r)\), represents the action \(?(a, r' \rightarrow r)\) for receiving a message on the channel \((a, r' \rightarrow r)\). We apologize to the reader for the inconvenience this reuse of notation may cause.

Definition 2

For an interaction \(\alpha =(a, r' \rightarrow R')\), define the end-point projection of \(\alpha \) at r by:

We extend end-point projections to sets and sequences of interactions by pointwise projection and removing \(\tau \) actions, and finally to sets of sequences of interactions in the obvious way.

Definition 3

A choreographic language is a triple (C, A, R) where \(A\subseteq \mathsf {A}\), \(R\subseteq _{fin}\mathsf {R}\), and \(C\subseteq \mathsf {IA}^{\infty }=\mathsf {IA}^*\cup \mathsf {IA}^{\omega }\). That is, a set C of finite and infinite sequences of interactions for a given set of actions A and roles R.

When A and R are obvious from the context, we shall take C as defining a choreographic language.

Definition 4

The end-point projection of a choreographic language (C, A, R) is the family of languages \((C_{|r} )_{r\in R}\).

2.2 DCR Graphs

In this section we recall Dynamic Condition Response (DCR) graphs [10, 12,13,14, 28]. This paper follows the set-based formulation of [10, 14, 28].

As formally defined below, a DCR graph consists of a directed graph and a marking. The nodes of the graph are labelled events and the edges are relations of five kinds: conditions (\(\mathrel {\rightarrow \!\!\bullet }\)), responses (\(\mathrel {\bullet \!\!\rightarrow }\)), inclusions (\(\mathrel {\rightarrow \!\!+}\)), exclusions (\(\mathrel {\rightarrow \!\!\%}\)) and milestones (\(\mathrel {\rightarrow \!\!\diamond }\)).

Definition 5

A DCR graph is a tuple \((E,M,L, \ell , \mathrel {\rightarrow \!\!\bullet },\mathrel {\bullet \!\!\rightarrow },\mathrel {\rightarrow \!\!\diamond },\mathrel {\rightarrow \!\!+},\mathrel {\rightarrow \!\!\%})\), where

• E is a set of events

• \(M\subseteq E \times E \times E\) is a marking

• L is a set of labels

• \(\ell :E \rightarrow L\) is a labelling function

• \(\phi \subseteq E\times E\) for \(\phi \in \{\mathrel {\rightarrow \!\!\bullet },\mathrel {\bullet \!\!\rightarrow },\mathrel {\rightarrow \!\!\diamond },\mathrel {\rightarrow \!\!+},\mathrel {\rightarrow \!\!\%}\}\) are relations between events.

A DCR graph defines a process whose executions are finite and infinite sequences of (labelled) events. Note that an event may be executed several times. The three sets of events in the marking \(M=(\mathsf {Ex},\mathsf {Re},\mathsf {In})\) defines the state of the DCR graph process, and are referred to as the executed events (\(\mathsf {Ex}\)), the pending response^{Footnote 1} events (\(\mathsf {Re}\)) and the included events (\(\mathsf {In}\)). The relations define effects of the execution of events and constrain the executions of the process defined by the DCR graph as defined formally below. Briefly:

• An inclusion (respectively exclusion) relation \(e\mathrel {\rightarrow \!\!+}e'\) (respectively \(e\mathrel {\rightarrow \!\!\%}e'\)) means that if e is executed, then \(e'\) is included (respectively excluded).

• A condition relation \(e\mathrel {\rightarrow \!\!\bullet }e'\) means that e is a condition for \(e'\), i.e. if e is included, then e must have been executed for \(e'\) to be enabled for execution.

• A response relation \(e\mathrel {\bullet \!\!\rightarrow }e'\) means that whenever e is executed, \(e'\) becomes a pending response. During a process execution, a pending event must eventually be executed (which makes it no longer pending, unless it has a response relation to itself) or be excluded. We refer to \(e'\) as a response to e.

• A milestone relation \(e\mathrel {\rightarrow \!\!\diamond }e'\) means that if e is included it must not be pending for \(e'\) to be enabled for execution. We refer to e as a milestone for \(e'\). Milestones are typically used in cyclic behaviour, when some earlier executed event e may be required to be executed again, i.e. it becomes pending, before the process can proceed executing event \(e'\).

For DCR graph G with events E and marking \(M=(\mathsf {Ex},\mathsf {Re},\mathsf {In})\) and event \(e\in E\) we write \(\mathord {(\mathrel {\rightarrow \!\!\bullet }\!e)}\) for the set \(\{e'\in E\mid e'\mathrel {\rightarrow \!\!\bullet }e\}\), write \(\mathord {(e\!\mathrel {\bullet \!\!\rightarrow })}\) for the set \(\{e'\in E\mid e \mathrel {\bullet \!\!\rightarrow }e'\}\) and similarly for \(\mathord {(e\!\mathrel {\rightarrow \!\!+})}\), \(\mathord {(e\!\mathrel {\rightarrow \!\!\%})}\) and \(\mathord {(\mathrel {\rightarrow \!\!\diamond }\!e)}\). We can now define when the events of a DCR graph are enabled.

Definition 6

(Enabled events). Let \(G=(E,M,L, \ell , \mathrel {\rightarrow \!\!\bullet },\mathrel {\bullet \!\!\rightarrow },\mathrel {\rightarrow \!\!\diamond },\mathrel {\rightarrow \!\!+},\mathrel {\rightarrow \!\!\%})\) be a DCR graph, with marking \(M = (\mathsf {Ex},\mathsf {Re},\mathsf {In})\). An event \(e \in \mathsf {E}\) is enabled, written \(e\in {\mathsf {enabled}(G)}\), iff (a) \(e \in \mathsf {In}{}\) and (b) \(\mathsf {In}{}\cap \mathord {(\mathrel {\rightarrow \!\!\bullet }\!e)} \subseteq \mathsf {Ex}\) and (c) \((\mathsf {Re}{}\cap \mathsf {In})\cap \mathord {(\mathrel {\rightarrow \!\!\diamond }\!e)} = \emptyset \).

That is, enabled events (a) are included, (b) their included conditions have already been executed, and (c) have no pending included milestones.

Example DCR choreography

Full size image

Example 7

We give an example of a DCR graph in Fig. 2 as visualised by the online-tool dcr.tools/forte19. Events are indicated by boxes with solid borders and collections of events are shown with dashed boxes. Relations are shown as arrows between the boxes. As formalised in [16], such collections are referred to as “nestings” and are just a visual shorthand, understanding arrows to (from) nestings to represent arrows to (from) every event inside the nesting.

Traditionally, the labels of DCR graphs only consist of an action and possibly a set of roles that may perform the action. In the present paper, however, the labels of the DCR graphs are interactions rather than just actions. Instead of labelling the boxes representing the events simply with the label, e.g., \((\mathsf {Ask}, \mathsf {Buyer} \rightarrow \{\mathsf {Seller1},\mathsf {Seller1}\})\), we have split the label in three fields in the visualisation similarly to the notation for BPMN choreographies: The initiator (Buyer) is written in the field at the top of the box; the action (\(\mathsf {Ask}\)) is written in the middle field, and the receiver(s) (\(\mathsf {Seller1},\mathsf {Seller2}\)) in the bottom field with a grey background. When no confusion is possible, we refer to events by the action shown in middle field, speaking of, e.g., “the event Ask” rather than the more precise “the event labelled Buyer, Ask, Seller1, Seller2.”

The marking of the graph and whether events are enabled or not is indicated visually: If the background of all fields is grey for a box, the event is included, but not enabled. For instance, the Ask event is enabled, but the two Quote events are not enabled (because the Ask event is a condition for the events and not yet executed). A box which is made opaque/dimmed out, such as the two Order events and the Details event, represents an event which is not included. When explaining Fig. 3 we describe the visualisation of executed and pending events.

The response relation \((\mathrel {\bullet \!\!\rightarrow })\) from the event Ask to the nesting box around the Quote events means that the Quote events become pending when Ask is executed. This expresses the liveness constraint, that if the buyer asks, a quote must eventually be given by both sellers. The milestone relation \((\mathrel {\rightarrow \!\!\diamond })\) from the box around the Quote events to the nesting box labelled Decide means that the events (Accept1, Accept2 and Reject) inside the Decide box cannot be executed if any of the Quote events are pending, not even if Quote happened in the past. This expresses the safety condition, that the buyer can not accept or reject if one of the sellers has not responded after the last time the buyer asked for a quote. The inclusion relation from e.g. Accept1 to Order for Seller 1 means that order event will be included if the buyer accepts the quote from Seller 1. The circular exclusion arrow in the Decide box means that any event inside the box is related by an exclude relation to any event inside the box, i.e. they are mutually and self-exclusive. That is, whenever one of the events inside the box happens, all three events inside the box are excluded. Moreover, due to the exclude relation from the Decide box to the Negotiate box, also the Ask and Quote events are excluded when a decision is made.

Below we formalise how the marking changes when an enabled event e is executed: (a) the event e is added to the set of executed events, (b) e is removed from the set of pending response events, and the responses to e are added to the set of pending response events, (c) the events excluded by e are removed from the set of included events, and the events included by e are added to the set of included events.

Definition 8

(Execution). Let \(G=(E,M,L, \ell , \mathrel {\rightarrow \!\!\bullet },\mathrel {\bullet \!\!\rightarrow },\mathrel {\rightarrow \!\!\diamond },\mathrel {\rightarrow \!\!+},\mathrel {\rightarrow \!\!\%})\) be a DCR graph, with marking \(M = (\mathsf {Ex},\mathsf {Re},\mathsf {In})\). When \(e\in {\mathsf {enabled}(G)}\), the result of executing e, written \(\mathsf {execute}(G, e)\) is a new DCR graph \(G'\) with the same events, labels, labelling function and relations, but a new marking \(M'= (\mathsf {Ex}',\mathsf {Re}',\mathsf {In}')\), where (a) \(\mathsf {Ex}' = \mathsf {Ex}\,\cup \, \{e\}\) (b) \(\mathsf {Re}' = (\mathsf {Re}\backslash \{e\})\, \cup \, \mathord {(e\!\mathrel {\bullet \!\!\rightarrow })}\), and (c) \(\mathsf {In}' = (\mathsf {In}\backslash \mathord {(e\!\mathrel {\rightarrow \!\!\%})})\, \cup \, \mathord {(e\!\mathrel {\rightarrow \!\!+})}\)

Example 9

In the graph in Fig. 2, we may execute the event Ask. Following the relations in the graph, this will make the two Quote events enabled and pending: they were previously not enabled due to their condition relation from Ask and once Ask becomes “executed” in the marking, that condition is fulfilled, and Quote becomes enabled. Altogether, executing Ask yields the graph shown in Fig. 3. Red text and an exclamation mark after the action in the middle field represents an event which is pending, as is the case for the two Quote events. A box with a check mark after the label represents an event which is executed, as can be seen for the event Ask. Note that Ask may be executed again immediately, leaving the process in the same state, but the two Quote events must eventually be executed (without any intermediate Ask) in order for the run to be accepting.

DCR choreography after execution of Ask. (Color figure online)

Full size image

From the definition of execution we can define a transition semantics for DCR graphs using labelled event transition system with responses.

Definition 10

(Transition semantics). Let \(G=(E,M,L, \ell , \mathrel {\rightarrow \!\!\bullet },\mathrel {\bullet \!\!\rightarrow },\mathrel {\rightarrow \!\!\diamond },\mathrel {\rightarrow \!\!+},\mathrel {\rightarrow \!\!\%})\) be a DCR graph. The Labelled Event Transition System with Responses (LETSR) for G is defined as \({\mathcal {T}}({G}) = ( \mathcal {G}, G, E, L, \ell , \rightarrow , \rho )\), where the DCR graph G is the initial state, E is the set of events, L is the set of labels, \(\ell \) is the labelling function, \(\rightarrow \subseteq \mathcal {G}\times E\times \mathcal {G}\) is the transition relation, defined by \((G,e,G')\in \rightarrow \) iff \(e\in {\mathsf {enabled}(G)}\) and \(G'=\mathsf {execute}(G, e)\), and \(\mathcal {G}=\{G'\mid G\rightarrow ^* G' \}\), the set of states, is the graphs reachable from the initial graph G by execution of events, and finally \(\rho \) is the response function defined on DCR graphs by \(\rho (G')=\mathsf {Re}\cap \mathsf {In}\), if \((\mathsf {Ex},\mathsf {Re},\mathsf {In})\) is the marking of \(G'\).

We say that two LETSR T and \(T'\) are isomorphic, written \(T\equiv T'\), if there is an isomorphism between the sets of states preserving and respecting transitions and the response function.^{Footnote 2}

We define the language of a DCR graph as all finite and infinite sequences of such executions, where we demand that all pending responses are either eventually executed or excluded.

Definition 11

(Language of a DCR graph). Let \(G=(E,M,L, \ell , \mathrel {\rightarrow \!\!\bullet },\mathrel {\bullet \!\!\rightarrow },\mathrel {\rightarrow \!\!\diamond },\mathrel {\rightarrow \!\!+},\mathrel {\rightarrow \!\!\%})\) be a DCR graph. A run of G is a finite or infinite sequence of events \(e_0, e_1,\ldots \) such that \(e_i\in {\mathsf {enabled}(G_i)}\), \(\mathsf {execute}(G_i, e_i) = G_{i+1}\), and \(G_0 = G\). We call a run accepting iff for each \(G_i\) with marking \(M_i = (\mathsf {Ex}_i, \mathsf {Re}_i, \mathsf {In}_i)\) and \(e \in \mathsf {Re}_i \cap \mathsf {In}_i\) there exists a \(j \ge i\) such that \(e_j=e\) or \(e \not \in \mathsf {Re}_j \cap \mathsf {In}_j\).

The language \(\mathop {\mathsf {lang}}({G})\subseteq L^{\infty }\) of G is the set of finite and infinite sequences of labels \(l_0l_1\cdots \) such that there is an accepting run \(e_0, e_1,\ldots \) where \({\ell }({e_i})=l_i\).

It has been proven in [9] that DCR graphs can express exactly the languages that are the union of a regular and an \(\omega \)-regular language. This means that one can express regular safety and liveness properties in DCR graphs.

Since the definition of accepting runs only depends on the included pending responses in the markings of the graphs and the events being executed during a run, it is easy to see that if two DCR graphs have isomorphic transition systems with responses then they also have the same languages.

Proposition 12

Let G and \(G'\) be DCR graphs. If \({\mathcal {T}}({G})\equiv {\mathcal {T}}({G'})\) then \(\mathop {\mathsf {lang}}({G})=\mathop {\mathsf {lang}}({G'})\).

Below we first account for how DCR Choreographies and DCR End-points can be defined using DCR graphs. We then derive the criteria for end-point projectability and provide the operational correspondence between an end-point projectable DCR graph and the synchronous composition of its end-points.

Definition 13

Let \(A\subseteq \mathsf {A}\) and \(R\subset _{fin}\mathsf {R}\) be sets of roles and actions, respectively. A triple (G, A, R) is then a DCR choreography when G is a deadlock-free DCR graph such that the labels \(L\subseteq \mathsf {IA}\) of G are interactions with actions in A and participants in R. For a role \(r\in R\), a tuple (G, A, R, r) is a DCR End-point when the labels L of G are interactions either of the form \((a, r \rightarrow R')\) or \((a, r' \rightarrow r)\) with \(a\in A\).

Example 14

The DCR graph in Fig. 2 is the DCR graph G of a DCR choreography (G, A, R) where the actions A and roles R are given by:

Note that by virtue of being a general declarative notation, one may specify DCR graphs with deadlocks, e.g. by having a cycle of condition relations. It is easy to prove, that if (\(\mathrel {\rightarrow \!\!\bullet }\cup \mathrel {\rightarrow \!\!\diamond }\)), i.e. the union of the condition and milestone relations, is acyclic, then the DCR graph is free of deadlocks. Moreover, such graphs can express all languages expressed by general DCR graphs, and in particular the complex behaviour in our running example.

We now turn to the key question for any choreography language: How do we project a global choreography description onto the intended behaviour of individual participants? And in particular, is this operation always possible, or are some global descriptions in fact not realisable by individual end-points?

Projections and distributed execution have been studied for DCR graphs in previous work [15, 17, 18], but in a rather different setting where events are only labeled by actions and initiating roles, not receiving roles. For this reason, it is safe in [15, 17, 18] to leave out an event in the projection to an end-point, if the execution of this event does not impact the state or enabledness of any event initiated by the participant responsible for that end-point. An example of such an event in our running example is the Details event for the Buyer end-point.

In the present paper we have explicit receivers and need to preserve all receiving events for a participant. Consequently, we can not directly use the notion of projection given in [15, 17, 18]. However, we may yet build on these projections to obtain one useful for DCR choreographies. The core idea in those papers was to project a graph G with events E to a network of local graphs for any division (not necessarily disjoint) of the events \(\delta _1 \cup \delta _2 \cup \ldots \cup \delta _n=E\), then define synchronous composition of such networks of DCR graphs. Intuitively, shared events, i.e. events occurring in more than one graph, are executed synchronously in the network, representing communication. The projection then ensured that execution of the network formed by the local graphs would have a transition system isomorphic to that of the global graph, and thus in particular exhibit the same language as the global graph.

In the following we reconcile the notion of projection from [15, 17, 18] and then subsequently define end-point projections.

First, we characterise when the execution of an event may change the marking or enabledness of another. To this end, we define the notion of direct dependency.

Definition 15

Let \(G=(E,M,L, \ell , \mathrel {\rightarrow \!\!\bullet },\mathrel {\bullet \!\!\rightarrow },\mathrel {\rightarrow \!\!\diamond },\mathrel {\rightarrow \!\!+},\mathrel {\rightarrow \!\!\%})\) be a DCR graph and let \(e,e'\in E\) be events of E. Then there is a direct dependency \(e'\preceq e\) from \(e'\) to e iff either of the following conditions are true

1. 1.

   \(e'=e,\)

2. 2.

   \(e' (\mathrel {\rightarrow \!\!\bullet }\cup \mathrel {\bullet \!\!\rightarrow }\cup \mathrel {\rightarrow \!\!+}\cup \mathrel {\rightarrow \!\!\%}\cup \mathrel {\rightarrow \!\!\diamond }) e\),

3. 3.

   \(\exists e''. \; e' (\mathrel {\rightarrow \!\!+}\cup \mathrel {\rightarrow \!\!\%}) e'' (\mathrel {\rightarrow \!\!\bullet }\cup \mathrel {\rightarrow \!\!\diamond }) e\),

4. 4.

   \(\exists e''. \; e' \mathrel {\bullet \!\!\rightarrow }e'' \mathrel {\rightarrow \!\!\diamond }e\).

That is, \(e'\preceq e\) iff either (1) they are the same, (2) there is a relation from \(e'\) to e, (3) \(e'\) includes or excludes an event which is itself a condition or milestone for e, or (4) \(e'\) has a response to a milestone for e.

The following proposition states that an event e must be directly dependent on any event \(e'\) whose execution may change the marking or enabledness of e.

Proposition 16

Let G be a DCR graph with marking \(M = (\mathsf {Ex},\mathsf {Re},\mathsf {In})\). Suppose \(e'\in {\mathsf {enabled}(G)}\), and let \(G' = \mathsf {execute}(G, e')\) and \(M'= (\mathsf {Ex}',\mathsf {Re}',\mathsf {In}')\) be the marking of \(G'\). If either of the following hold, then \(e'\preceq e\).

1. 1.

   , 

2. 2.

   , 

3. 3.

   ,

4. 4.

   .

Proof

(Sketch) For lack of space we just show why condition 2 above implies \(e'\preceq e\), the other conditions follow from a similar inspection of the definitions. First note that the set \(\mathsf {Ex}\) of executed events always grows, i.e. once executed an event can never become not executed. So we only need to consider the case \(e\not \in \mathsf {Ex}\) and \(e\in \mathsf {Ex}'\). From the Definition 8 it is clear that the only event that can be included in the set \(\mathsf {Ex}\) during execution is the event being executed, so it follows that \(e=e'\) and thus \(e'\preceq e\).

We note that this implication is not a bi-implication, e.g., in the DCR graph comprising just the two events e, f and the single relation \(e\mathrel {\rightarrow \!\!\bullet }f\) in a marking where e is already executed, we clearly have \(e\preceq f\) (by Definition 15(2) because there is a relation from e to f), yet executing e in fact cause no changes to marking or enabledness of f.

Intuitively, we will obtain the end-point projection for a participant r by keeping (a) events labelled with interactions involving r, as well as (b) the direct dependencies of the events for which r is the initiator. We then interpret the interactions as end-point actions as described in Sect. 2.1. In order for the interactions to make sense as actions for the end-point process at r, the role r must be involved in its direct dependencies. We formalise this as follows.

Definition 17

Let (G, A, R) be a DCR choreography and \(\ell \) the labelling function of G; and let \(r\in R\) be a role. This choreography is end-point projectable for r iff for all e, if \(\mathsf {Initiator}(e)=r\) and \(e' \preceq e\), then \({\ell }({e'})_{\mid r}\not =\tau \),

Example 18

Referring again to the example DCR choreography in Fig. 2, we find that this choreography is in fact not end-point projectable for the participants \(\mathsf {Seller1}\) and \(\mathsf {Seller2}\). We see in Fig. 2 that the Accept1 event causes Accept2 to be excluded, however, Seller2 is initiator of Accept2, but not participating in Accept1. To be precise, because of the exclusion we have \(\mathsf {Accept1}\preceq \mathsf {Accept2}\) and \({\ell }({\mathsf {Accept2}})=(\textsf {Accept2}, \textsf {Buyer} \rightarrow \textsf {Seller2})\) yet \({\ell }({\mathsf {Accept1}})=(\textsf {Accept1}, \textsf {Buyer} \rightarrow \textsf {Seller1})\), so \({\ell }({\mathsf {Accept1}})_{\mid \mathsf {Shipper}} =\tau \).

We fix this by redefining the choreography such that Seller2 is included in the Accept1 interaction, that is, so that Seller2 is notified that he lost the contract; and vice versa including Seller1 in the Accept2 interaction. We show the projectable process in Fig. 4. This choreography is end-point projectable.

We proceed by defining the end-point projection. We start by recalling the definition of projection in [15, 17, 18], adapted to keep all labels.

End-point projectable DCR choreography

Full size image

Definition 19

(Adapted DCR \(\delta \)-Projection cf. [15, 17]). Given a DCR graph

and a set of events \(\delta \subseteq E\), define the projection of G to the events \(\delta \) as the graph \({G}\mathord |_{\delta } = ({E}\mathord |_{\delta },{M}\mathord |_{\delta },{L}\mathord |_{\delta }, {\ell }\mathord |_{\delta }, {\mathrel {\rightarrow \!\!\bullet }}\mathord |_{\delta }, {\mathrel {\bullet \!\!\rightarrow }}\mathord |_{\delta }, {\mathrel {\rightarrow \!\!\diamond }}\mathord |_{\delta }, {\mathrel {\rightarrow \!\!+}}\mathord |_{\delta }, {\mathrel {\rightarrow \!\!\%}}\mathord |_{\delta })\) given by:

1. 1.

   \( {E}\mathord |_{\delta } = \{e\in E\mid \exists e'\in \delta . \; e \preceq e'\}\),

2. 2.

   \( {M}\mathord |_{\delta } = ({\mathsf {Ex}}\mathord |_{\delta }, {\mathsf {Re}}\mathord |_{\delta }, {\mathsf {In}}\mathord |_{\delta })\) where:

   1. (a)

      \({\mathsf {Ex}}\mathord |_{\delta } = \mathsf {Ex}\cap {E}\mathord |_{\delta }\)

   2. (b)

      \({\mathsf {Re}}\mathord |_{\delta } = \mathsf {Re}\cap {E}\mathord |_{\delta }\)

   3. (c)

      \({\mathsf {In}}\mathord |_{\delta } = \bigl (\mathsf {In}\cap ( {(\mathop {\mathrel {\rightarrow \!\!\bullet }}\delta )} \cup \, {(\mathop {\mathrel {\rightarrow \!\!\diamond }}\delta )} \cup \, \delta )\bigr ) \cup \bigl ({E}\mathord |_{\delta } \setminus ( (\mathord {\mathrel {\rightarrow \!\!\bullet }}\delta ) \cup (\mathord {\mathrel {\rightarrow \!\!\diamond }}\delta ) \cup \delta )\bigr )\).

3. 3.

   \( {\ell }\mathord |_{\delta }(e) = \ell (e), \)

4. 4.

   \({L}\mathord |_{\delta } = \mathsf {img}(\ell )\)

5. 5.

   \( {\mathrel {\rightarrow \!\!\bullet }}\mathord |_{\delta } = \,\mathrel {\rightarrow \!\!\bullet }\cap \, \bigl ((\mathrel {\rightarrow \!\!\bullet }\delta ) \times \delta \bigr )\)

6. 6.

   \( {\mathrel {\rightarrow \!\!\diamond }}\mathord |_{\delta } = \,\mathrel {\rightarrow \!\!\diamond }\cap \,\bigl ((\mathrel {\rightarrow \!\!\diamond }\delta ) \times \delta \bigr )\)

7. 7.

   \( {\mathrel {\bullet \!\!\rightarrow }}\mathord |_{\delta } = \,\mathrel {\bullet \!\!\rightarrow }\cap \, \bigl (((\mathrel {\bullet \!\!\rightarrow }\mathrel {\rightarrow \!\!\diamond }\delta ) \times (\mathrel {\rightarrow \!\!\diamond }\delta )) \cup ((\mathrel {\bullet \!\!\rightarrow }\delta ) \times \delta )\bigr )\)

8. 8.

   \({\mathrel {\rightarrow \!\!+}}\mathord |_{\delta } = \,\mathrel {\rightarrow \!\!+}\cap (((\mathrel {\rightarrow \!\!+}\mathrel {\rightarrow \!\!\bullet }\delta ) \times (\mathrel {\rightarrow \!\!\bullet }\delta )) \cup ((\mathrel {\rightarrow \!\!+}\mathrel {\rightarrow \!\!\diamond }\delta ) \times (\mathrel {\rightarrow \!\!\diamond }\delta )) \cup ((\mathrel {\rightarrow \!\!+}\delta ) \times \delta ))\)

9. 9.

   \( {\mathrel {\rightarrow \!\!\%}}\mathord |_{\delta } = \,\mathrel {\rightarrow \!\!\%}\cap \, (((\mathrel {\rightarrow \!\!\%}\mathrel {\rightarrow \!\!\bullet }\delta ) \times (\mathrel {\rightarrow \!\!\bullet }\delta )) \cup ((\mathrel {\rightarrow \!\!\%}\mathrel {\rightarrow \!\!\diamond }\delta ) \times (\mathrel {\rightarrow \!\!\diamond }\delta )) \cup ((\mathrel {\rightarrow \!\!\%}\delta ) \times \delta ))\).

The complexity in these rules arises mostly from the necessity of including events that may affect milestones or conditions for the events in \(\delta \). We see this particularly in the right-most half of 2(c), in the second clause in 7–9, and in the fourth clause in 8–9.

We now define the end-point projection for a DCR choreography with respect to a role r. The projection comes in two steps: first we compute the \(\delta \)-projection, taking \(\delta \) to be the set of events for which r is the initiator. Second, we simply add all events where r is a receiver. The latter step does not really change the behaviour in terms of sequences of actions, but it ensures that all receiving roles will be present for an interaction, even when it has no effect on other events in the end-point. As also described in the beginning of the section, this was not essential for the previous work, since receivers were not explicit.

Definition 20

(DCR end-point projection). Let (G, A, R) be a DCR choreography with events E and labelling function \(\ell \). For any \(r\in R\), define

and let \(G_{\mid \delta }=(E_{\mid \delta },M,L, \ell _{\mid \delta }, \mathrel {\rightarrow \!\!\bullet },\mathrel {\bullet \!\!\rightarrow },\mathrel {\rightarrow \!\!\diamond },\mathrel {\rightarrow \!\!+},\mathrel {\rightarrow \!\!\%})\) be the \(\delta \)-projection of G for r. Suppose \(M=(\mathsf {Ex},\mathsf {Re},\mathsf {In})\) and define

The end-point projection of (G, A, R) for r is then defined as the DCR end-point \((G_{\mid r},A_{\mid r},R,r)\) where

Example 21

The result of end-point projecting the corrected choreography in Fig. 4 can be seen in Figs. 5, 6 and 7.

Lemma 22

Let (G, A, R) be a DCR choreography, let \(r\in R\) be a role of R, and let \((G_{\mid r},A_{\mid r},R,r)\) be the projection of that choreography to r. If (G, A, R) is projectable for r, then every label in \(G_{\mid r}\) is an interaction which has r as a participant.

Proof

The set of events of \(G_{\mid r}\) consists of the events \(E_{\mid \delta }\) of the \(\delta \)-projection for \(\delta =\{e\in E_0\mid \mathsf {Initiator}(e)=r\}\) and the events \(E' =\{e\in E\mid \exists a \, r' . \;{\ell }({e})_{\mid r}=(a,r',r)\}\). Clearly, the events in \(E'\) by definition all have the role r among the receivers and thus as participant. According to Definition 19, we have \({E}\mathord |_{\delta } = \{e\in E\mid \exists e'\in \delta . \; e \preceq e'\}\). Now, since \(\mathsf {Initiator}(e')=r\) for all \(e'\in \delta \) it follows from the definition of end-point projectability in Definition 17 that \({\ell }({e})_{\mid r}\not =\tau \) when \(e \preceq e'\) and thus r is also a participant in the interaction for all \(e\in {E}\mathord |_{\delta }\).

As shown below, it follows easily, that if an event is shared between two end-points, it has the same initiator.

Lemma 23

Let \(C=(G,A,R)\) be an end-point projectable DCR choreography, \(r,r'\in R\) be roles of R, and \((G_{\mid r},A_{\mid r},R,r)\) and \((G_{\mid r'},A_{\mid r'},R,r')\) be the projections of C to r and \(r'\). If \(e\in E\cap E'\), where E and \(E'\) are the events of \(G_{\mid r}\) and \(G_{\mid r'}\) respectively, then \(\mathsf {Initiator}(\ell (e))=\mathsf {Initiator}(\ell (e'))\).

End-point projection of Fig. 4 for Buyer.

Full size image

End-point projection of Fig. 4 for Seller1.

Full size image

End-point projection of Fig. 4 for Shipper.

Full size image

Proof

According to Definition 20, the label of an event e in an end-point projection for role r is given by the restriction \({\ell }({e})_{\mid r}\). According to Definition 2 the initiator role is preserved by the restriction or the label is \(\tau \). However, by Definition 17 the label cannot be \(\tau \). Thus, being end-point projections of the same end-point projectable choreography C the event in the two end-point projections will have the same initiator role.

We now define the synchronous composition of a finite set of DCR end-points, for which the labels of shared events agree on the Initiator role. Intuitively, an event e is enabled in the synchronous composition, if it is enabled in all of the end-points in which it occurs. The execution of an event is then defined simply by executing the event in all of the components it occurs. Finally, the label is the interaction obtained by taking the union of receivers.

Definition 24

(Synchronous composition of DCR end-points). For \(R=\{r_1,r_2,\ldots ,r_n\}\) and DCR end-points \(P_i=(G_i,A_i,R,r_i)\) for \(i\in \{1,..,n\}\) we write the synchronous parallel composition as \(P=\varPi _{i\in \{1,..,n\}} P_i\). Define

• \(E=\bigcup _i\in \{1,..,n\} E_i\), where \(E_i\) is the events of \(G_i\).

• \(e\in {\mathsf {enabled}(P)}\) iff \(e\in E_i\) implies \(e\in {\mathsf {enabled}(G_i)}\) for all \(i\in \{1,..,n\}\).

• \(\mathsf {execute}(P, e)=\varPi _{i\in \{1,..,n\}} P'_i\), if \(e\in {\mathsf {enabled}(P)}\) and \(P_i=(G'_i,A_i,R,r_i)\) and \(G'_i=\mathsf {execute}(G_i, e)\), if \(e\in E_i\) and \(P'_i=P_i\) otherwise.

• \(\ell _P(e)=(a, r \rightarrow R')\) if \(e\in E_i\) implies \(\ell _i(e)=(a, r \rightarrow R'_i)\) and \(R'=\bigcup _i\in I\), where \(I=\{i\in \{1,\ldots ,n\}\mid e\in E_i\}\).

• \(\rho _P(P')=\bigcup _{i\in \{1,\ldots ,n\}} \mathsf {Re}_i\cap \mathsf {In}_i\) if \(P'=\varPi _{i\in \{1,..,n\}} P'_i\), \(P'_i=(G'_i,A_i,R,r_i)\) and the marking of \(G'_i\) is \((\mathsf {Ex}_i,\mathsf {Re}_i,\mathsf {In}_i)\).

We now define the LETSR for P by \({\mathcal {T}}({P})=(\mathcal{{P}},P, E, L, \ell _P, \rightarrow _P, \rho _P )\), where \((P',e,P'')\in \rightarrow _P\) if \(e\in {\mathsf {enabled}(P')}\) and \(P''=\mathsf {execute}(P', e)\), and \(\mathcal{{P}}=\{P'\mid P\rightarrow ^* P'\}\).

The following theorem establishes the key property, that the synchronous composition of the end-points yields a transition system with responses isomorphic to the transition system for the choreography, and thus is in particular deadlock free.

Theorem 25

Let \(C=(G,A,R)\) be an end-point projectable DCR choreography, \(R=\{r_1,\ldots ,r_n\}\) and \(P_i=(G_i,A_i,R,r_i)\) for \(i\in \{1,\ldots ,n\}\) the DCR end-points resulting from end-point projection of C. Then \({\mathcal {T}}({C})\equiv {\mathcal {T}}({\varPi _{i\in \{1,..,n\}} P_i})\) and thus \(\varPi _{i\in \{1,..,n\}} P_i\) is deadlock free.

Proof

(Sketch) The proof follows the same approach as the proof of Theorem 5.1 in [18] where a bisimulation is constructed between the original graph (in this case the choreography) and the network of synchronous parallel composition of projections. The reason why the same approach can be used is that the main difference between the present work and the work in [18] is that we have included also receiving events in the end-points that have no effect on the synchronous product, such as the Details event in Fig. 5.

We note that the isomorphism by Proposition 12 implies that the language of the choreography is the same as the language of the composition of the end-points.

Based on the formal process notation of DCR graphs, we have provided the first declarative model for choreographies able to describe general liveness properties. We identified the local causality criteria for end-point projectability and defined end-point projections, using previous work on distributions of DCR graphs. We showed that the synchronous product of the end-point projections had the same behaviour as the original choreography. As future work we intend to extend the results to declarative timed choreographies, benefiting from projections already being defined for timed DCR graphs in [18].

Related Work. Properties for guaranteeing projectability are proposed in various settings and depend on the chosen choreography language. The results in [6] require three main properties: connectedness, well-threadedness, and coherence. While well-threadedness and coherence concern the behaviour of replicated servers, connectedness is the same as the projectability criterium of BPMN 2.0.2, which we also adopt in the present paper. The connectedness property occurs also in other works on choreography, e.g., [8, 23]. In the theory of multiparty session types [20] and in Chor [7], such property is omitted at a price of a more flexible interpretation of sequencing.

To the authors’ knowledge, this is the first work considering general liveness properties at the choreography-level. Other works in the literature have studied liveness for multiparty interactions from session types and contract development: Padovani et al. [32] propose a type system for session types to control liveness properties. However, the model considered is roleless since types describe interactions but without specifying which roles implement them. The work in [11] extends binary session types to specify response properties, that is applied to a variant of a collaborative BPMN process language to verify whether liveness for dead-lock free processes can be achieved. A recent paper by Lange et al. [24] investigates a bounded liveness property for GO programs, where protocols are specified as global types. Such property resembles a progress property and is not as general as our liveness. For instance, requiring that after a Quote we have eventually an Accept or a Reject cannot be expressed as bounded liveness. Honesty is a variant of liveness used in contract-oriented programming [2]. In short, an endpoint is honest if it abides the sequence of actions stipulated in its contract. Honesty will fail if the contract promises the execution of an action and the endpoint does not execute it. Contracts in this sense correspond to DCR responses. We differ from [2] in the sense that we do not require a session-type to verify liveness. It is specified in the model as a behavioural constraint only in the places that is required.

Our previous work in [4], presented a proof system for choreographies where properties such as liveness and connectedness can be expressed in terms of modal (may/must) operators. Apart from the difference on the languages explored (the global calculus in [4] and DCR in the present work), we differ from being able to express one-to-many communications. For DCR graphs, projections were studied in a different context in [15, 17, 18], where all participants were implicit receivers of actions and projections thus always defined.