Keywords

1 Introduction

If we consider the very core definition of what a business or work process is, we see that collaboration is an essential aspect. In [22], a process is defined as:

“a collection of inter-related events, activities and decision points that involve a number of actors and objects, and that collectively lead to an outcome that is of value to at least one customer”.

The definition highlights, in fact, that a process involves a number of actors, of which at least one is external to the organization. This generalizes to multiple external actors that may be involved in the process execution: from providers furnishing input material, resources, and/or services to the organization, to customers and other external stakeholders that are interested in the value produced through the process.

Collaborative work processes are hence widespread. In this work, we consider how collaboration is handled by taking the subjective perspective of one of interacting parties, singling out the process orchestrated by the in-focus party and how it relates to the behavior of other parties. Other approaches are obviously possible: for example, collaboration can be globally captured in a choreography model, from which local processes can be derived.

In the context of service interaction and execution, these aspects have been tackled when formalizing and analyzing collaborative processes [1, 5, 46], and in the context of realizability for multi-party choreographic processes, considering that they must be enacted in a decentralized way through interaction of the parties, which in turn call for ensuring that they locally have enough visibility of the current state of affairs when required to perform some task [20, 36]. More recently, similar notions have been applied to BPMN collaborative processes, sometimes indeed reflecting the two sources of nondeterminism [13], and sometimes instead blurring them [33]. Such a blurring can be distinctively seen in widely employed Petri net encodings of BPMN [21, 37], where radically different constructs such as internal decisions, event-based gateways, and boundary events are all captured as free choices in the Petri nets.

A flourishing line of research on this matter exists also for declarative processes. Several approaches have brought forward formal models for collaborative/distributed process specifications, with two main lines respectively focused on Dynamic Condition Response (DCR) Graphs [31, 32] and artifact-centric formalisms [4, 23]. The common theme of these works is to ensure the overall correct design and executability of distributed, collaborative processes that emerge from the composition of local declarative components. Local processes are typically composed under a cooperative assumption, where their internal non-determinism related to the choices they take is aligned with that of the others.

In our approach, we consider a different setting, where collaboration is in a way approached “cautiously”, considering that when the process of an in-focus party interacts with external participants, those external participants enact their own, at least not fully controllable independent processes. This interpretation dates back to seminal contributions on open, reactive systems [30, 42], where two sources of non-determinism have to be considered. On the one hand, there is non-determinism resolved by the choices internally taken by the in-focus process; on the other hand, there is non-determinism arising from the external choices picked by the other parties. While the first is within the scope of the local orchestration, and hence can be resolved existentially, the second is uncontrollable, and thus all possibilities have to be taken into account by the process.

This delicate interplay is apparent by looking into de-facto process modelling notations, such as BPMN. There, internal control-flow structures are paired with corresponding structures dealing with external actors and events, leading to constructs such as message exchange, different types of unsolicited events, boundary events attached to exception flows, and event-driven gateways. All such structures are used to indicate routes that are taken by the process not due to internal decisions of its orchestrator, but based on which of the external events (from the set of o available ones) occurs first.

Surprisingly, collaborative processes have never been studied in the context of \(\textsf{DECLARE}\), where constraints are in fact all combined together without distinguishing how they interact with the different sources of control. In fact, \(\textsf{DECLARE}\) [40, 41] simply defines a process as a monolithic set of activities equipped with a set of constraints composed in a conjunction. No distinction is given based on which parties (or agents) control which actions. Similarly, constraints are not differentiated among those that define the context of execution (e.g., indicating under which conditions external partners can interact with the process), and those that capture the expected behavior of the in-focus process (e.g., expressing what the process should do in response to external stimuli).

In this work, we close this gap by introducing collaborative \(\textsf{DECLARE}\) (\(\textsf{coDECLARE}\)), where activities are assigned to the internal orchestrator or to external participants, and constraints are partitioned into conditions capturing assumptions on how the external participants can interact with the in-focus process, and conditions that express guarantees provided by the in-focus process. This reflects a peculiar characteristics when dealing with work processes or, more in general, information systems, which makes them different from general reactive systems where the environment is often assumed to be completely uncontrollable. In fact, when external stakeholders interact with a process enacted by a single party, they freely decide which task to select next among the possible ones made available to them. In this sense, the presence of external actors requires the process to define the context of interaction, and then to suitably react to all possible interactions within this context. On the one hand, the process defines the assumptions under which its external parties can send messages/generate events that have to be handled. On the other hand, external actors are uncontrollable, thus calling the in-focus process to be able to guarantee a suitable management of all possible situations within the space of possibilities defined by the context.

To handle these features, we resort to the long-standing literature on realizability and synthesis for temporal specifications, widely studied in AI and formal methods, and we show how to lift it for defining \(\textsf{coDECLARE}\) and solve key tasks related to correctness and enactment. Our main contributions are as follows:

  1. 1.

    We discuss why it is essential in this collaborative setting to distinguish responsibility over activities and separate constraints into assumption and guarantee constraints.

  2. 2.

    We define \(\textsf{coDECLARE}\) and discuss how central tasks such as that of \(\textsf{DECLARE}\) consistency and enactment have to be redefined in the light of collaborative, declarative processes.

  3. 3.

    We show how consistency and enactment of \(\textsf{coDECLARE}\) specifications can be reduced to realizability and synthesis for Linear Temporal Logic over finite traces (\(\textsf{LTLf}\)) , for which very mature implementations exist [6, 10, 27, 29, 48, 50].

The paper is organized as follows. In Sect. 2 we review the necessary background. In Sect. 3 we introduce the framework of collaborative \(\textsf{DECLARE}\). Section 4 formally defines the consistency and enactment for \(\textsf{coDECLARE}\), whereas Sect. 5 shows how those can be effectively checked and computed using the existing reactive synthesis techniques. Conclusions and future directions follow.

2 A Bird-Eye-View on \(\textsf{LTLf}\) and \(\textsf{DECLARE}\)

We recall the necessary background on \(\textsf{LTL}\) on finite traces (\(\textsf{LTLf}\)), and how it is used to formalize the \(\textsf{DECLARE}\) language.

2.1 \(\textsf{LTLf}\)

\(\textsf{LTLf}\) is a temporal logic to express properties of finite traces.

Definition 1

(Syntax of LTLf). Given a set \(\varSigma \) of proposition letters, a formula \(\phi \) of \(\textsf{LTLf}\) is defined as follows [18]:

figure a

where \(p \in \varSigma \). Formulas of \(\textsf{LTLf}\) over the alphabet \(\varSigma \) are interpreted over finite traces (or state sequences, or words), i.e., sequences in the set \((2^\varSigma )^{+}\).    \(\triangleleft \)

Intuitively, indicates strong next, postulating that there must exist a next state in the trace, and \(\phi \) must hold therein. Instead, indicates weak next, capturing that if a next state exists, then \(\phi \) must hold therein. Hence, evaluates to false in the last state of the trace, while evaluates to true, both regardless of \(\phi \). Formula indicates instead until, capturing that later in the trace (obviously, before the end of the trace) \(\phi _2\) must hold, and in all the states between the current one and the one where \(\phi _2\) holds, \(\phi _1\) must hold.

In the following, we will write general finite trace semantics to denote the interpretation under these structures. Let \(\sigma = \langle \sigma _{0}, \ldots , \sigma _{n-1} \rangle \in (2^{\varSigma })^{+}\) be a finite trace. We define the length of \(\sigma \) as \(|\sigma | = n\). With \(\sigma _{[i,j]}\) (for some \(0\le i\le j<|\sigma |\)) we denote the subinterval \(\langle \sigma _i,\dots ,\sigma _j \rangle \) of \(\sigma \).

Definition 2

(LTLf satisfaction relation, model, language, equivalence). Given an \(\textsf{LTLf}\) formula \(\phi \) over \(\varSigma \), the satisfaction relation of \(\varSigma \) by trace \(\sigma \in (2^{\varSigma })^{+}\) at time \(0 \le i < |\sigma |\), denoted by \(\sigma , i \models \phi \), is inductively defined as:

  • \(\sigma ,i \models p\) iff \(p\in \sigma _i\);

  • iff \(p\not \in \sigma _i\);

  • iff \(\sigma ,i \models \phi _1\) or \(\sigma ,i \models \phi _2\);

  • \(\sigma ,i \models {\phi _1 \wedge \phi _2}\) iff \(\sigma ,i \models \phi _1\) and \(\sigma ,i \models \phi _2\);

  • iff \(i+1<|\sigma |\) and \(\sigma ,i+1\models \phi \);

  • iff either \(i+1=|\sigma |\) or \(\sigma ,i+1\models \phi \);

  • iff there exists \(i\le j<|\sigma |\) such that \(\sigma ,j\models \phi _2\), and \(\sigma ,k\models \phi _1\) for all k, with \(i \le k < j\).

Table 1. \(\textsf{DECLARE}\) patterns together with their \(\textsf{LTLf}\) formalization
Full size table

We say that \(\sigma \) is a model of \(\phi \) (written as \(\sigma \models \phi \)) iff \(\sigma ,0 \models \phi \). The language (over finite trace) of \(\phi \), denoted by \({{\,\mathrm{\mathcal {L}}\,}}(\phi )\), is the set of traces \(\sigma \in (2^\varSigma )^+\) such that \(\sigma \models \phi \). We say that two formulas \(\phi , \psi \in \textsf{LTLf} \) are equivalent iff \({{\,\mathrm{\mathcal {L}}\,}}(\phi )={{\,\mathrm{\mathcal {L}}\,}}(\psi )\).   \(\triangleleft \)

As customary, we define the following abbreviations: (eventually) captures that \(\phi \) holds at some moment in the future, (globally) captures that \(\phi \) holds from the current state to the end of the trace, and weakens by not necessarily requiring that \(\phi _2\) becomes true. Also notice that .

2.2 \(\textsf{DECLARE}\)

\(\textsf{DECLARE}\) is a framework [41] and a language [40] for the declarative specification of processes, enjoying flexibility by design [44]. We refer to [39] for a thorough treatment of declarative processes.

A \(\textsf{DECLARE}\) specification consists of a finite set of patterns used for constraining the allowed execution traces of the process. Each pattern is defined over a set of (atomic) actions, and has a semantics based on \(\textsf{LTLf}\). Table 1 recalls the typical \(\textsf{DECLARE}\) patterns and their \(\textsf{LTLf}\) formalization.

In the context of this work, we actually support arbitrary patterns in \(\textsf{LTLf}\), going beyond the patterns of Table 1. We therefore directly use \(\textsf{LTLf}\) formulas in place of constraint patterns.

Definition 3

(DECLARE specification). A \(\textsf{DECLARE}\) specification is a pair \(\langle \mathcal {A},\mathcal {C}\rangle \), where \(\mathcal {A}\) is a finite set of activities, and \(\mathcal {C}\) is a finite set of \(\textsf{LTLf}\) formulas over \(\mathcal {A}\), called constraints.    \(\triangleleft \)

\(\textsf{DECLARE}\) also comes with a graphical notation. We illustrate next a \(\textsf{DECLARE}\) specification, which will be used throughout the entire paper.

Example 1

Consider the \(\textsf{DECLARE}\) specification from Fig. 1(a), shown in the standard graphical notation associated to \(\textsf{DECLARE}\). The specification is a fragment of an order-to-cash process. The specification dictates that an order can be paid or canceled at most once (constraint 0..1 on cancel and pay). Whenever an order is paid, then the customer address has to be set at least once, wither before or after the payment (resp-existence(pay,set)). Upon payment either shipment or refund should eventually occur (response(pay,\(\texttt {ship} \vee \texttt {refund}\))). In turn, shipment and refund can only occur after payment (precedence(pay,ship) and precedence(pay,refund)). Shipment is only possible if the address has been set (precedence(pay,ship)), and the address cannot be updated anymore once shipment occurs (neg-response(ship,set)). Finally, shipment and cancelation are mutually exclusive (not-coexistence(cancel,ship)).   \(\triangleleft \)

Differently from arbitrary \(\textsf{LTLf}\) formulas, \(\textsf{DECLARE}\) assumes that every state corresponds to the execution of one and only one activity, that is, that exactly one proposition is true therein [16, 25]. This leads to a semantics based on so-called simple finite traces.

Definition 4 (Simple finite trace)

A simple finite trace over \(\mathcal {A}\) is a finite trace \(\sigma =\langle \sigma _0,\dots ,\sigma _n \rangle \in \mathcal {A}^+\), such that for every \(i \in \{ 0,\ldots ,|\sigma -1| \}\), we have \(|\sigma _i|=1\).   \(\triangleleft \)

Definition 5

(DECLARE model trace). Given a \(\textsf{DECLARE}\) specification \(\mathcal {D}= \langle \mathcal {A},\mathcal {C}\rangle \), a simple trace \(\sigma \) over \(\mathcal {A}\) is a model trace of \(\mathcal {D}\) if \(\sigma \models \bigwedge _{\varphi _i \in \mathcal {C}} \varphi _i\).   \(\triangleleft \)

We close by recalling that, without loss of generality, one can redefine the notion of model trace by taking as input an arbitrary \(\textsf{LTLf}\) trace, proviso altering the \(\textsf{DECLARE}\) specification with an additional special formula forcing the arbitrary trace to be simple.

Remark 1

([24, 39]). Given a \(\textsf{DECLARE}\) specification \(\mathcal {D}= \langle \mathcal {A},\mathcal {C}\rangle \), to check wether an arbitrary model trace \(\sigma \) over \(\mathcal {A}\) is indeed a model trace of \(\mathcal {D}\) we check whether \(\sigma \models \psi _{simple}(\mathcal {A}) \bigwedge _{\varphi _i \in \mathcal {C}} \varphi _i\), where for a set S of propositions we define .   \(\triangleleft \)

3 Collaborative \(\textsf{DECLARE}\)

We now critically assess the notion of simple traces (Definition 4), and that of \(\textsf{DECLARE}\) specifications (Definition 3), in the light of collaborative processes, such as actually the one introduced in Example 1.

Fig. 1.
figure 1

A graphical representation of an order handling process in \(\textsf{DECLARE}\) (a), then refined in (b) as a \(\textsf{coDECLARE}\) specification. Rectangles denote actions, connectors constraints. Customer action s/constraints are in orange, those of the seller in blue. (Color figure online)

Full size image

3.1 Executing a Collaborative Process

By inspecting Example 1, it is clear that the activities contained in the specification cannot be all ascribed to a single locus of execution. Instead, the process brings together two parties: a seller - responsible for orchestrating the order-to-cash process, and a customer, representing the external participant. In this light, the first important change we need to apply to the specification, is to actually assign the different activities to one of the two parties.

Example 2

In the order-to-cash process of Fig. 1, activities set address and pay are controlled by the customer, while cancel, ship, refund are controlled by the seller.   \(\triangleleft \)

In case of multiple external parties, for the purpose of this paper we can all model them as a single, external party, as it is typically done in the literature [34, 43]. In fact, what matters is distinguishing the two different sources of nondeterminism when choosing which activity to execute: the one of the orchestrator, or that of external, uncontrollable actors. From now on, we refer to the orchestrator as controller, and to the external parties as environment.

Since the environment is uncontrollable, capturing a process execution as a simple trace (in the sense of Definition 4) is overly restrictive. Conceptually speaking, in fact, the process specification is given to controller, and therefore it is in the interest of controller to ensure that the resulting trace satisfies the specification.

In fact, controller has to observe what environment has done so far, so as to suitably react. For example, the seller may decide to behave differently depending on whether the customer has paid and later cancelled or not. This calls for moving from the notion of simple trace to that of process strategy for controller.

Definition 6 (Process strategy)

Let \(\mathcal {A}^E\) and \(\mathcal {A}^C\) be two disjoint sets of activities, respectively denoting the environment and the controller activities. A process strategy is a function \(s:(E)^+\rightarrow P\) that for every finite sequence \(\textbf{e}=\langle e_0,\ldots ,e_n \rangle \) of activities chosen by the environment, determines the next activity \(P_n=s(\textbf{e})\) executed by the controller.   \(\triangleleft \)

Notice that a process strategy respects the original \(\textsf{DECLARE}\) semantics of simple traces, as it enables only one activity to be executed per state.

One may wonder why the process strategy does not use the whole partial trace accumulated so far, including the activities of both the environment and the controller, but instead merely focuses on previous activities executed by environment. As we will see, more sophisticated notions of process strategies will not be needed to solve the key tasks of collaborative processes.

3.2 Satisfying the Constraints of a Collaborative Process

Now that we have a notion of process strategy, we can imagine that the orchestrator uses it to guarantee that the constraints of the \(\textsf{DECLARE}\) specification of interest are indeed all satisfied when concluding the execution (that is, the strategy yields, at completion time, a model trace). However, considering that the environment is uncontrollable, it turns out that this is impossible even for very trivial \(\textsf{DECLARE}\) specifications that assign at least one activity to environment.

Example 3

Consider the \(\textsf{DECLARE}\) specification of Fig. 1(a), with the activity partitioning from Example 2. The seller cannot define a process strategy that guarantees the satisfaction of all constraints, since the customer controls activities that are subject to unary constraints (0..1 on cancel and pay) or binary constraints all related to the customer (resp-existence(pay,set)). Since the customer is uncontrollable, they may issue two payments, or two cancelations, or may pay without ever setting an address.   \(\triangleleft \)

Example 3 witnesses that we cannot monolithically consider all specification constraints as being under the responsibility of the controller, while leaving environment free to generate an arbitrary sequence of activities under their responsibility. In fact, as stated in the introduction, external parties need to come with some context on their freedom of choice. This is concretely reflected inside BPM systems, which expose executable activities to the external parties, and define how to handle external events, only under certain circumstances.

To reflect this requirement in our declarative setting, we give constrained freedom to the environment, by partitioning the constraints into those that must be respected by the environment to properly interact with the process, and those that the controller has to satisfy. This reflects the paradigm of assume-guarantee contracts [7]: under the assumption that the environment behaves in such a way that their constraints are satisfied, the orchestrator is bound to guarantee the satisfaction of their own constraints.

With this intuition in mind, we define collaborative \(\textsf{DECLARE}\) specifications.

Definition 7

(coDECLARE specification). A collaborative \(\textsf{DECLARE}\) (\(\textsf{coDECLARE}\)) specification is a tuple \(\mathcal {D}=\langle \mathcal {A}^E,\mathcal {A}^C,\mathcal {C}^E,\mathcal {C}^C\rangle \), where:

  • \(\mathcal {A}^E\) is a finite set of environment activities;

  • \(\mathcal {A}^C\) is a finite set of controller activities, with \(\mathcal {A}^E\cap \mathcal {A}^C= \emptyset \);

  • \(\mathcal {C}^E\) is a set of \(\textsf{LTLf}\) constraints over \(\mathcal {A}^E\cup \mathcal {A}^C\) representing the environment constraints;

  • \(\mathcal {C}^C\) is a set of \(\textsf{LTLf}\) constraints over \(\mathcal {A}^E\cup \mathcal {A}^C\) representing the controller constraints;

We respectively call \(\mathcal {D}^a= \langle \mathcal {A}^E\cup \mathcal {A}^C,\mathcal {C}^E\rangle \) and \(\mathcal {D}^g= \langle \mathcal {A}^E\cup \mathcal {A}^C,\mathcal {C}^C\rangle \) the assumption and guarantee specifications of \(\mathcal {D}\).   \(\triangleleft \)

Example 4

We refine the \(\textsf{DECLARE}\) specification of Fig. 1(a), considering the activity partitioning from Example 2, into the \(\textsf{coDECLARE}\) specification \(\mathcal {D}_{order}\) of Fig. 1(b). The partitioning is done according to the following idea. To participate to the order handling process, the customer has to commit to: (i) paying and cancelling at most once, (ii) ensuring that an address is set upon payment, (iii) not updating the address nor cancelling once the seller has shipped the order. At the same time, the seller commits to: (i) shipping only if the customer sets an address and pays, (ii) refunding only if a previous customer payment exists, (iii) ensuring that shipment or refund occur whenever the customer pays, (iv) not shipping if the customer cancels the order. One can see that the vast majority of constraints present in the original \(\textsf{DECLARE}\) specifications have been maintained and assigned either to the environment (customer) or the controller (seller). The only exception is the not coexistence constraint relating cancelation and shipment, which is now refined into two time-oriented constraints, one assuming that the customer does not cancel after a seller’s shipment (\(\textsf {neg-response}(\texttt {ship},\texttt {cancel})\)), and the other guaranteeing that the seller does not ship after a customer’s cancelation ((\(\textsf {neg-response}(\texttt {cancel},\texttt {ship})\)).   \(\triangleleft \)

We can directly lift the notion of model trace (as per Definition 5) to the case of \(\textsf{coDECLARE}\). To do so, we formalize the intuition given so far: the trace must be such that whenever it satisfies the assumption on the environment, then it must satisfy the guarantee on the orchestrator. This implicitly means that executions violating the assumption on the environment are all considered model traces, as these are traces over which the environment cannot claim any guarantee. This is in line with the notion of assume-guarantee contract [7], and that of assume-guarantee synthesis [8, 11, 38].

Definition 8

(coDECLARE model trace). Given a \(\textsf{coDECLARE}\) specification \(\mathcal {D}=\langle \mathcal {A}^E,\mathcal {A}^C,\mathcal {C}^E,\mathcal {C}^C\rangle \), a simple trace \(\sigma \) over \(\mathcal {A}^E\cup \mathcal {A}^C\) is a model trace of \(\mathcal {D}\) if, whenever it is a model trace for \(\mathcal {D}^a\) (in the sense of Definition 5), then it is also a model trace for \(\mathcal {D}^g\) (again in the sense of Definition 5).   \(\triangleleft \)

Example 5

Consider the \(\textsf{coDECLARE}\) specification \(\mathcal {D}_{order}\) of Fig. 1(b). Four model traces for \(\mathcal {D}_{order}\) are \(\langle \texttt {set},\,\texttt {pay},\,\texttt {ship}\rangle \), \(\langle \texttt {pay},\,\texttt {set},\,\texttt {refund}\rangle \), \(\langle \texttt {pay},\,\texttt {set}\,\texttt {cancel}\,\texttt {refund}\rangle \), and \(\langle \texttt {pay}\,\texttt {set}\,\texttt {ship}\,\texttt {cancel}\rangle \). They respectively denote a good execution where the order is shipped, an execution where the seller decides to refund for an internal problem, and an execution where the seller refunds due to a customer cancellation, and one where no refund is given in spite of cancellation since the order has been already shipped. The trace \(\langle \texttt {pay}\,\texttt {set}\,\texttt {cancel}\rangle \) is instead not a model trace, as the seller should refund.   \(\triangleleft \)

The main open question now is: how can the orchestrator ensure that an ongoing execution for a \(\textsf{coDECLARE}\) model eventually leads to a proper, model trace? The challenge here is that, even if the environment is constrained by their assumption specification, it still has a (constrained) freedom to decide which environment activities are executed, and in which order. Hence, to be able to properly execute the specification, the orchestrator must have a strategy (in the sense of Definition 6) to guarantee that no matter how the environment behaves within the space given by the assumption specification, then the execution is progressed and finally stopped by satisfying the guarantee specification. This is tackled in the next section.

4 Consistency and Enactment of \(\textsf{coDECLARE}\)

To tackle the problem of enactment of \(\textsf{coDECLARE}\) specifications, we start pointing out the striking similarity with the long-standing problem of synthesis from declarative specification, which dates back to Church [12]. In summary, given a declarative specification, one can define two distinct problems. The first concerns verification, and is about checking the correctness of the specification, namely whether the specification has a satisfying assignment (which, in the case of linear temporal specifications, means a trace). A different problem is that of synthesis, which deals with deriving a correct-by-construction program (in the shape, e.g., of a Mealy or Moore machine, I/O-transducer, or circuit) that realizes the specification and makes it possible to execute it. Extensive research has been conducted on different synthesis settings, considering in particular closed and open (also called reactive) systems, starting from the seminal contributions by Harel, Pnueli and Rosner [30, 42]. In the reactive setting, using the same terminology adopted here, the system (referred to as controller) interacts with an uncontrollable environment, which, in turn, can affect the behavior of the controller. Reactive synthesis is hence modeled as a two-player game between Controller, whose aim is to satisfy the formula, and Environment, who tries to violate it. The objective of the synthesis task is then to synthesize a program for Controller indicating which actions the Controller should take to guarantee the satisfaction of the declarative specification of interest, no matter what are the actions taken by Environment. This problem was originally studied in [12] and solved in [9], and for \(\textsf{LTL}\) specifications in particular it was shown to be -complete [43, 45]. The high theoretical complexity and practical infeasibility of the original approach, led to a plethora of studies focused on settings more amenable to effective synthesis algorithms, one of the most important being synthesis for \(\textsf{LTLf}\)- thus considering finite traces [28].

In this section, we connect such long-standing literature with \(\textsf{coDECLARE}\), in particular defining consistency and (automatic) enactment for \(\textsf{coDECLARE}\) by adapting to our setting the well-established notions of realizability and synthesis from declarative specifications.

4.1 Realizability over Simple Traces

We start by considering the realizability task [43] for \(\textsf{LTLf}\) formulas, in the setting where executions correspond to simple traces (cf. Definition 4). Intuitively, given an \(\textsf{LTLf}\) formula \(\phi \) over two sets of controllable \(\mathcal {C}\) and uncontrollable \(\mathcal {U}\) variables (s.t. \(\mathcal {C}\cap \mathcal {U}=\emptyset \)), we have that \(\phi \) is realizable if there exists a strategy for controller that, no matter the choices made by the environment regarding the variables in \(\mathcal {U}\) to set true, chooses truth assignments to variables in \(\mathcal {C}\) so that \(\phi \) is satisfied. Hereinafter, we talk about variables in the context of general definitions, and activities in the context of \(\textsf{coDECLARE}\) and processes, and use \(\mathcal {A}^E\) and \(\mathcal {A}^C\) as uncontrollable and controllable variables, respectively.

To adapt realizability to our setting, we use process strategies from Definition 6. Since realizability is usually tested using a two-player game between the controller and environment, we postulate that such strategies are applied in the strictly alternating way, and that the environment always starts first. These assumptions will be clarified later.

Definition 9 (Realizability over simple traces)

Let \(\phi \) be an \(\textsf{LTLf}\) formula over \(\mathcal {A}\). \(\phi \) is realizable over simple finite traces iff there exists a process strategy \(s:(\mathcal {U})^+\rightarrow \mathcal {C}\) such that, for any infinite sequence \(\mathcal {U}=\langle \mathcal {U}_0, \mathcal {U}_1, \dots \rangle \in (\mathcal {U})^\omega \) of actions chosen by the environment, there exists \(k\in \mathbb {N}\) such that \({{\,\mathrm{\texttt{simres}}\,}}(s,\mathcal {U})_{[0,k]} \models \phi \).Footnote 1   \(\triangleleft \)

First and foremost, notice that the way the process strategy starts and completes is perfectly compatible with the notion of a business process. On the one hand, every process instance starts because of an activity triggered by the environment. On the other hand, the power to decide when an execution should be stopped is of the controller: it is in fact the internal orchestration mechanism that defines when a process instance reaches a final state. We now comment on strict alternation. First, the fact that every step comes with just a single chosen activity is in line with the notion of simple trace. Second, imposing alternation does not incur in any loss of generality, as we can equip both actors with a no-op activity whose purpose is simply to relinquish control back to the other actor. In our running example (cf. 1(b)), this is for example useful for controller to wait that the customer sets their address when the customer indeed triggers a payment without a prior execution of set.

4.2 Consistency and Orchestration

To ensure that a \(\textsf{coDECLARE}\) specification is consistent, we need to ensure that controller can define a strategy that yields a model trace – as per Definition 8. Considering Definition 10, we thus get the following.

Definition 10 (Consistency)

A \(\textsf{coDECLARE}\) specification \(\mathcal {D}=\langle \mathcal {A}^E,\mathcal {A}^C,\mathcal {C}^E,\mathcal {C}^C\rangle \) is consistent if the \(\textsf{LTLf}\) formula \(\bigwedge _{\varphi _i \in \mathcal {C}^E} \varphi _i \rightarrow \bigwedge _{\psi _j \in \mathcal {C}^C} \psi _j\) is realizable over simple finite traces.    \(\triangleleft \)

A process strategy witnessing consistency can be effectively seen as an orchestration mechanism for controller: it defines a specific behaviour for controller ensuring that, whenever environment behaves in accordance to the assumption specification, the resulting reactions yield a simple trace satisfying the guarantee specification. Obviously, for a consistent specification, many different process strategyes may exist, resulting in different orchestration mechanisms for the controller. We show this in our running example.

Example 6

Consider the \(\textsf{coDECLARE}\) specification \(\mathcal {D}_{order}\) from Fig. 1(b). Multiple process strategies exist for the seller. We show two. The first is an always refund strategy:

  • The seller simply generates a no-op, unless the customer pays.

  • As soon as the customer pays, the seller immediately reacts by refunding.

The second is a ship as soon as possible strategy:

  • The seller simply generates a no-op, unless the customer pays.

  • If the customer pays, the seller checks whether the customer has already set an address. If so, then the seller immediately ships. If not, then the seller waits for further activities executed by the seller. In particular, since the customer operates under the assumption that an address must eventually be set:

    • if the customer sets the address, the seller immediately ships afterwards;

    • if the customer cancels and only later sets the address, the seller reacts to the cancelation by refunding.

Obviously, many other process strategies exist. For example, ship as soon as possible may be turned into a more cautious strategy where, instead of immediately shipping whenever there are the conditions for doing so, seller waits for a while to see whether customer intends to cancel.   \(\triangleleft \)

Example 6 may show that some of the process strategies for the controller (such as the always refund strategy) are unintended. This should not be seen as a technical limitation of our approach, but rather as the same issue of typical under-specification problems arising in standard \(\textsf{DECLARE}\), a well-known problem that actually pervades declarative modelling languages in general. In fact, additional constraints could be added to cut off some unintended process strategies for the controller, as discussed next.

Example 7

Consider Example 6. We may want to ensure that the seller cannot use always refund as an orchestration mechanism. A possible way to do so would be to constrain that the seller only refunds upon an explicit cancelation of the customer, in particular when this is triggered after a payment. This could be done by adding to the guarantee specification a further constraint \(\textsf {resp-existence}(\texttt {refund},\texttt {cancel})\). Interestingly, in every possible execution strategy for seller, this constraint will be interpreted as the more restrictive constraint \(\textsf {precedence}(\texttt {cancel},\texttt {refund})\); in fact, since \(\texttt {cancel}\) is under the control of the customer, the seller can only guarantee to satisfy \(\textsf {resp-existence}(\texttt {refund},\texttt {cancel})\) by first waiting that the customer indeed cancels, as refunding before a cancellation may lead to a violation of the constraint (if the customer decides not to cancel, which they can legitimately do).   \(\triangleleft \)

5 Encoding into \(\textsf{LTLf}\) Realizability

In this section, we show how \(\textsf{coDECLARE}\) consistency can be checked using the standard decision procedure from the literature on \(\textsf{LTLf}\) realizability [19], also using the same technique to extract actual process strategies for orchestration.

To do so, we have to resolve a mismatch between the definition of realizability over simple traces (in the sense of Definition 10), and the general notion of \(\textsf{LTLf}\) realizability. The mismatches are that in \(\textsf{LTLf}\) realizability: a there is no simple trace semantics, and thus strategies are deciding on sequences of sets of actions; b strict alternation is not required and there is no need to secure exclusive control of only one player over a state in the game runs.

Definition 11

(LTLf strategy, realizability [19]). Given sets \(\mathcal {C}\) and \(\mathcal {U}\) as in the previous section, a strategy is a function \(s:(2^\mathcal {U})^+ \rightarrow 2^\mathcal {C}\). An \(\textsf{LTLf}\) formula \(\phi \) over \(\mathcal {U}\cup \mathcal {C}\) is realizable if there is a strategy s s.t. for every infinite sequence \(\mathcal {U}=\langle \mathcal {U}_0,\mathcal {U}_1,\ldots \rangle \) \(\in (2^\mathcal {U})^\omega \), there exists \(k\in \mathbb {N}\) s.t. \({{\,\mathrm{\texttt{res}}\,}}(s,\mathcal {U})_{[0,k]}\models \phi \), where \({{\,\mathrm{\texttt{res}}\,}}(s,\mathcal {U})= \langle \mathcal {U}_0\cup s(\langle \mathcal {U}_0 \rangle ), \mathcal {U}_1 \cup s(\langle \mathcal {U}_0, \mathcal {U}_1 \rangle ), \ldots \rangle \) is the trace resulting from reacting to \(\mathcal {U}\) according to s.   \(\triangleleft \)

Given an \(\textsf{LTLf}\) formula \(\phi \), the decision procedure for checking realizability of \(\phi \) performs the following steps [19]. First, build a non-deterministic finite automaton \(\S \) for \(\phi \) and determinise it. Then, play a reachability game using \(\S \) as the arena so as to check whether the process can reach a final state of the automaton (see  [34] for more details on the actual procedure for this step). If this is the case, then \(\phi \) is realizable, otherwise it is not.

Notice that the first step, in the worst case, takes double exponential time: \(\S \) has at most exponentially many states [19] and the standard subset construction algorithm for determinization of \(\S \) will require potentially lead to exponential blow-up in the number of states of the resulting deterministic automaton. The reachability game can be solved in polynomial time in the size of automaton [14] and thus does not affect the overall complexity. Notice also that if \(\phi \) is shown to be realizable, then a strategy s can be extracted [34]. In practice, using various heuristics, the first step can be computed efficiently for \(\textsf{DECLARE}\)  [15, 47].

An important step towards reducing the consistency check (and in turn synthesis of process strategies for orchestration) to realizability (and synthesis) of \(\textsf{LTLf}\) over finite traces is in enforcing the assumptions made in Sect. 4 on the two-player game used for realizability checking. To this end, we define the following auxiliary \(\textsf{LTLf}\) formulas, making sure that (i) the game of the play is a simple trace; (ii) the environment plays at all even states; (iii) the controller plays at all odd states. The formulas are as follows:

figure s

We use here the weak next (i.e., ) operator to ensure that the two-player game used for checking the realizability of these formulas can stop at any iteration.

The following theorem from [26] shows how we can recast the realizability technique discussed above to the case if \(\textsf{coDECLARE}\) specifications.

Theorem 1

([26]). Let \(\mathcal {D}=\langle \mathcal {A}^E,\mathcal {A}^C,\mathcal {C}^E,\mathcal {C}^C\rangle \) be a \(\textsf{coDECLARE}\) specification. It holds that \(\mathcal {D}\) is consistent iff the \(\textsf{LTLf}\) formula \(\psi _{simple}(\mathcal {A}^E\cup \mathcal {A}^C) \wedge \psi _{con}(\mathcal {A}^C) \wedge ((\psi _{env}(\mathcal {A}^E) \wedge \mathcal {C}^E) \rightarrow \mathcal {C}^C)\) is realizable.   \(\triangleleft \)

Tool Support. The formula from Theorem 1 can be given as input to the realizability algorithm discussed above. This makes it possible to use any off-the-shelf tool for \(\textsf{LTLf}\) synthesis for the purpose of \(\textsf{coDECLARE}\) consistency and orchestration. This paves the way towards a direct implementation of our approach. In fact, since the introduction of the \(\textsf{LTLf}\) reactive synthesis problem [19], several optimized tools have been developed for solving this problem. Among all, we mention the Syft [51] and the Cynthia tools [17]. \(\textsf{LTLf}\) reactive synthesis is an active area of research: this is witnessed also by the organization of an annual competition (SYNTCOMP [34, 35]). We thus expect that the practical efficiency of \(\textsf{LTLf}\) synthesis tools reflect also to \(\textsf{coDECLARE}\) enactment.

6 Conclusions

We have introduced a novel framework to capture collaborative, declarative processes specified in \(\textsf{DECLARE}\), where the process orchestrator (i.e., the controller) must be able to suitably handle the interaction with uncontrollable external parties (i.e., the environment). We have described how this framework, called \(\textsf{coDECLARE}\), can be naturally framed in an assume-guarantee style, where the following behavioral contract is stipulated by the controller and environment: under the assumption that the environment behaves according to an assumption \(\textsf{DECLARE}\) specification, the controller ensures to react by satisfying a guarantee \(\textsf{DECLARE}\) specification. We have shown, both foundationally and in terms of algorithmic support, how this framework can be connected to the well-studied framework of realizability and synthesis for \(\textsf{LTLf}\) specifications.

The natural, next step is to leverage this connection and provide a proof-of-concept implementation for consistency checking and process strategy generation for orchestration in \(\textsf{coDECLARE}\), calling different back-end \(\textsf{LTLf}\) realizability/synthesis tools. We are also studying that when the \(\textsf{LTLf}\) formulas of interest have the shape of \(\textsf{DECLARE}\) patterns, better complexity bounds for solving these problems can be obtained [26]. We also foresee three interesting foundational lines of research starting from the basis provided here. The first concerns the definition of variants of consistency/orchestration for \(\textsf{coDECLARE}\), in the case where the overall specification turns out to be unrealizeable. To this end, so-called best-effort strategies have been introduced [2]. However, while in our setting assume-guarantee specifications can be treated by constructing an implication formula, this is not true anymore in the case of best-effort strategies, and more sophisticated notions of synthesis under assumption have to be studied [3]. The second line concerns the actual process strategies generated from a \(\textsf{coDECLARE}\) specification. As discussed in the paper, each strategy defines a particular way for controller to ensure that whenever the environment behaves according to the assumption specification, then the guarantee specification is satisfied. In a BPM context, it would be definitely of interest to lift synthesis to a more general orchestration mechanism, where all possible strategies are combined, allowing the controller to decide at runtime, step-by-step, which specific strategy to follow. This is akin to maximally permissive strategies [49], but novel research is needed to represent them by natively dealing with concurrency and other typical control-flow patterns. A last line is to consider different notions of collaboration when dealing with \(\textsf{DECLARE}\) specifications. A significant setting, which departs from the one tackled here, is that where collaboration is approached in a choreographic way, observing interaction from an external point of view, and considering all the interacting parties are equally standing. This was partly studied in some seminal works [39, Chapter 8], [40], but not further developed so far.