ServLog : A unifying logical framework for service modeling and contracting

Abstract

Implementing semantics-aware services, which includes semantic Web services, requires novel techniques for modeling and analysis. The problems include automated support for service discovery, selection, negotiation, and composition. In addition, support for automated service contracting and contract execution is crucial for any large scale service environment where multiple clients and service providers interact. Many problems in this area involve reasoning, and a number of logic-based methods to handle these problems have emerged in the field of Semantic Web Services. In this paper, we lay down theoretical foundations for service modeling, contracting, and reasoning, which we call ServLog, by developing novel techniques for modeling and reasoning about service contracts with the help of Concurrent Transaction Logic. With this framework, we significantly extend the modeling power of the previous work by allowing expressive data constraints and iterative processes in the specification of services. This approach not only captures typical procedural constructs found in established business process languages, but also greatly extends their functionality, enables declarative specification and reasoning about services, and opens a way for automatic generation of executable business processes from service contracts.

1. Introduction

The move towards service-aware systems, starting with emergence of service-oriented architectures and service computing [36], and newer approaches such as artifact-centric [29] and data-aware systems [13], microservices [35], and not least the emerging field of service science [43], calls for the development of novel techniques to support various service-related tasks such as service modeling and discovery, service process specification, automated contracting for services, service enactment and monitoring. These issues have been partially addressed by a number of pioneering projects in the area of Semantic Web Services, such as WSMF [20], OWL-S [32],1

¹

http://www.daml.org/services/owl-s/.

WSMO [38],2

²

http://www.wsmo.org/.

SWSL,3

³

http://www.w3.org/Submission/SWSF-SWSL/.

DIP [46],4

⁴

http://dip.semanticweb.org/.

and SUPER [27 ,28],5

⁵

http://ip-super.org/.

and more recently [41]. Nevertheless, many core issues remained largely unsolved. The present paper builds on the previous efforts while primarily addressing the behavioral aspects of services, including service contracting and service contract execution. It complements approaches such as OWL-S and WSMO, which primary focused on semantic annotations for Web services, brings new insights, and points to new directions for research in Semantic Web Services.

In a service-oriented environment, interaction is expected among large numbers of clients and service providers, so making contracts through human interaction is not feasible. To enable automatic establishment of contracts, a formal contract description language is needed, and a reasoning mechanism must verify that the contract terms are fulfilled, as well as support the execution of the contract. A contract specification has to describe the aspects of a service, such as values to be exchanged, procedures, and guarantees. A service contracting and contract execution reasoning mechanism has to decide whether such a specification can actually satisfy the constraints of the parties involved in the contract, and if so, support the execution of the contract in a way that the constraints are satisfied. The present paper develops just such a unifying logical framework, called ServLog.

ServLog is based on Concurrent Transaction Logic (CTR) [11] and continues the line of research that employs CTR as a unifying formalism for modeling, discovering, choreographing, contracting, and enactment of Web services [17,18,39,40,42]. Transaction Logic has also been successfully used in a number of other domains ranging from security verification policies to reasoning about actions and other service-related issues [7,8,22,24,37]. The present work builds on the results reported in [39,40], but greatly extends that previous work through generalization and addition of new modeling and reasoning techniques. All this is achieved while at the same time significantly simplifying the technical machinery. The contributions with respect to our previous work are detailed in Section 6. With ServLog we lay down the theoretical foundations for service contracting. Specifically, we extend the expressive power of the constraint language used for specifying contracts, allow iterative processes, and allow to pass arguments to processes. We also extend our reasoning techniques to deal with the new expressive variety of modeling primitives, making it possible to address an array of issues in service contracts, ranging from complex process descriptions to temporal and data constraints. The inference procedure for CTR developed here also contributes to the body of results about CTR itself – it covers CTR conjunctive formulas that enable execution of constrained transactions, which previous CTR proof theory was not able to handle. We also develop a logical language for specifying and enacting processes of great complexity.

While this paper aims to be self-contained and we went to great length to provide sufficient details on CTR, it is clear that we must assume certain background from the reader. Specifically, the paper requires proficiency in basic predicate calculus and logic programming.

The remainder of this paper is organized as follows. Section 2 informally describes the basic techniques from service contract specification used in ServLog and introduces the problem of service contracting and service contract execution. Section 3 gives a short introduction to CTR to keep the paper self-contained. Section 4 formally defines modeling constructs. Section 5 describes the reasoning procedure of ServLog – the key component of service contracting and contract execution in our framework. Section 6 discusses related works and contrasts them with ServLog. Section 7 concludes the paper.

2. Service modeling, contracting, and contract execution

There is a number of modeling languages for capturing interactions between services and clients (or among internal tasks within the same service), some focusing on specific features and targeting different audiences (e.g. business analysts, Web service developers, etc.). For example, the Business Process Model and Notation (BPMN)6

⁶

http://www.omg.org/spec/BPMN/2.0/.

is a standard for business process modeling and provides a graphical notation for specifying business processes (BPMN distinguishes between public and private processes, choreographies, and collaborations; it can provide different views of internal and external interactions). Another approach to modeling service processes is the WSMO model of choreography,7

⁷

http://www.wsmo.org/TR/d14/.

which is limited to server-side interactions. In contrast, the model of the W3C Choreography Group includes both service-side interactions and client-side interactions.8

⁸

http://www.w3.org/TR/2006/WD-ws-cdl-10-primer-20060619/.

At a higher level of abstraction, however, all interactions can be represented through control and data dependencies between tasks. ServLog captures this level of abstraction in a logic and enables powerful forms of automated reasoning about it. Figure 1 depicts the main aspects of service behavior addressed by ServLog.

Fig. 1.

Elements of the reasoning architecture for services in ServLog.

The service process is described through its control and data flows – a specification that tells how to interact with the service and how data flows among tasks. A service process may also expose inner workings of the service (interactions that are not between the service and the client but between internal tasks of the service or third parties) for common situations in which the service allows the client to impose constraints on how the service process is to be executed.

The service policy component in Fig. 1 is a set of constraints on a service process and on its input. The contract requirements included on the client side of the figure represent the contractual requirements of the user that go beyond the basic functions of a service. (Examples of basic services are selling books and helping with travel arrangements, while an example of a service requirement is the request that the amount should be charged only after shipping.) In ServLog, service processes are described via control and data flow graphs, while service policy and client contract requirements are described via constraints.

We will now discuss these modeling aspects in more detail using a typical order placement scenario. This scenario describes the flow of interaction between a client and a service, where the interaction starts with the user placing an order, after which the service initiates a concurrent execution of processing the order items, handling shippers for the items, and receipt of a payment. The order processing workflow ends once the above tasks all finish. Processing the order items, handling shippers, and payment receipt are specified in further details, leaving the possibility for the client and the service to make some choices during the interaction (for example, providing a full payment for the order or paying per item). At the same time, the scenario shows how data (e.g. $\mathit{Order}\mathrm{\#}$ ) flows through the workflow tasks as the interactions happen. In addition, the scenario includes a set of non-trivial constraints imposed by the client and the service, which affect the execution. For example, the service has the policy (expressed as a constraint) of booking a shipper only if there are at least seven items to be sent with the shipper. The description of the scenario ends with the definition of the problems addressed in this paper, namely service contracting and service contract execution.

Fig. 2.

Service process example: A hierarchical control and data flow graph.

Service process  Figure 2 shows the service process described earlier as a hierarchical control and data flow graph, called a process graph. The control flow aspect of process graphs is typically used to specify local execution dependencies among the interactions of the service; it is a good way to visualize the overall flow of control. Data flow complements the control flow by specifying the data dependencies among the interactions.

With Fig. 2 we are not attempting to suggest yet another notation for service processes; the purpose is to introduce and explain our running example in a compact and focused way. Representing the same information, say, in BPMN would have been much bulkier and would require inventing additional notation to compensate for features (such as data flow) that BPMN lacks.

Control flow The nodes in a service process graph represent interaction tasks, which can be thought of as functions that take inputs and/or produce outputs. Some tasks are meant to be executed by the service and some by the client. The distinction between service and client tasks is part of the service process description. In general there can be several actors involved, some acting as clients in one context and services in another.

In Fig. 2, tasks are represented as labeled rectangles. The label of a rectangle is the name of the task and the graph inside the rectangle is the definition of that task. Such a task is called composite because it has nontrivial internal structure. Tasks that do not have associated graphs are primitive. A service process graph can thus be viewed as containing a hierarchy of tasks. The graph shown at the top is the root of the hierarchy. In our example, the tasks of the top-level graph include process_order_items, handle_shippers, and handle_payment. These tasks are composite and their rectangles are shown separately. The task place_order is an example of a primitive task. Such tasks have grey background in the figure. Three such tasks, place_order, full_payment, and pay_one_item, are client tasks. The rest are service tasks.

The top-level graph and each composite task has an initial and a final interaction task, the successor task(s) for each interaction task, and a sign that tells whether all these successors must be executed concurrently (represented by AND-split nodes), or whether only one of the alternative branches needs to be executed non-deterministically (represented by OR-nodes).9

⁹

This non-determinism has an XOR flavor.

For instance, in the top-level graph, all successors of the initial interaction place_order must be executed whereas in the definition of pay either full_payment or pay_per_item is to be executed.

Composite tasks may be marked with the suffix “*”, which means that these tasks may execute multiple times. We call these tasks iterative and differentiate them from non-iterative tasks. Iteration is indicated through recursive occurrences of the same tasks – by placing tasks inside their own definitions. Figure 2 shows two iterative tasks: process_order_items and pay_per_item. For example, process_order_items is an iterative task where a sequence of sub-tasks, select_item followed by process_item can be executed multiple times (for example for each item in the purchase order). Iteration is indicated by an occurrence of a process_order_items box to the right of the process_item box. Note that recursive occurrences of tasks may be followed by other tasks, which gives us a general mechanism for capturing different kinds of iterations, including loops and nesting.

It should now be clear how the control flow aspect of the service process graph in Fig. 2 represents the virtual manufacturer scenario described earlier: first the order is placed (place_order), then the items in the purchase order are processed (process_order_items), delivery is arranged (handle_shippers), and payment is settled (handle_payment). These three tasks are executed in parallel. Once all of them complete, handling of the order is finished (end_order). The other parts of the figure show how each of the above tasks is executed. The important thing to observe here is that some tasks are complex and some primitive; some are to be executed in parallel (the AND-nodes) and some in sequence; some tasks have non-deterministic choice (the OR-nodes) and some are iterative.

Data flow Interaction with a service typically involves passing data and the flow of that data is normally captured using data dependencies between tasks. Such dependencies complement the control flow and complete the description of the service process graph.

Since tasks can be conceptualized as functions that take input and produce output, arguments are attached to tasks to capture both input and output. In Fig. 2, each task-label has one or more arguments. For example, handle_payment has the arguments (Order#,Price), meaning that, to execute handle_payment, Order# and Price must be provided.10

¹⁰

In general, arguments can be in or out (and even in-out). In logic programming, this is typically specified via modes. In our description, the mode should be clear from the context. We avoid specifying the modes explicitly in order to avoid unnecessary distraction.

In our scenario, Order# and Price will be provided by the service’s task place_order, which will generate an order number and compute the price based on the items selected by the client (and the pricing data stored in the database). These data items will then be passed to other tasks, such as handle_payment.

Data-passing between tasks is captured via the shared argument names and through a shared data space (e.g., a database) of the workflow process.11

¹¹

ServLog is independent of the choice of such a shared space.

Data-passing through shared arguments is possible between a task and its direct successors, or within the definition of the same composite task. The scope of arguments is relevant in this case: argument names of a task are logical variables. When they are shared with the task’s direct successors, they refer to the same data items, i.e., data is passed from tasks to their direct successors using shared arguments. This aspect should be familiar from basic logic and logic programming. For example, data identified by Order# in process_order_items(Order#) is the same as the data identified by Order# in place_order(Order#,Price), i.e., place_order passes Order# to process_order_items. In case of a composite task, the names of its arguments are global to that task’s definition, meaning that if subtasks in its definition use the same argument names as the composite task then they refer to the same data items. In this way, the composite task passes data to its subtasks. For example, the composite task process_order_items passes Order# to its process_item subtask.

Note also that sharing via shared variables is bi-directional, as pure logic has no notion of explicit input and output. However, for practical reasons, some logic programming systems accept mode specification and do mode-inference, which allows the user to identify the producers of data.

Data-passing through shared data space is used when passing data is not possible through shared arguments due to the difference in scope of the arguments. This often occurs when data needs to be shared between tasks that have no control dependencies in the control flow part of the service process graph. For example, if select_item(Order#,Item) needs to pass Order# and Item to book_shipper(Ord#,Shipper,Itm), data-passing through shared argument names is not an option, since these subtasks appear inside composite tasks that are not related via control dependencies. To capture such data-passing, a shared database can be used as follows: select_item can store Order# and Item, and book_shipper can read them later. This is depicted by the dashed arc going from select_item to book_shipper. The label on the arc represents the data items that are being passed. In our case, Order# is being passed as Ord# and Item as Itm.

Data items can be consumable or non-consumable. In case of data-passing through shared argument names, data is non-consumable: data-producing tasks share data via all of their out-ports with the receiving tasks. The latter can further share this data with their descendants, and so on. In our example, place_order produces Order#-items, and that item is then shared with process_order_items, handle_shippers, and handle_payment. Note the emphasis on sharing: all tasks involved work on the same copy of the data – the phenomenon that is familiar from basic predicate logic and logic programming. In case of data-passing through a shared database, data can be consumable or non-consumable. It is consumable when each query to the databases is followed by deletion of the queried data item. It is non-consumable data if such deletion is not implied. In our example, the data items that we employ for passing data through a shared database are consumable.

Another aspect of the service process graphs concerns transition conditions on arcs. For example, producer(Item,Producer) in the definition of process_item and itemAvailable(Order#,Producer,Item) or itemUnavailable(Order#,Producer,Item) in the definition of inform_client.12

¹²

Such conditions represent relations queried by service tasks, but which the tasks do not modify (and thus are not used for data passing). That data is not being consumed by the service tasks.

Another example of transition condition is a test of the form $\mathit{Quantity}\mathrm{>}3$ . A transition condition signifies that in order for the next interaction with the service to take place, the condition must be satisfied. Transition conditions are Boolean tests attached to the arcs in the service process graphs. These tests may also be queries to the underlying database. Only the arcs whose transition conditions evaluate to true can be followed at run time. For uniformity, ServLog treats transition conditions formally as a separate type of task.

The final remark concerns the nature of primitive tasks. A primitive task is a black box that performs operations in a way that is completely hidden from ServLog’s reasoning system. It does not mean that the work performed by the task is trivial. For example, place_order may perform database updates to record the order number, price and customer’s information, send an email notification to the customer, perform a credit check, and do many other things. The point is that all these operations might not be of much interest to the service’s logic designer and she might decide to abstract them away. If, however, the details of some formerly primitive task might become important for the reasoning mechanism, the tasks may be elaborated upon and become composite. We will illustrate this idea in a very concrete way in Fig. 6 of Section 4.

Service policies and client contract requirements  Apart from the local dependencies represented directly in control flow graphs, global constraints often arise as part of policy specification. Another case where global constraints arise is when a client has specific requirements to the interaction with the service. These requirements usually have little to do with the functionality of a service (e.g., handling orders); instead they represent guarantees that the client wants before entering into a contract with the service. We call such constrains client contract requirements. In Fig. 3 we give an example of global constraints that represent service policies and client contract requirements for our running example.

Fig. 3.

Global behavioral constraints on iterative processes.

Constraints can be imposed on separate tasks (e.g., a task must or must not execute, may execute a certain number of times) or it can involve several tasks (a task must execute in a certain relationship to another task, e.g., before, after, between). Furthermore, constraints can be combined using Boolean connectives (e.g., a task must execute but after its execution some other task must not execute or must execute some number of times).

Other constraints may involve data only. Examples of such constraints include service pre- and post-conditions. For instance, the requirement that “a confirmation number must be available after the execution of the book_shipper service” is a post-condition for that service, where the confirmation number is a data item in the constraint. Since data in such constraints arise as a result of interactions, this kind of constraint can be seen as a special case of constraints on interactions. Other types of constraints involve Quality of Services (QoS) and Service Level Agreements (SLAs). For instance, “availability provided by the book_shipper service is always greater than the requested availability” is a QoS requirement. ServLog can also model QoS constraints but the treatment of such specialized constraints is outside the scope of this paper.

Fig. 4.

Example of well-formed formula that represents the top-level composite task of Fig. 2.

Service contracting and service contract execution  With a modeling mechanism in place, we define service contracting and service contract execution in ServLog as follows:

• Service contracting: Given a service process (i.e., control and data flow) and a set of service policies and client contract requirements (i.e., constraints), decide whether an execution of the service process that satisfies both the service policies and the client contract requirements exists. Note that it does not matter in the end if this is actually executed but the important aspect is that there is at least one and execution of the contract can proceed.

• Service contract execution: Execute tasks in the process in a way where client and service take turns as prescribed by the control and data flows and the constraints. When a step is proposed, the logic’s proof system verifies if acceptance of that step still leaves the possibility of a successful execution of the entire service process that satisfies all the constraints. If so, the step is accepted and executed; it is rejected otherwise. A list of possible allowed steps can also be suggested by the system at each turn.

To solve the above two problems, Section 4 formally defines service processes, service policies, and client contract requirements using Concurrent Transaction Logic (CTR). Section 5 then extends the original proof theory of CTR to make it possible to address the above reasoning tasks.

3. Overview of CTR

Concurrent Transaction Logic (CTR) [11] is an extension of classical predicate logic, which allows programming and reasoning about state-changing processes. Here we summarize the relevant parts of CTR’s syntax and give an informal account of its semantics. For details we refer the reader to [11].

Basic syntax  The atomic formulas of CTR are identical to those of classical logic, i.e., they are expressions of the form $\mathit{p}\mathrm{(}{\mathit{t}}_1\mathrm{,}\dots \mathrm{,}{\mathit{t}}_{\mathit{n}}\mathrm{)}$ , where p is a predicate symbol and the ${\mathit{t}}_{\mathit{i}}$ ’s are terms constructed of constants, variables, and function symbols. Complex formulas are built with the help of connectives and quantifiers. Apart from the classical ∨, ∧, ¬, ∀, and ∃, CTR has two additional infix connectives, ⊗ (serial conjunction) and ∣ (concurrent conjunction), and a modal operator ⊙ (isolated execution). For instance, $$\begin{array}{c}\odot \mathrm{(}\mathit{p}\mathrm{(}\mathit{X}\mathrm{)}\otimes \mathit{q}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{)}\mid \mathrm{(}\forall \mathit{Y}\mathrm{(}\mathit{r}\mathrm{(}\mathit{Y}\mathrm{)}\vee \mathit{s}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}\mathrm{\left)}\mathrm{\right)}\end{array}$$ is a well-formed formula in CTR, while Fig. 4 contains an example of a well-formed formula that represents the top-level composite task of Fig. 2.

Informal semantics  Underlying the logic and its semantics is a set of database states and a collection of paths. For this paper, the reader can think of states as just relational databases, but the logic is more general and can deal with a wide variety of states. Formally, in this paper, a state is a pair consisting of a state identifier and a relational database.

A path is a finite sequence of state identifiers (constants used to refer to the actual states). For instance, if ${\mathbf{\text{s}}}_1\mathrm{,}{\mathbf{\text{s}}}_2\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{n}}$ are state identifiers, then $⟨{\mathbf{\text{s}}}_1⟩$ , $⟨{\mathbf{\text{s}}}_1\mathrm{,}{\mathbf{\text{s}}}_2⟩$ , and $⟨{\mathbf{\text{s}}}_1\mathrm{,}{\mathbf{\text{s}}}_2\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{n}}⟩$ are paths of length 1, 2, and n, respectively.

As in classical logic, CTR formulas take truth values. However, unlike classical logic, the truth of CTR formulas is determined over paths, not at states. If a formula, ϕ, is true over a path $⟨{\mathbf{\text{s}}}_1\mathrm{,}{\mathbf{\text{s}}}_2\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{n}}⟩$ , it means that ϕ can execute starting at state ${\mathbf{\text{s}}}_1$ . During the execution, the current state will change to ${\mathbf{\text{s}}}_2\mathrm{,}{\mathbf{\text{s}}}_3\mathrm{,}\dots$  , etc., and the execution terminates at state ${\mathbf{\text{s}}}_{\mathit{n}}$ . In such a case we will also call the path $⟨{\mathbf{\text{s}}}_1\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{n}}⟩$ an execution of ϕ.

Although we are interested in execution of CTR formulas over paths, if a formula involves the concurrency operator, the subformulas may be executed in an interleaved fashion, like database transactions. For instance, if $\mathit{\varphi }=\mathrm{(}\mathit{p}\otimes \mathit{q}\otimes \mathit{r}\mathrm{)}\mid \mathrm{(}\mathit{u}\otimes \mathit{v}\mathrm{)}$ , the concurrency operator means that legal executions of ϕ consist of an execution of some part of $\mathit{p}\otimes \mathit{q}\otimes \mathit{r}$ , e.g., p, then of some execution of $\mathit{u}\otimes \mathit{v}$ , e.g., u then again of some part of $\mathit{p}\otimes \mathit{q}\otimes \mathit{r}$ , such as q or even $\mathit{q}\otimes \mathit{r}$ , then the remaining part of $\mathit{u}\otimes \mathit{v}$ , i.e., v, etc. The concurrency operator does not preclude the two parts of ϕ from executing one after another (in any order), but this type of non-interleaved execution is less interesting. In the first, interleaved execution, the two parts of ϕ execute not on paths but on multi-paths, i.e., on sequences of paths. Execution of one part of ϕ may be broken by executions of another part, so the intervening gaps in the execution of $\mathit{p}\otimes \mathit{q}\otimes \mathit{r}$ are filled by executions of $\mathit{u}\otimes \mathit{v}$ (and vice versa).

A multi-path (or an m-path) is a sequence $\mathrm{(}{\mathit{\pi }}_1\mathrm{,}\dots \mathrm{,}{\mathit{\pi }}_{\mathit{k}}\mathrm{)}$ of paths. If $\mathit{\mu }=\mathrm{(}{\mathit{\pi }}_1\mathrm{,}\dots \mathrm{,}{\mathit{\pi }}_{\mathit{k}}\mathrm{)}$ and ${\mathit{\mu }}^{\prime }=\mathrm{(}{\mathit{\pi }}_1^{\prime }\mathrm{,}\dots \mathrm{,}{\mathit{\pi }}_{\mathit{n}}^{\prime }\mathrm{)}$ are two m-paths, their concatenation, $\mathit{\mu }\bullet {\mathit{\mu }}^{\prime }$ , is the m-path $\mathrm{(}{\mathit{\pi }}_1\mathrm{,}\dots \mathrm{,}{\mathit{\pi }}_{\mathit{k}}\mathrm{,}{\mathit{\pi }}_1^{\prime }\mathrm{,}\dots \mathrm{,}{\mathit{\pi }}_{\mathit{n}}^{\prime }\mathrm{)}$ and their interleaving, $\mathit{\mu }\Vert {\mathit{\mu }}^{\prime }$ , is an m-path of the form $\mathrm{(}{\mathit{\kappa }}_1\mathrm{,}\dots \mathrm{,}{\mathit{\kappa }}_{\mathit{k}+\mathit{n}}\mathrm{)}$ such that it is a topological sort of the two sequences μ and ${\mathit{\mu }}^{\prime }$ . For example, one interleaving of $\mathrm{(}⟨{\mathbf{\text{s}}}_1\mathrm{,}{\mathbf{\text{s}}}_2\mathrm{,}{\mathbf{\text{s}}}_3⟩\mathrm{,}⟨{\mathbf{\text{s}}}_6\mathrm{,}{\mathbf{\text{s}}}_7⟩\mathrm{)}$ and of $\mathrm{(}⟨{\mathbf{\text{s}}}_4\mathrm{,}{\mathbf{\text{s}}}_5⟩\mathrm{,}⟨{\mathbf{\text{s}}}_8\mathrm{,}{\mathbf{\text{s}}}_9⟩\mathrm{)}$ is $\mathrm{(}⟨{\mathbf{\text{s}}}_1\mathrm{,}{\mathbf{\text{s}}}_2\mathrm{,}{\mathbf{\text{s}}}_3⟩\mathrm{,}⟨{\mathbf{\text{s}}}_4\mathrm{,}{\mathbf{\text{s}}}_5⟩\mathrm{,}⟨{\mathbf{\text{s}}}_6\mathrm{,}{\mathbf{\text{s}}}_7⟩\mathrm{,}⟨{\mathbf{\text{s}}}_8\mathrm{,}{\mathbf{\text{s}}}_9⟩\mathrm{)}$ . Also, $\mathrm{(}⟨{\mathbf{\text{s}}}_1\mathrm{,}{\mathbf{\text{s}}}_2\mathrm{,}{\mathbf{\text{s}}}_3⟩\mathrm{,}⟨{\mathbf{\text{s}}}_4\mathrm{,}{\mathbf{\text{s}}}_5⟩\mathrm{,}⟨{\mathbf{\text{s}}}_8\mathrm{,}{\mathbf{\text{s}}}_9⟩\mathrm{,}⟨{\mathbf{\text{s}}}_6\mathrm{,}{\mathbf{\text{s}}}_7⟩\mathrm{)}$ is another interleaving, meanwhile $\mathrm{(}⟨{\mathbf{\text{s}}}_1\mathrm{,}{\mathbf{\text{s}}}_2\mathrm{,}{\mathbf{\text{s}}}_3⟩\mathrm{,}⟨{\mathbf{\text{s}}}_6\mathrm{,}{\mathbf{\text{s}}}_7⟩\mathrm{,}⟨{\mathbf{\text{s}}}_4\mathrm{,}{\mathbf{\text{s}}}_5⟩\mathrm{,}⟨{\mathbf{\text{s}}}_8\mathrm{,}{\mathbf{\text{s}}}_9⟩\mathrm{)}$ is a degenerate interleaving.

Finally, a path $\mathit{\pi }=⟨{\mathbf{\text{s}}}_1\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{m}}⟩$ is a merge of an m-path $\mathrm{(}{\mathit{\pi }}_1\mathrm{,}\dots \mathrm{,}{\mathit{\pi }}_{\mathit{n}}\mathrm{)}$ if there are integers $1={\mathit{i}}_0⩽{\mathit{i}}_1⩽{\mathit{i}}_2⩽\cdots ⩽{\mathit{i}}_{\mathit{n}-1}⩽{\mathit{i}}_{\mathit{n}}=\mathit{m}$ such that ${\mathit{\pi }}_1=⟨{\mathbf{\text{s}}}_{{\mathit{i}}_0}\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{{\mathit{i}}_1}⟩$ , ${\mathit{\pi }}_2=⟨{\mathbf{\text{s}}}_{{\mathit{i}}_1}\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{{\mathit{i}}_2}⟩\mathrm{,}\dots \mathrm{,}{\mathit{\pi }}_{\mathit{n}-1}=⟨{\mathbf{\text{s}}}_{{\mathit{i}}_{\mathit{n}-2}}\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{{\mathit{i}}_{\mathit{n}-1}}⟩$ , ${\mathit{\pi }}_{\mathit{n}}=⟨{\mathbf{\text{s}}}_{{\mathit{i}}_{\mathit{n}-1}}\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{{\mathit{i}}_{\mathit{n}}}⟩$ . Note that for the merge to be possible, the end-state of each path ${\mathit{\pi }}_{\mathit{l}}$ in the m-path must be the start-state of the subsequent path ${\mathit{\pi }}_{\mathit{l}+1}$ for each $1⩽\mathit{l}\mathrm{<}\mathit{n}$ . For instance, $⟨{\mathbf{\text{s}}}_1\mathrm{,}{\mathbf{\text{s}}}_2\mathrm{,}{\mathbf{\text{s}}}_3\mathrm{,}{\mathbf{\text{s}}}_4\mathrm{,}{\mathbf{\text{s}}}_5\mathrm{,}{\mathbf{\text{s}}}_6⟩$ is a merge of the m-path $\mathrm{(}⟨{\mathbf{\text{s}}}_1\mathrm{,}{\mathbf{\text{s}}}_2⟩\mathrm{,}⟨{\mathbf{\text{s}}}_2\mathrm{,}{\mathbf{\text{s}}}_3\mathrm{,}{\mathbf{\text{s}}}_4⟩\mathrm{,}⟨{\mathbf{\text{s}}}_4⟩\mathrm{,}⟨{\mathbf{\text{s}}}_4\mathrm{,}{\mathbf{\text{s}}}_5\mathrm{,}{\mathbf{\text{s}}}_6⟩\mathrm{)}$ .

A multi-path structure is a mapping that, for each multi-path μ, tells which ground atomic formulas are true on μ. Informally, this can be understood as telling which ground atomic transactions can execute along μ. Note that CTR formulas hold truth values not over states, but over multi-paths.

First, we connect truth over path of length 1 to database states.

• If s is a state identifier and p is a fact that is true in the database associated with s then p is true over the path $⟨\mathbf{\text{s}}⟩$ (and the m-path $\mathrm{(}⟨\mathbf{\text{s}}⟩\mathrm{)}$ ).

CTR connectives are used to construct composite formulas out of the atomic ones, and the statements below define which composite formulas are true on which multi-paths.

• $\mathit{\varphi }\otimes \mathit{\psi }$ : execute ϕ then execute ψ. Model-theoretically: $\mathit{\varphi }\otimes \mathit{\psi }$ is true over an m-path μ in a multi-path structure if ϕ is true over a prefix m-path of μ, ${\mathit{\mu }}_1$ (in that same structure), and ψ is true over the suffix m-path, ${\mathit{\mu }}_2$ . That is, if $\mathit{\mu }={\mathit{\mu }}_1\bullet {\mathit{\mu }}_2$ .

• $\mathit{\varphi }\mid \mathit{\psi }$ : ϕ and ψ execute concurrently, in an interleaved fashion. That is, $\mathit{\varphi }\mid \mathit{\psi }$ is true over an m-path μ in a multi-path structure if ϕ is true over an m-path ${\mathit{\mu }}_1$ (in that same structure), ψ is true over an m-path ${\mathit{\mu }}_2$ , and μ is one of the interleavings ${\mathit{\mu }}_1\Vert {\mathit{\mu }}_2$ .

• $\mathit{\varphi }\wedge \mathit{\psi }$ : ϕ and ψ execute along the same path. That is, $\mathit{\varphi }\wedge \mathit{\psi }$ is true on an m-path μ if both ϕ and ψ are true on μ. In practice, this is best understood in terms of constraints on execution. For instance, ϕ can be thought of as a non-deterministic transaction and ψ as a constraint on the execution of ϕ. It is this feature of the logic that lets us specify constraints as part of service contracts.

• $\mathit{\varphi }\vee \mathit{\psi }$ : execute ϕ or execute ψ non-deterministically. That is, $\mathit{\varphi }\vee \mathit{\psi }$ is true on an m-path μ if either ϕ or ψ is true on μ.

• $\neg \mathit{\varphi }$ : execute in any way provided that this will not be a valid execution of ϕ. That is, $\neg \mathit{\varphi }$ is true on any m-path on which ϕ is not true. Negation is an important ingredient in temporal constraint specifications.

• $\odot \mathit{\varphi }$ : execute ϕ in isolation, i.e., without interleaving with other concurrently running tasks. That is, $\odot \mathit{\varphi }$ is true on any singleton m-path (an m-path that contains just one path) where ϕ is true. Note: $\odot \mathit{\varphi }$ is never true on an m-path that consists of more than one path, so the execution of $\odot \mathit{\varphi }$ cannot be broken by other executions. This operator enables us to specify non-interleaved parts of service contacts.

When considering the entire service, we are interested in its executions over paths, not m-paths: executions over m-paths are used only to represent concurrently running subtasks of the service. To complete the picture, we define truth of CTR formulas over paths:

• ϕ is true over a path, π, if it is true over an m-path, μ, and π is a merge of μ.

CTR contains a special propositional constant, $\mathtt{\text{state}}$ , which is true only on paths of length 1, that is, on database states. In service processes, $\mathtt{\text{state}}$ is often used as the exit condition for iterative tasks. Another propositional constant that we will use to represent constraints is $\mathtt{path}$ , defined as $\mathtt{\text{state}}\vee \neg \mathtt{\text{state}}$ ; this constant is true on every path.

Concurrent-Horn subset of CTR  The implication $\mathit{p}\leftarrow \mathit{q}$ is defined as $\mathit{p}\vee \neg \mathit{q}$ . The form and the purpose of the implication in CTR is similar to that of Datalog: p can be thought of as the name of a procedure and q as the definition of that procedure. However, unlike Datalog, both p and q take truth values over execution paths, not at individual states.

More precisely, $\mathit{p}\leftarrow \mathit{q}$ means: if q can execute along a path $⟨{\mathbf{\text{s}}}_1\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{n}}⟩$ , then so can p. If p is viewed as a task name, then the meaning can be re-phrased as: one way to execute task p is to execute its definition, q.

To specify service processes we use concurrent-Horn goals and concurrent-Horn rules.

Definition 3.1 (Concurrent-Horn goal).

A concurrent-Horn goal is either an atomic formula or has the form $\mathit{\varphi }\otimes \mathit{\psi }$ , $\mathit{\varphi }\mid \mathit{\psi }$ , $\mathit{\varphi }\vee \mathit{\psi }$ , or $\odot \mathit{\varphi }$ , where ϕ and ψ are concurrent-Horn goals.

When confusion does not arise, we will often talk about CTR goals, omitting the “concurrent-Horn” adjective.

Concurrent-Horn goals occur in our setting in two places: as bodies of the rules that are used to define composite tasks and as formulas that are formal embodiments of control flow graphs. In the latter case, we will be interested in finding out whether a control flow graph can be enacted. Such a question corresponds to proving a statement of the form $\exists \bar{\mathit{X}}\mathit{\varphi }$ , where ϕ is a CTR goal and $\bar{\mathit{X}}$ is the set of variables that occur in ϕ.

Definition 3.2 (Concurrent-Horn rule).

A concurrent-Horn rule is a CTR formula of the form $$\begin{array}{c}\forall \bar{\mathit{X}}\mathrm{(}\mathit{head}\leftarrow \mathit{body}\mathrm{)}\end{array}$$ where $\mathit{head}$ is an atomic formula, $\mathit{body}$ is a concurrent-Horn goal, and $\bar{\mathit{X}}$ is the set of variables that occurs in head and body.

Since all variables in a rule are quantified the same way (universally outside of the rule), we will usually omit explicit quantifiers – a common practice that simplifies the notation.

The concurrent-Horn fragment of CTR has an SLD-style proof procedure that proves concurrent-Horn formulas and executes them at the same time [11]. The present paper significantly extends this proof theory to formulas that contain the ∧ connective thus enabling execution of constrained transactions, which are non-Horn. We also deal with a much larger class of constraints than [17,39], including iterative processes.

Primitive updates  In CTR, primitive updates are ground (i.e., variable-free) atomic formulas that change the underlying database state. Semantically they are represented by binary relations over state identifiers. For instance, if $⟨{\mathbf{\text{s}}}_1\mathrm{,}{\mathbf{\text{s}}}_2⟩$ belongs to the relation corresponding to a primitive update u, it means that u can cause a transition from state ${\mathbf{\text{s}}}_1$ to state ${\mathbf{\text{s}}}_2$ . We will conveniently represent this kind of situation using the following notation: $$\begin{array}{}\text{(1)}& {\mathbf{\text{s}}}_1\stackrel{\mathit{u}}{⟶}{\mathbf{\text{s}}}_2\end{array}$$

Usually the binary relations that represent primitive updates are defined outside of CTR. In that case, they are called transition oracles [9–12]. Transition oracles can be defined using formal English or a number of other formal languages. They can also be represented in CTR as partially defined actions [37]. In either case, the primitive updates can be defined to perform any kind of transformation. For instance, they can add or delete single tuples or sets of tuples, add and delete entire relations, and so on.

In the examples, we will be representing primitive updates using predicate symbols that have variables (e.g., place_order(Order#,Price)). It should be understood that such a predicate represents a family of related updates, one for each instantiation of the variables. Clearly, place_order(12365409,$123) and place_order(09865412,$321) cause similar, but different state transitions.

Constraints  Because formulas are defined on paths, CTR can express a wide variety of constraints on the way formulas may execute. One can place existential constraints on execution (these are based on serial conjunction), or universal constraints, which are based on serial implication. To express the former, we use the propositional constant $\mathtt{path}$ introduced above. For example, $\mathtt{path}\otimes \mathit{\psi }\otimes \mathtt{path}$ is a constraint that is true on a path if ψ is true somewhere on that path. To express universal constraints, the binary connectives “⇐” and “⇒” are used, which are defined via ⊗ and ¬ as follows: $\mathit{\psi }\Leftarrow \mathit{\varphi }\stackrel{\mathrm{def}}{=}\neg \mathrm{(}\neg \mathit{\psi }\otimes \mathit{\varphi }\mathrm{)}$ and $\mathit{\psi }\Rightarrow \mathit{\varphi }\stackrel{\mathrm{def}}{=}\neg \mathrm{(}\mathit{\psi }\otimes \neg \mathit{\varphi }\mathrm{)}$ . A moment’s reflection should convince the reader that $\mathit{\psi }\Leftarrow \mathit{\varphi }$ means that whenever ϕ occurs then ψ must have occurred just before it and that $\mathit{\psi }\Rightarrow \mathit{\varphi }$ means that whenever ψ occurs then ϕ must occur right after it. Thus, $\mathtt{path}\Rightarrow \mathit{\psi }\Leftarrow \mathtt{path}$ constrains executions to be such that every subpath encountered in the course of the execution satisfies ψ (including subpaths of the form $⟨\mathbf{\text{s}}⟩$ , where $\mathbf{\text{s}}$ is an arbitrary intermediate state).

Executional entailment  The notion of executional entailment is the key semantic concept in CTR that brings the informal notion of execution into the logic. Let $\mathbf{\text{P}}$ be a set of CTR formulas, ϕ is a CTR formula and ${\mathbf{\text{s}}}_0\mathrm{,}{\mathbf{\text{s}}}_1\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{n}}$ is a sequence of database states. Then the statement $$\begin{array}{}\text{(2)}& \mathbf{\text{P}}\mathrm{,}{\mathbf{\text{s}}}_0{\mathbf{\text{s}}}_1\dots {\mathbf{\text{s}}}_{\mathit{n}}\vDash \mathit{\varphi }\end{array}$$ is true if and only if $\mathbf{\text{M}}\mathrm{,}⟨{\mathbf{\text{s}}}_0\mathrm{,}{\mathbf{\text{s}}}_1\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{n}}⟩\vDash \mathit{\varphi }$ (i.e., ϕ is true on the path $⟨{\mathbf{\text{s}}}_0\mathrm{,}{\mathbf{\text{s}}}_1\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{n}}⟩$ in $\mathbf{\text{M}}$ ), for every multi-structure $\mathbf{\text{M}}$ that satisfies $\mathbf{\text{P}}$ .

Related to this is the statement $$\begin{array}{r}\mathbf{\text{P}}\mathrm{,}{\mathbf{\text{s}}}_0\text{ ---}\vDash \mathit{\varphi }\end{array}$$ which are true iff (2) is true for some sequence of database states ${\mathbf{\text{s}}}_0\mathrm{,}{\mathbf{\text{s}}}_1\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{n}}$ .

The aforementioned proof theory for CTR assumes that $\mathbf{\text{P}}$ is a set of concurrent-Horn rules and it manipulates the statements of the form $\mathbf{\text{P}}\mathrm{,}\mathbf{\text{s}}\text{ ---}⊢\mathit{\varphi }$ . It is sound and complete in the sense that there is a proof of $\mathbf{\text{P}}\mathrm{,}{\mathbf{\text{s}}}_0\text{ ---}⊢\mathit{\varphi }$ if and only if $\mathbf{\text{P}}\mathrm{,}{\mathbf{\text{s}}}_0\text{ ---}\vDash \mathit{\varphi }$ is true.

4. Formalizing service contracts in ServLog

This section formally defines the core modeling elements of ServLog. First we define service processes directly in CTR. Section 4.2 then introduces service policies and contract requirements as constraints that can be expressed in CTR. Section 4.3 then defines an important notion, which we call the service contract assumption.

4.1. Modeling service processes

Definition 4.1 (Task).

A task is represented by a predicate. The name of the predicate is the name of that task and the arity specifies the number of arguments that the predicate takes. For notational simplicity, we assume that each predicate name has exactly one arity, so each task is uniquely defined by its name.

In service contract specifications, the actual invocations of tasks are represented by task atoms.

Definition 4.2 (Task atom).

A task atom is a statement of the form $$\begin{array}{c}\mathit{p}\mathrm{(}{\mathit{t}}_1\mathrm{,}\dots \mathrm{,}{\mathit{t}}_{\mathit{n}}\mathrm{)}\hfill \end{array}$$ where p is a task predicate of arity n ( $\mathit{n}⩾0$ ) and ${\mathit{t}}_1\mathrm{,}\dots \mathrm{,}{\mathit{t}}_{\mathit{n}}$ are terms (defined as in first-order logic) that represent the arguments that p takes. The terms representing the arguments of the task are placeholders for data items that the task manipulates (its inputs and outputs).

For brevity, we will often write task atoms as $\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}$ , $\mathit{p}\mathrm{(}\bar{\mathit{U}}\mathrm{)}$ , etc., where $\bar{\mathit{T}}$ , $\bar{\mathit{U}}\mathrm{,}\dots$ stand for the tuples of arguments that the task takes.

When confusion does not arise, the term “task” will refer both to tasks and task atoms.

We distinguish between two main types of task predicates: composite and primitive. Composite task predicates are the ones defined by rules (i.e., they are allowed in the rule heads) and primitive tasks are not allowed in the rule heads. The primitive task predicates are further subdivided into update-tasks, query-tasks, and builtin test tasks. The update task predicates are those used as the primitive updates of CTR, the query tasks are the ones whose predicates are used to represent the facts stored in database states, and the builtin tests use predicates whose truth is independent of the database state. These three categories of predicates are disjoint. The transition conditions on the arcs of service process graphs, which were introduced in Section 2, are also treated in ServLog as tasks: specifically as query tasks or builtin tests – whichever applies in each case.

In this paper, we will be using the builtins “=” (identity), “!=” (distinct values), “>”, “<”, and others, as needed. The identity predicate $\mathit{a}=\mathit{b}$ is true if and only if a and b are the same ground (i.e., variable-free) term and $\mathit{a}!=\mathit{b}$ holds if a and b are distinct ground terms. Clearly, the truth of these predicates is independent of the database state (or of a path) where the predicate is evaluated.

From now on, when talking about CTR goals and rules, we assume that the atomic formulas are task atoms only. In addition, the predicates occurring in the rule heads must correspond to composite tasks only.

Definition 4.3 (Task occurrence).

A task p occurs in a CTR goal Ω if Ω contains a task atom $\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}$ for some  $\bar{\mathit{T}}$ .

Definition 4.4 (Immediate subtask).

Let p and q be a pair of tasks and R be a set of rules. We say that p is an immediate subtask of q with respect to R if and only if R contains a rule of the form $\mathit{q}\mathrm{(}\bar{\mathit{T}}\mathrm{)}\leftarrow \mathrm{\Omega }$ and p occurs in Ω.

Definition 4.5 (Subtasks).

Let p and q be a pair of tasks and R be a set of rules. Then p is a subtask of q with respect to R if and only if p is either an immediate subtask of q or there is an immediate subtask r of q such that p is a subtask of r.

Definition 4.6 (Non-iterative rule).

A rule in R is non-iterative if and only if it has the form $$\begin{array}{c}\mathit{q}\mathrm{(}\bar{\mathit{T}}\mathrm{)}\leftarrow \mathrm{\Omega }\end{array}$$ where q does not occur in Ω and none of the tasks that occur in Ω have q as a subtask.

Here is an example of a non-iterative rule (p and r are assumed to be primitive tasks here): $\mathit{q}\mathrm{(}?\mathit{X}\mathrm{)}\leftarrow \mathit{p}\mathrm{(}?\mathit{X}\mathrm{,}?\mathit{Y}\mathrm{)}\otimes \mathit{r}\mathrm{(}?\mathit{Y}\mathrm{)}$ . As seen in this example, variables in ServLog are represented as symbols prefixed with “?”.

Definition 4.7 (Iterative rule).

A rule $\mathit{q}\mathrm{(}\bar{\mathit{T}}\mathrm{)}\leftarrow \mathrm{\Omega }$ in R is iterative if and only if q either occurs in Ω directly or it is a subtask of a task that occurs in Ω.

Here are examples of iterative rules: $$\begin{array}{l}\begin{array}{cc}\hfill \mathit{q}\mathrm{(}?\mathit{X}\mathrm{)}\leftarrow & \mathrm{(}\mathit{p}\mathrm{(}?\mathit{X}\mathrm{,}?\mathit{Y}\mathrm{)}\otimes \mathit{q}\mathrm{(}?\mathit{Y}\mathrm{)}\otimes \mathit{r}\mathrm{(}?\mathit{Y}\mathrm{,}?\mathit{Z}\mathrm{)}\mathrm{)}\hfill \\ \hfill & \vee \mathit{s}\mathrm{(}?\mathit{Y}\mathrm{)}\hfill \end{array}\\ \mathit{q}\mathrm{(}?\mathit{X}\mathrm{)}\leftarrow \mathit{p}\mathrm{(}?\mathit{X}\mathrm{,}?\mathit{Y}\mathrm{)}\otimes \mathit{q}\mathrm{(}?\mathit{Y}\mathrm{)}\otimes \mathit{q}\mathit{q}\mathrm{(}?\mathit{Y}\mathrm{,}?\mathit{Z}\mathrm{)}\\ \mathit{q}\mathit{q}\mathrm{(}?\mathit{X}\mathrm{)}\leftarrow \mathrm{(}\mathit{p}\mathit{p}\mathrm{(}?\mathit{X}\mathrm{,}?\mathit{Y}\mathrm{)}\otimes \mathit{q}\mathrm{(}?\mathit{Y}\mathrm{)}\mathrm{)}\vee \mathit{t}\mathrm{(}?\mathit{X}\mathrm{)}\end{array}$$

Note that here q and $\mathit{q}\mathit{q}$ are both iterative tasks that are mutually dependent on each other (are subtasks of each other). In practice, however, the most common form of iterative tasks is a loop of the form $$\begin{array}{l}\mathit{q}\mathrm{(}\bar{\mathit{T}}\mathrm{)}\leftarrow \mathrm{\Phi }\otimes \mathit{q}\mathrm{(}\bar{\mathit{U}}\mathrm{)}\\ \mathit{q}\mathrm{(}\bar{\mathit{T}}\mathrm{)}\leftarrow \mathrm{\Psi }\end{array}$$ where Φ and Ψ do not depend on q.

Definition 4.8 (Service process).

A service process is a pair $\mathrm{(}\mathrm{\Omega }\mathrm{,}\mathbf{\text{R}}\mathrm{)}$ , where Ω is a CTR goal and R is a set of iterative and non-iterative rules whose heads are task atoms of the tasks that occur in Ω or are subtasks of these tasks.

Recall that primitive tasks come in three guises: updates, queries, and builtins. Similarly, we classify composite tasks based on the rules that define them. Namely, if a task is defined by at least one iterative rule (i.e. there exists an iterative rule with the task as its head), we call the task iterative; if it is defined only by non-iterative rules then the task is non-iterative.

Equipped with this mechanism for defining service processes in ServLog, one can capture a wide range of control and data flow constructs that often appear in business process languages and notations. For example, the service process introduced in Fig. 2 is represented in ServLog as shown in Fig. 5.

The top-level graph is specified as a CTR goal at the very beginning. The tasks appearing in that goal are defined by the rules that follow. This service process illustrates data flow through variables as well as via a shared database. For example, passing data from process_order_items to book_shipper is done via the underlying database by having process_order_items insert $\mathit{selected}\text{\_}\mathit{item}\mathrm{(}?\mathit{Order}\mathrm{\#}\mathrm{,}?\mathit{Item}\mathrm{)}$ and then querying this data item by the task handle_shippers. In order to fully capture the dataflow, we introduce three additional database query predicates:

producer(?Item,?Producer), which returns a producer for the given item,

itemAvailable(?Order#,?Producer,?Item), which is true if the given item is produced by the given producer and the item is in stock, and

itemUnavailable(?Order#,?Producer,?Item), which is the negation of itemAvailable.

While the set of available producers is relatively static, the relation itemAvailable can be modified by the contact_producer(?Producer,?Item) task. For instance, after contacting the producer an item might become reserved.

Data flow types supported by ServLog are simple yet powerful: tasks can share data through shared variables or through the underlying shared database – the former is standard in classical logic and in logic programming languages, the latter is a feature of CTR. For instance, in the subprocess process_item in Fig. 5, the same data is passed through the shared variables $?\mathit{Order}\mathrm{\#}$ and $?\mathit{Item}$ to the query producer, and also other tasks (e.g., contact_producer). These data come from the task process_order_items and then are passed along to the top-level invocation of process_item. Inside process_item, new data is obtained by the query producer and then is passed to the subtasks contact_producer and inform_client through the shared variable ?Producer.

Fig. 5.

ServLog representation of the service process from Fig. 2.

In Section 2, we explained the nature of primitive updates as “black boxes” whose inner workings are hidden from ServLog’s reasoning mechanism. In Fig. 5, for example, the tasks place_order, select_item, and some others are said to be primitive CTR updates that correspond to primitive tasks in Fig. 2 and their implementation is opaque to the system. However, as explained there, ServLog lets the service logic designer to represent tasks at different levels of abstraction and primitive tasks may be expanded into complex tasks, if desired. Figure 6 illustrates this point using some earlier primitive tasks as an example.

Fig. 6.

Expansion of some primitive updates from Fig. 5.

4.2. Modeling constraints

We now formalize service policies and contract requirements as constraints in ServLog. Note that constraints are not defined directly as CTR formulas (unlike task definitions). The main reason for this is that constraints represent patterns that executions of service processes must follow and specialized language constructs for such patterns make specification of constraints easier to understand. Nevertheless, the constraints of ServLog can be expressed as CTR formulas (see Appendix C), so CTR is indeed used here as a unifying formalism for both service task definition and constraints. Recall that whereas CTR can represent constraints, they are not Concurrent Horn formulas and are therefore not handled by the existing CTR proof theory – the extension of the CTR proof theory to handle constraints is proposed in Section 5.2 and is an important contribution of this paper.

A constraint specifies the rules governing the occurrences of various tasks during the execution of a service. Each occurrence of a task is represented by a pattern, which specifies the task name and various conditions on the arguments with which that task can be invoked during the execution. These conditions can require that certain arguments must be bound to specific values and they can also require that certain arguments must be shared within a task occurrence or across the occurrences of different tasks.

Definition 4.9 (Task pattern).

A task pattern has the form $\mathit{p}\mathrm{(}{\mathit{t}}_1\mathrm{,}\dots \mathrm{,}{\mathit{t}}_{\mathit{n}}\mathrm{)}$ where each ${\mathit{t}}_{\mathit{i}}$ is either a regular ground term (of the kind that may occur in a task atom) or a placeholder. A placeholder is either a named logical variable (which will be designated with the prefix ’_’, e.g., _Ord#) or a don’t care placeholder, denoted by ’_’. Each occurrence of a don’t care placeholder represents a new logical variable that does not occur in other patterns.

We will often need to perform two operations: matching and refinement. The former is the usual matching operator of first-order logic: it is a substitution, θ such that $\mathit{\theta }\mathrm{(}\mathit{pattern}\mathrm{)}=\mathit{task}\text{\_}\mathit{atom}$ . Since $\mathit{task}\text{\_}\mathit{atom}$ is ground, θ will normally be a ground substitution. In this case we will say that the pattern and the ground task match. Note that different occurrences of ’_’ may be mapped by θ to different constants, since such occurrences represent different logical variables. Refinement is defined next.

Definition 4.10 (Refinement).

The refinement operation takes a ground task atom and a pair of task patterns and yields another task pattern as follows: $$\begin{array}{ll}\hfill & \mathtt{\text{refine}}\mathrm{(}\mathit{out}\text{\_}\mathit{pattern};\\ \hfill & \phantom{\mathtt{\text{refine}}\mathrm{(}}\mathit{in}\text{\_}\mathit{ground}\text{\_}\mathit{task}\mathrm{,}\mathit{in}\text{\_}\mathit{pattern}\mathrm{)}\\ \hfill & =\mathit{refined}\text{\_}\mathit{pattern}\end{array}$$ Here the arguments in_ground_task and in_pattern must have the same task name and in_ground_task must match in_pattern. The task-pattern out_pattern may have a different task name. The result of the operation, refined_pattern, is defined as follows: Let θ be the substitution that matches in_pattern against in_ground_task. If out_pattern has variables other than those in in_pattern, θ can map them to anything (to some other variable or constant). Then $$\begin{array}{c}\mathit{refined}\text{\_}\mathit{pattern}=\mathit{\theta }\mathrm{(}\mathit{out}\text{\_}\mathit{pattern}\mathrm{)}\end{array}$$

One can verify by direct inspection that the task atom p(2,1,abc,cde,13,cde,13,5) matches the pattern p(_,1,abc,_foo,_bar,_foo,_bar,_), that $$\begin{array}{ll}\hfill & \mathtt{refine}\mathrm{(}\mathtt{p}\mathrm{(}\text{\_}\mathtt{ff}\mathrm{,}\mathtt{5}\mathrm{,}\text{\_}\mathrm{)};\\ \hfill & \phantom{\mathtt{\text{refine(}}}\mathtt{p}\mathrm{(}\mathtt{1}\mathrm{,}\mathtt{2}\mathrm{,}\mathtt{3}\mathrm{)}\mathrm{,}\mathtt{p}\mathrm{(}\text{\_}\mathrm{,}\text{\_}\mathtt{ff}\mathrm{,}\mathtt{3}\mathrm{)}\mathrm{)}\\ \hfill & =\mathtt{p}\mathrm{(}\mathtt{2}\mathrm{,}\mathtt{5}\mathrm{,}\text{\_}\mathrm{)}\mathrm{,}\end{array}$$ and that $$\begin{array}{ll}\hfill & \mathtt{refine}\mathrm{(}\mathtt{q}\mathrm{(}\text{\_}\mathtt{f}\mathrm{,}\mathtt{5}\mathrm{,}\text{\_}\mathtt{f}\mathrm{,}\text{\_}\mathrm{,}\text{\_}\mathtt{h}\mathrm{)};\\ \hfill & \phantom{\mathtt{\text{refine(}}}\mathtt{p}\mathrm{(}\mathtt{1}\mathrm{,}\mathtt{2}\mathrm{,}\mathtt{2}\mathrm{,}\mathtt{3}\mathrm{)}\mathrm{,}\mathtt{p}\mathrm{(}\text{\_}\mathtt{g}\mathrm{,}\text{\_}\mathtt{f}\mathrm{,}\text{\_}\mathtt{f}\mathrm{,}\mathtt{3}\mathrm{)}\mathrm{)}\\ \hfill & =\mathtt{q}\mathrm{(}\mathtt{2}\mathrm{,}\mathtt{5}\mathrm{,}\mathtt{2}\mathrm{,}\text{\_}\mathrm{,}\text{\_}\mathtt{h}\mathrm{)}.\end{array}$$ The last example also illustrates the situation where in_pattern has named placeholders that do not occur in out_pattern; the number of arguments in the input and output patterns can also differ.

Definition 4.11 (Constraints).

In this definition, we will use $\bar{\mathit{t}}$ , $\bar{\mathit{u}}$ , etc., to represent tuples that include placeholders as some of the arguments in task patterns. The uppercase symbols $\bar{\mathit{T}}$ , $\bar{\mathit{U}}$ , etc., will denote tuples of arguments in task atoms (i.e., they do not contain placeholders). The task names p, q, r, and the task patterns mentioned in the constraints, below, do not need to be distinct.

The set $\mathcal{C}\mathcal{ONSTR}$ of constraints supported by ServLog is formally defined as follows. For each constraint we first give its syntax followed by a brief informal explanation and then provide a formal semantic definition. Appendix C provides alternative representation of these constraints as CTR formulas.

Existence constraints:

• ${\mathtt{atleast}}_{\mathit{n}}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\mathrm{)}$ : task p must execute at least n times (n ⩾ 1).

  Formally, an execution $⟨{\mathbf{\text{s}}}_1\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{m}}⟩$ satisfies this constraint if and only if there are ground task atoms $\mathit{p}\mathrm{(}\overline{{\mathit{T}}_1}\mathrm{)}\mathrm{,}\dots \mathrm{,}\mathit{p}\mathrm{(}\overline{{\mathit{T}}_{\mathit{n}}}\mathrm{)}$ that executed at some states ${\mathbf{\text{s}}}_{{\mathit{i}}_1}\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{{\mathit{i}}_{\mathit{n}}}$ (i.e., ${\mathbf{\text{s}}}_{{\mathit{i}}_1}\stackrel{\mathit{p}\mathrm{(}\overline{{\mathit{T}}_1}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{{\mathit{i}}_1+1}\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{{\mathit{i}}_{\mathit{n}}}\stackrel{\mathit{p}\mathrm{(}\overline{{\mathit{T}}_{\mathit{n}}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{{\mathit{i}}_{\mathit{n}}+1}$ ) such that $\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}$ matches $\mathit{p}\mathrm{(}\overline{{\mathit{T}}_1}\mathrm{)}$ , $\mathit{p}\mathrm{(}\overline{{\mathit{T}}_2}\mathrm{)}\mathrm{,}\dots \mathrm{,}\mathit{p}\mathrm{(}\overline{{\mathit{T}}_{\mathit{n}}}\mathrm{)}$ .13

  ¹³

  The notation $\mathit{s}\stackrel{\mathit{p}}{⟶}{\mathit{s}}^{\prime }$ was introduced in (1) in Section 3. Recall that since $\mathit{p}\mathrm{(}\overline{{\mathit{T}}_1}\mathrm{)}\mathrm{,}\dots \mathrm{,}\mathit{p}\mathrm{(}\overline{{\mathit{T}}_{\mathit{n}}}\mathrm{)}$ cause state transitions, they are primitive update tasks.

• $\mathtt{absence}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\mathrm{)}$ : task p must not execute.

  Formally, an execution $⟨{\mathbf{\text{s}}}_1\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{m}}⟩$ satisfies this constraint if and only if there is no state ${\mathbf{\text{s}}}_{\mathit{i}}$ in that execution such that ${\mathbf{\text{s}}}_{\mathit{i}}\stackrel{\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{\mathit{i}+1}$ and $\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}$ matches $\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}$ .

• ${\mathtt{exactly}}_{\mathit{n}}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\mathrm{)}$ : task p must execute exactly n times (n ⩾ 1).

  An execution $⟨{\mathbf{\text{s}}}_1\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{m}}⟩$ satisfies this constraint if and only if it satisfies ${\mathtt{atleast}}_{\mathit{n}}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\mathrm{)}$ but not ${\mathtt{atleast}}_{\mathit{n}+1}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\mathrm{)}$ .

Serial constraints:

• $\mathtt{after}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}⇢\mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)}\mathrm{)}$ : whenever p executes, q must execute after it. Task q is not required to execute immediately after p, and several other instances of p might execute before q actually does.

  Formally, an execution $⟨{\mathbf{\text{s}}}_1\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{m}}⟩$ satisfies this constraint if and only if whenever there is a state ${\mathbf{\text{s}}}_{\mathit{i}}$ in this execution, such that ${\mathbf{\text{s}}}_{\mathit{i}}\stackrel{\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{\mathit{i}+1}$ and $\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}$ matches $\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}$ , there must be a state ${\mathbf{\text{s}}}_{\mathit{j}}$ in that same execution such that $\mathit{j}⩾\mathit{i}+1$ , ${\mathbf{\text{s}}}_{\mathit{j}}\stackrel{\mathit{q}\mathrm{(}\bar{\mathit{U}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{\mathit{j}+1}$ , and $\mathtt{\text{refine}}\mathrm{(}\mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)};\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}\mathrm{,}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\mathrm{)}$ matches $\mathit{q}\mathrm{(}\bar{\mathit{U}}\mathrm{)}$ .

  For instance, if the above constraint has the form $\mathtt{after}\mathrm{(}\mathit{p}\mathrm{(}\text{\_}\mathit{foo}\mathrm{,}\text{\_}\mathrm{)}⇢\mathit{q}\mathrm{(}\text{\_}\mathrm{,}\text{\_}\mathit{foo}\mathrm{)}\mathrm{)}$ then the sequence $\mathit{p}\mathrm{(}\mathit{a}\mathrm{,}1\mathrm{)}\mathrm{,}\mathit{q}\mathrm{(}2\mathrm{,}\mathit{a}\mathrm{)}$ is a valid execution, but $\mathit{p}\mathrm{(}\mathit{a}\mathrm{,}1\mathrm{)}\mathrm{,}\mathit{q}\mathrm{(}2\mathrm{,}\mathit{b}\mathrm{)}$ is not.

• $\mathtt{before}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}⇠\mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)}\mathrm{)}$ : whenever q executes, it must be preceded by an execution of p. Task p does not have to execute immediately prior to q.

  An execution $⟨{\mathbf{\text{s}}}_1\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{m}}⟩$ is said to satisfy this constraint if and only if whenever there is a state ${\mathbf{\text{s}}}_{\mathit{i}}$ in this execution such that ${\mathbf{\text{s}}}_{\mathit{i}}\stackrel{\mathit{q}\mathrm{(}\bar{\mathit{U}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{\mathit{i}+1}$ and $\mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)}$ matches $\mathit{q}\mathrm{(}\bar{\mathit{U}}\mathrm{)}$ , there must be a state ${\mathbf{\text{s}}}_{\mathit{j}}$ in that same execution such that $\mathit{j}⩽\mathit{i}-1$ , ${\mathbf{\text{s}}}_{\mathit{j}}\stackrel{\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{\mathit{j}+1}$ , and $\mathtt{\text{refine}}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)};\mathit{q}\mathrm{(}\bar{\mathit{U}}\mathrm{)}\mathrm{,}\mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)}\mathrm{)}$ matches $\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}$ .

  For instance, if the constraint is $$\begin{array}{c}\mathtt{before}\mathrm{(}\mathit{p}\mathrm{(}\text{\_}\mathit{foo}\mathrm{,}\text{\_}\mathrm{)}⇠\mathit{q}\mathrm{(}\text{\_}\mathrm{,}\text{\_}\mathit{foo}\mathrm{)}\mathrm{)}\end{array}$$ then the sequence $\mathit{p}\mathrm{(}\mathit{a}\mathrm{,}1\mathrm{)}\mathrm{,}\mathit{q}\mathrm{(}2\mathrm{,}\mathit{a}\mathrm{)}$ is a valid execution, but $\mathit{p}\mathrm{(}\mathit{a}\mathrm{,}1\mathrm{)}\mathrm{,}\mathit{q}\mathrm{(}2\mathrm{,}\mathit{b}\mathrm{)}$ is not.

• : if task p executes then task q cannot execute in the future.

  Formally, an execution $⟨{\mathbf{\text{s}}}_1\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{m}}⟩$ satisfies this constraint if and only if whenever there is a state ${\mathbf{\text{s}}}_{\mathit{i}}$ in this execution such that ${\mathbf{\text{s}}}_{\mathit{i}}\stackrel{\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{\mathit{i}+1}$ and $\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}$ matches $\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}$ , there is no state ${\mathbf{\text{s}}}_{\mathit{j}}$ in that execution such that $\mathit{j}\mathrm{>}\mathit{i}$ , ${\mathbf{\text{s}}}_{\mathit{j}}\stackrel{\mathit{q}\mathrm{(}\bar{\mathit{U}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{\mathit{j}+1}$ , and $\mathtt{\text{refine}}\mathrm{(}\mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)};\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}\mathrm{,}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\mathrm{)}$ matches $\mathit{q}\mathrm{(}\bar{\mathit{U}}\mathrm{)}$ .

• $\mathtt{between}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}⇢\mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)}⇠\mathit{r}\mathrm{(}\bar{\mathit{v}}\mathrm{)}\mathrm{)}$ : task q must execute between any two executions of p and r. That is, after an execution of p, any subsequent execution of r has to wait until q is executed.

  An execution $⟨{\mathbf{\text{s}}}_1\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{m}}⟩$ satisfies this constraint if and only if whenever there are states ${\mathbf{\text{s}}}_{\mathit{i}}$ , ${\mathbf{\text{s}}}_{\mathit{k}}$ ( $\mathit{k}\mathrm{>}\mathit{i}+1$ ) such that ${\mathbf{\text{s}}}_{\mathit{i}}\stackrel{\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{\mathit{i}+1}$ , ${\mathbf{\text{s}}}_{\mathit{k}}\stackrel{\mathit{r}\mathrm{(}\bar{\mathit{V}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{\mathit{k}+1}$ , $\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}$ matches $\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}$ , and $\mathit{r}\mathrm{(}\bar{\mathit{v}}\mathrm{)}$ matches $\mathit{r}\mathrm{(}\bar{\mathit{V}}\mathrm{)}$ , then there must be a state ${\mathbf{\text{s}}}_{\mathit{j}}$ such that $\mathit{i}\mathrm{<}\mathit{j}\mathrm{<}\mathit{k}$ , ${\mathbf{\text{s}}}_{\mathit{j}}\stackrel{\mathit{q}\mathrm{(}\bar{\mathit{U}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{\mathit{j}+1}$ , and both $\mathtt{\text{refine}}\mathrm{(}\mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)};\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}\mathrm{,}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\mathrm{)}$ and $\mathtt{\text{refine}}\mathrm{(}\mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)};\mathit{r}\mathrm{(}\bar{\mathit{V}}\mathrm{)}\mathrm{,}\mathit{r}\mathrm{(}\bar{\mathit{v}}\mathrm{)}\mathrm{)}$ match $\mathit{q}\mathrm{(}\bar{\mathit{U}}\mathrm{)}$ .

• : task q must not execute between any pair of executions of p and r. Thus, if q executes after p, no future execution of r is possible.

  An execution $⟨{\mathbf{\text{s}}}_1\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{m}}⟩$ satisfies this constraint if and only if whenever there are states ${\mathbf{\text{s}}}_{\mathit{i}}$ , ${\mathbf{\text{s}}}_{\mathit{k}}$ ( $\mathit{k}\mathrm{>}\mathit{i}+1$ ) such that ${\mathbf{\text{s}}}_{\mathit{i}}\stackrel{\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{\mathit{i}+1}$ , ${\mathbf{\text{s}}}_{\mathit{k}}\stackrel{\mathit{r}\mathrm{(}\bar{\mathit{V}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{\mathit{k}+1}$ , $\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}$ matches $\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}$ , and $\mathit{r}\mathrm{(}\bar{\mathit{v}}\mathrm{)}$ matches $\mathit{r}\mathrm{(}\bar{\mathit{V}}\mathrm{)}$ , then there is no state ${\mathbf{\text{s}}}_{\mathit{j}}$ such that $\mathit{i}\mathrm{<}\mathit{j}\mathrm{<}\mathit{k}$ , ${\mathbf{\text{s}}}_{\mathit{j}}\stackrel{\mathit{q}\mathrm{(}\bar{\mathit{U}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{\mathit{j}+1}$ , and both $\mathtt{\text{refine}}\mathrm{(}\mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)};\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}\mathrm{,}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\mathrm{)}$ and $\mathtt{\text{refine}}\mathrm{(}\mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)};\mathit{r}\mathrm{(}\bar{\mathit{V}}\mathrm{)}\mathrm{,}\mathit{r}\mathrm{(}\bar{\mathit{v}}\mathrm{)}\mathrm{)}$ match $\mathit{q}\mathrm{(}\bar{\mathit{U}}\mathrm{)}$ .

Immediate serial constraints:

• $\mathtt{right}\text{\_}\mathtt{after}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\to \mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)}\mathrm{)}$ : whenever p executes, q must execute immediately after it.

  Formally, an execution $⟨{\mathbf{\text{s}}}_1\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{m}}⟩$ satisfies this constraint if and only if whenever there is a state ${\mathbf{\text{s}}}_{\mathit{i}}$ in this execution such that ${\mathbf{\text{s}}}_{\mathit{i}}\stackrel{\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{\mathit{i}+1}$ and $\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}$ matches $\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}$ , then ${\mathbf{\text{s}}}_{\mathit{i}+1}\stackrel{\mathit{q}\mathrm{(}\bar{\mathit{U}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{\mathit{i}+2}$ must hold and $\mathtt{\text{refine}}\mathrm{(}\mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)};\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}\mathrm{,}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\mathrm{)}$ must match $\mathit{q}\mathrm{(}\bar{\mathit{U}}\mathrm{)}$ .

• $\mathtt{right}\text{\_}\mathtt{before}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\leftarrow \mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)}\mathrm{)}$ : whenever q executes, p must have been executed immediately before it.

  Formally, an execution $⟨{\mathbf{\text{s}}}_1\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{m}}⟩$ satisfies this constraint if and only if whenever there is a state ${\mathbf{\text{s}}}_{\mathit{i}}$ in this execution such that ${\mathbf{\text{s}}}_{\mathit{i}}\stackrel{\mathit{q}\mathrm{(}\bar{\mathit{U}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{\mathit{i}+1}$ and $\mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)}$ matches $\mathit{q}\mathrm{(}\bar{\mathit{U}}\mathrm{)}$ , then ${\mathbf{\text{s}}}_{\mathit{i}-1}\stackrel{\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{\mathit{i}}$ must hold and $\mathtt{\text{refine}}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)};\mathit{q}\mathrm{(}\bar{\mathit{U}}\mathrm{)}\mathrm{,}\mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)}\mathrm{)}$ must match $\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}$ .

• $\mathtt{not}\text{\_}\mathtt{right}\text{\_}\mathtt{after}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\nrightarrow \mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)}\mathrm{)}$ : whenever p and q execute, q must not execute immediately after p. That is, after p there must be an execution of a task other than q before q is allowed again.

  An execution $⟨{\mathbf{\text{s}}}_1\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{m}}⟩$ is said to satisfy this constraint if and only if whenever there is a state ${\mathbf{\text{s}}}_{\mathit{i}}$ in this execution such that ${\mathbf{\text{s}}}_{\mathit{i}}\stackrel{\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{\mathit{i}+1}$ , where $\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}$ matches $\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}$ , and ${\mathbf{\text{s}}}_{\mathit{i}+1}\stackrel{\mathit{r}\mathrm{(}\bar{\mathit{U}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{\mathit{i}+2}$ for some $\mathit{r}\mathrm{(}\bar{\mathit{U}}\mathrm{)}$ , then $\mathtt{refine}\mathrm{(}\mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)}\mathrm{,}\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}\mathrm{,}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\mathrm{)}$ must not match $\mathit{r}\mathrm{(}\bar{\mathit{U}}\mathrm{)}$ .

Composite constraints: If ${\mathit{C}}_1\mathrm{,}{\mathit{C}}_2\in \mathcal{C}\mathcal{ONSTR}$ then so are ${\mathit{C}}_1\wedge {\mathit{C}}_2$ (a conjunctive constraint) and ${\mathit{C}}_1\vee {\mathit{C}}_2$ (a disjunctive constraint).

Nothing else is in $\mathcal{C}\mathcal{ONSTR}$ .

Note the use of different arrows between the arguments in some of the constraints. The convention here is that the task at the tail of the arrow represents the condition of the constraint (if or whenever the task executes) and the task at the head of the arrow indicates the effect of the constraint (the task must or must not execute in a given relationship to the task at the tail of the arrow). We use strong arrows to indicate immediacy (execution must take place right before or after) and dashed arrows indicate that immediacy is not required. Slashed arrows indicate negative relationships (e.g., the task in the head must not execute). Note also that the negation of $\mathtt{right}\text{\_}\mathtt{before}$ can be defined as follows: $$\begin{array}{l}\mathtt{\text{not\_right\_before}}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\nleftarrow \mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)}\mathrm{)}\\ \equiv \mathtt{not}\text{\_}\mathtt{right}\text{\_}\mathtt{after}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\nrightarrow \mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)}\mathrm{)}.\end{array}$$

The following is an example of a legal constraint in $\mathcal{C}\mathcal{ONSTR}$ : $$\begin{array}{l}{\mathtt{atleast}}_2\mathrm{(}\mathit{p}\mathrm{(}\text{\_}\mathit{X}\mathrm{,}1\mathrm{,}\text{\_}\mathit{X}\mathrm{)}\mathrm{)}\\ \wedge {\mathtt{exactly}}_3\mathrm{(}\mathit{q}\mathrm{(}\text{\_}\mathrm{,}\text{\_}\mathrm{,}\text{\_}\mathrm{)}\mathrm{)}\\ \wedge \mathtt{right}\text{\_}\mathtt{after}\mathrm{(}\mathit{p}\mathrm{(}\text{\_}\mathit{X}\mathrm{,}\text{\_}\mathrm{,}\text{\_}\mathrm{)}\to \mathit{r}\mathrm{(}\text{\_}\mathrm{,}\text{\_}\mathit{X}\mathrm{)}\mathrm{)}\end{array}$$

The constraint ${\mathtt{atleast}}_2\mathrm{(}\mathit{p}\mathrm{(}\text{\_}\mathit{X}\mathrm{,}1\mathrm{,}\text{\_}\mathit{X}\mathrm{)}\mathrm{)}$ requires that p executes at least twice and arguments 1 and 3 have the same value in each execution, while the second argument is the integer 1. In the constraint $\mathtt{right}\text{\_}\mathtt{after}\mathrm{(}\mathit{p}\mathrm{(}\text{\_}\mathit{X}\mathrm{,}\text{\_}\mathrm{,}\text{\_}\mathrm{)}\to \mathit{r}\mathrm{(}\text{\_}\mathrm{,}\text{\_}\mathit{X}\mathrm{)}\mathrm{)}$ , the placeholder $\text{\_}\mathit{X}$ is shared between p and r. This means that whenever p is executed, r must follow immediately and r’s second argument must be the same as the first argument in p.

The constraints from Fig. 3 can now be represented in ServLog, as depicted in Fig. 7.

Fig. 7.

Representation of constraints from Fig. 3.

Many other types of constraints can be naturally expressed in $\mathcal{C}\mathcal{ONSTR}$ , as shown below:

• ${\mathtt{\text{atmost}}}_{\mathit{n}}\mathrm{(}\mathit{p}\mathrm{(}\text{\_}\mathrm{,}1\mathrm{)}\mathrm{)}$ – task p can execute at most n times and each time the second argument must be 1. This constraint was defined in item 1 above.

• $\mathtt{absence}\mathrm{(}\mathit{p}\mathrm{(}\text{\_}\mathrm{,}4\mathrm{)}\mathrm{)}\vee {\mathtt{atleast}}_1\mathrm{(}\mathit{q}\mathrm{(}2\mathrm{,}\text{\_}\mathrm{,}3\mathrm{)}\mathrm{)}$ – if p is executed with its second argument 4, then q must also execute (before or after p) and its first and last arguments must be 2 and 3 respectively.

• $\mathrm{(}\mathtt{absence}\mathrm{(}\mathit{p}\mathrm{(}\mathrm{)}\mathrm{)}\vee {\mathtt{atleast}}_1\mathrm{(}\mathit{q}\mathrm{(}\mathrm{)}\mathrm{)}\mathrm{)}\wedge \mathrm{(}\mathtt{absence}\mathrm{(}\mathit{q}\mathrm{(}\mathrm{)}\mathrm{)}\vee {\mathtt{atleast}}_1\mathrm{(}\mathit{p}\mathrm{(}\mathrm{)}\mathrm{)}\mathrm{)}$ – if p is executed, then q must also be executed, and vice versa.

• $\mathtt{after}\mathrm{(}\mathit{p}\mathrm{(}\text{\_}\mathit{X}\mathrm{)}⇢\mathit{q}\mathrm{(}\text{\_}\mathit{X}\mathrm{)}\mathrm{)}\wedge \mathtt{before}\mathrm{(}\mathit{p}\mathrm{(}\text{\_}\mathit{X}\mathrm{)}⇠\mathit{q}\mathrm{(}\text{\_}\mathit{X}\mathrm{)}\mathrm{)}$ – every occurrence of task p must be followed by an occurrence of task q with the same argument and there must be an occurrence of p before every occurrence of q and their arguments must be the same.

• $\mathtt{absence}\mathrm{(}\mathit{p}\mathrm{(}\text{\_}\mathrm{)}\mathrm{)}\vee \mathtt{between}\mathrm{(}\mathit{p}\mathrm{(}\text{\_}\mathit{X}\mathrm{)}⇢\mathit{q}\mathrm{(}\text{\_}\mathit{X}\mathrm{)}⇠\mathit{p}\mathrm{(}\text{\_}\mathrm{)}\mathrm{)}$ – if task p is executed then q must execute after it, with the same argument, and before that q there can be no other p.

• $\mathtt{absence}\mathrm{(}\mathit{q}\mathrm{(}\text{\_}\mathrm{)}\mathrm{)}\vee \mathrm{(}\mathtt{before}\mathrm{(}\mathit{p}\mathrm{(}\text{\_}\mathrm{)}⇠\mathit{q}\mathrm{(}\text{\_}\mathrm{)}\mathrm{)}\wedge \mathtt{between}\mathrm{(}\mathit{q}\mathrm{(}\text{\_}\mathrm{)}⇢\mathit{p}\mathrm{(}\text{\_}\mathrm{)}⇠\mathit{q}\mathrm{(}\text{\_}\mathrm{)}\mathrm{)}\mathrm{)}$ – if task q is executed, it has to be preceded by an occurrence of p. The next instance of q can execute only after another occurrence p.

• $\mathtt{between}\mathrm{(}\mathit{p}\mathrm{(}\text{\_}\mathit{X}\mathrm{)}⇢\mathit{q}\mathrm{(}\text{\_}\mathit{X}\mathrm{)}⇠\mathit{p}\mathrm{(}\text{\_}\mathit{X}\mathrm{)}\mathrm{)}\wedge \mathtt{between}\mathrm{(}\mathit{q}\mathrm{(}\text{\_}\mathit{X}\mathrm{)}⇢\mathit{p}\mathrm{(}\text{\_}\mathit{X}\mathrm{)}⇠\mathit{q}\mathrm{(}\text{\_}\mathit{X}\mathrm{)}\mathrm{)}$ – tasks p and q must alternate when they execute with the same argument.

• $\mathtt{right}\text{\_}\mathtt{after}\mathrm{(}\mathit{p}\mathrm{(}\text{\_}\mathrm{)}\to \mathit{q}\mathrm{(}\text{\_}\mathrm{)}\mathrm{)}\wedge \mathtt{right}\text{\_}\mathtt{before}\mathrm{(}\mathit{p}\mathrm{(}\text{\_}\mathrm{)}\leftarrow \mathit{q}\mathrm{(}\text{\_}\mathrm{)}\mathrm{)}$ – executions of p and q must be next to each other with no intervening tasks in-between.

• $\mathtt{absence}\mathrm{(}\mathit{p}\mathrm{(}\text{\_}\mathrm{)}\mathrm{)}\vee \mathtt{absence}\mathrm{(}\mathit{q}\mathrm{(}\text{\_}\mathrm{)}\mathrm{)}$ – it is not possible for p and q to execute in the same service process run.

• – q must not execute between any two executions of p with the same arguments, and p must not execute between any two executions of q with the same arguments.

4.3. The service contract assumption

We now introduce modeling assumptions, which tighten the form of the constraints and tasks that are allowed in service processes. These assumptions do not limit the modeling power of the language in the sense that any service process can be represented by another process that satisfies these assumptions. However, these assumptions greatly simplify the reasoning system of Section 5.

Definition 4.12 (Service contract assumption).

A service process G and a set of constraints $\mathcal{C}$ satisfy the service contract assumption if and only if the set of constraints $\mathcal{C}$ is based on primitive update tasks and the primitive update tasks of G satisfy the independence assumption.

The last two notions in this definition are spelled out in Definitions 4.13 and 4.14 below. Also recall that a primitive task is one that is not defined by a rule and a primitive update task is just a primitive CTR update.

Definition 4.13 (Constraints based on primitive update tasks).

A set of constraints is based on primitive update tasks if and only if all tasks appearing in the constraints are primitive update tasks.

This restriction does not limit the modeling power of the language, since one can always instrument composite tasks in such a way that the resulting set of constraints will be based on primitive update tasks. More specifically, one can insert “bounding” primitive update tasks at various locations in the definition of composite tasks, and then transform constraints on composite tasks into constraints on those bounding primitive update tasks. These bounding tasks are defined as no-ops and their only purpose is to capture the various stages in the life cycle of a task. Examples include the beginning and end of a task, the beginning and end of an iteration, and so on.

The rationale behind restricting constraints to primitive update tasks is that specifying constraints directly over composite tasks can be highly ambiguous. For instance, what should the sentence “task b must start after task a” mean exactly? Should b start after a begins or after a ends? Similar ambiguity exists with other constraints, such as before and between constraints. Requiring that constraints are based on primitive update tasks avoids ambiguity and complications without limiting the modeling power.

The following example illustrates the process of inserting bounding tasks to delineate the beginning and the end of a composite task:

Every non-iterative composite task of the form $\mathit{p}\leftarrow \mathrm{\Omega }$ can be changed to: $$\begin{array}{c}\mathit{p}\leftarrow {\mathit{p}}_{\mathit{start}}\otimes \mathrm{\Omega }\otimes {\mathit{p}}_{\mathit{end}}\end{array}$$

Every iterative composite task, for example, of the form $\mathit{p}\leftarrow \mathrm{(}\mathrm{\Phi }\otimes \mathit{p}\mathrm{)}\vee \mathrm{\Psi }$ , can be changed to: $$\begin{array}{rcl}\mathit{p}& \leftarrow & \mathrm{(}{\mathit{p}}_{\mathit{start}}\otimes \mathrm{\Phi }\otimes \mathit{p}\otimes {\mathit{p}}_{\mathit{end}}\mathrm{)}\\ & & \vee \mathrm{(}{\mathit{p}}_{\mathit{start}}\otimes \mathrm{\Psi }\otimes {\mathit{p}}_{\mathit{end}}\mathrm{)}\end{array}$$

In fact, there are many other ways to insert bounding tasks, which would enable many more kinds of constraints. For instance, $$\begin{array}{c}\mathit{p}\leftarrow {\mathit{p}}_{\mathit{start}}\otimes {\mathrm{\Phi }}_{\mathit{start}}\otimes \mathrm{\Phi }\otimes {\mathrm{\Phi }}_{\mathit{end}}\otimes \mathit{p}\otimes {\mathit{p}}_{\mathit{end}}\end{array}$$ These bounding tasks are regular primitive updates that insert unique tokens every time they execute. For example, ${\mathit{p}}_{\mathit{start}}$ might insert $\mathit{token}\mathrm{(}{\mathit{p}}_{\mathit{start}}\mathrm{,}0\mathrm{)}$ , $\mathit{token}\mathrm{(}{\mathit{p}}_{\mathit{start}}\mathrm{,}1\mathrm{)}$ , $\mathit{token}\mathrm{(}{\mathit{p}}_{\mathit{start}}\mathrm{,}2\mathrm{)}$ , and so on, on each successive execution.

A constraint such as $\mathtt{after}\mathrm{(}\mathit{p}⇢\mathit{q}\mathrm{)}$ , where p and q are composite tasks, can now be interpreted as $\mathtt{after}$ ( ${\mathit{p}}_{\mathit{start}}⇢{\mathit{q}}_{\mathit{start}}$ ), or $\mathtt{after}$ ( ${\mathit{p}}_{\mathit{end}}⇢{\mathit{q}}_{\mathit{start}}$ ), or $\mathtt{after}$ ( ${\mathit{p}}_{\mathit{start}}⇢{\mathit{q}}_{\mathit{start}}$ ) ∧ $\mathtt{after}$ ( ${\mathit{p}}_{\mathit{end}}⇢{\mathit{q}}_{\mathit{end}}$ ). By exposing the bounding primitive subtasks, ServLog enables many kinds of constraints that cannot be specified on composite tasks directly. For instance, the constraint $\mathtt{before}$ ( ${\mathit{p}}_{\mathit{start}}⇠{\mathit{q}}_{\mathit{end}}$ ) or the constraint $\mathtt{between}$ ( ${\mathit{p}}_{\mathit{start}}⇢{\mathit{q}}_{\mathit{start}}⇠{\mathit{p}}_{\mathit{end}}$ ).

An important benefit of the use of bounding start- and end-tasks is that they enable easy specification of pre- and post-conditions for any task in a service and even for the entire service. For instance, if ${\mathit{serv}}_{\mathit{start}}$ and ${\mathit{serv}}_{\mathit{end}}$ are bounding primitive tasks for the entire service and precond is a query then $\mathtt{right}\text{\_}\mathtt{before}\mathrm{(}\mathit{precond}\leftarrow {\mathit{serv}}_{\mathit{start}}\mathrm{)}$ establishes precond as a precondition for the entire service. Likewise, $\mathtt{right}\text{\_}\mathtt{after}\mathrm{(}{\mathit{serv}}_{\mathit{end}}\to \mathit{postcond}\mathrm{)}$ establishes postcond as a post-condition for the service. A service can have several pre- and post-conditions and some of these constraints can belong to client requirements while others can be specified as part of the service policy.

Definition 4.14 (Independence assumption).

Two primitive update tasks are said to be independent if and only if they are represented by disjoint binary relations over database states.

A service process satisfies the independence assumption if and only if all its primitive update tasks are independent of each other.

Independence implies that any transition between a pair of states is caused by precisely one primitive update task, and no other task can cause that transition.

Any set of primitive update tasks can be instrumented so that the tasks would become independent. For example, each primitive update task, t, can be made to insert a unique token every time it executes. Specifically, t might insert $\mathit{token}\mathrm{(}\mathit{t}\mathrm{,}0\mathrm{)}$ on the first execution and then $\mathit{token}\mathrm{(}\mathit{t}\mathrm{,}1\mathrm{)}$ , $\mathit{token}\mathrm{(}\mathit{t}\mathrm{,}2\mathrm{)}$ , etc., on subsequent executions. As a result, any transition between any pair of states would be possible by at most one primitive update task.

Without the independence assumption it is hard to come up with an effective algorithm for checking satisfaction of constraints by service executions, and it is hard to develop a simple enough proof theory for finding service executions that satisfy such constraints. To see this, suppose that the independence assumption is not satisfied and there are two distinct primitive update tasks such that $\mathit{s}\stackrel{\mathit{p}}{⟶}{\mathit{s}}^{\prime }$ and $\mathit{s}\stackrel{\mathit{q}}{⟶}{\mathit{s}}^{\prime }$ hold. Suppose that we are now trying to execute p at state s. In the presence of constraints such as $\mathtt{before}\mathrm{(}\mathit{r}⇠\mathit{q}\mathrm{)}$ , $\mathtt{absence}\mathrm{(}\mathit{q}\mathrm{)}$ , and the like, it would be hard to determine whether p can be executed, since one must first determine if execution of p amounts to execution of another, prohibited task, such as q, in this example.

5. Reasoning about contracts in ServLog

We begin with an example that shows how service contracting and contract execution are intended to work. The example illustrates most of the aspects of service modeling introduced in Section 4: service processes (control and data flows), client contract requirements, and service policies. The last two are represented via constraints. Section 5.2 formalizes the decision procedure as an extension to the proof procedure of the original CTR.

5.1. Informal example

For simplicity, the example uses propositional tasks only, but the proof procedure in Section 5.2 is designed to work for the more general case where tasks have arguments. For concreteness and to illustrate the interactive aspect of our model, we assume the following division among the tasks involved:

• Service tasks: a, f, g

• Client tasks: d, e, h

Service process:

Process formula: $$\begin{array}{}\text{(3)}& \mathit{a}\otimes \mathrm{(}\mathit{B}\mid \mathit{C}\mathrm{)}\otimes \mathrm{(}\mathit{g}\vee \mathit{h}\mathrm{)}\end{array}$$

Rules: $$\begin{array}{l}\mathit{B}\leftarrow \mathit{d}\vee \mathit{e}\\ \mathit{C}\leftarrow \mathrm{(}\mathit{f}\otimes \mathit{C}\mathrm{)}\vee \mathtt{\text{state}}\end{array}$$

Client contract requirements: $$\begin{array}{}\text{(4)}& \mathtt{absence}\mathrm{(}\mathit{e}\mathrm{)}\wedge {\mathtt{atleast}}_2\mathrm{(}\mathit{f}\mathrm{)}\end{array}$$

Service policy: $$\begin{array}{}\text{(5)}& \mathtt{after}\mathrm{(}\mathit{d}⇢\mathit{f}\mathrm{)}\wedge \mathtt{absence}\mathrm{(}\mathit{g}\mathrm{)}\end{array}$$

Service contracting  As explained at the end of Section 2, service contracting is an interactive decision procedure that checks whether an execution of the service process exists and satisfies both the service policies and the client contract requirements. In our example this amounts to finding an execution path of (3) such that the constraints (4) and (5) are satisfied. For example, $\{\mathit{a}\mathrm{,}\mathit{d}\mathrm{,}\mathit{f}\mathrm{,}\mathit{f}\mathrm{,}\mathit{f}\mathrm{,}\mathit{h}\}$ is an execution path for (3) path that satisfies the constraints, but $\{\mathit{a}\mathrm{,}\mathit{f}\mathrm{,}\mathit{f}\mathrm{,}\mathit{d}\mathrm{,}\mathit{h}\}$ is an execution that violates $\mathtt{after}\mathrm{(}\mathit{d}⇢\mathit{f}\mathrm{)}$ . The proof procedure introduced in Section 5.2 is designed to find paths on which the constraints are satisfied, if such paths exist. Note it does not matter if the path that was found will actually be the one to be executed – all that is needed is to find out if the contract is satisfiable. If service contracting does not find a path that satisfies the constraints, it means that no execution will ever be successful and the contract is unsatisfiable.

Service contract execution  If a contract is satisfiable, its execution deals with the actual interactions performed by the client and the service. The idea is based on the same proof theory that is used for service contracting, but it is applied differently. When a task is chosen for execution by the client or the service, the proof theory of Section 5.2 checks if acceptance of that task still leaves the possibility of a successful execution of the remainder of the service process (that satisfies the constraints). If so, the task is accepted and executed; otherwise the task is rejected and a different task must be chosen for execution by the agent in question. Note that such a task must exist because when accepting the previous task we must have checked that some continuation is possible.

Contract execution for our example works as follows:

1. Suppose the service selects task a. (This is the only task that can possibly be chosen according to our process specification.) We already checked (while doing service contracting) that there is a legal execution that starts with a, so the task is accepted.

2. The remainder of the process is $\mathrm{(}\mathrm{(}\mathit{d}\vee \mathit{e}\mathrm{)}\mid \mathrm{(}\mathrm{(}\mathit{f}\otimes \mathit{C}\mathrm{)}\vee \mathtt{\text{state}}\mathrm{)}\mathrm{)}\otimes \mathrm{(}\mathit{g}\vee \mathit{h}\mathrm{)}$ (where B and C are replaced with their definitions). The next step can be taken either by the client (e.g., by picking d or e) or by service (e.g., by picking f). It is also possible for the system itself to execute an internal action by picking state (here the client and the service “take a short break”). Let us assume that the client takes initiative and picks e for execution. The system checks if e can be executed and finds that this would violate the constraint $\mathtt{absence}\mathrm{(}\mathit{e}\mathrm{)}$ ; so e is rejected. Suppose that the client does not give up and selects d for execution. Again, the system checks if d is allowed to execute given the constraints. In this case no constraint forbids the execution of d because $\mathit{a}\mathrm{,}\mathit{d}\mathrm{,}\mathit{f}\mathrm{,}\mathit{f}\mathrm{,}\mathit{f}\mathrm{,}\mathit{h}$ is a valid execution of the remainder of the process, so d is accepted.

   It would be very inefficient if the system had to go back to the beginning of the path in order to check if acceptance of an action permits a valid continuation. To avoid this, we modify the constraints after acceptance of each action so that we will never have to look back in order to decide whether to accept or reject an action. For instance, after accepting d the system revises the constraints by replacing $\mathtt{after}\mathrm{(}\mathit{d}⇢\mathit{f}\mathrm{)}$ with ${\mathtt{atleast}}_1\mathrm{(}\mathit{f}\mathrm{)}$ . This is possible because after the execution of d the constraint $\mathtt{after}\mathrm{(}\mathit{d}⇢\mathit{f}\mathrm{)}$ will be satisfied iff f is executed at some point in the future, whence ${\mathtt{atleast}}_1\mathrm{(}\mathit{f}\mathrm{)}$ . The system now checks whether an execution of the remaining process $\mathrm{(}\mathrm{(}\mathit{f}\otimes \mathit{C}\mathrm{)}\vee \mathtt{\text{state}}\mathrm{)}\otimes \mathrm{(}\mathit{g}\vee \mathit{h}\mathrm{)}$ exists under the updated set of constraints $\mathtt{absence}\mathrm{(}\mathit{e}\mathrm{)}\wedge {\mathtt{atleast}}_2\mathrm{(}\mathit{f}\mathrm{)}\wedge {\mathtt{atleast}}_1\mathrm{(}\mathit{f}\mathrm{)}\wedge \mathtt{absence}\mathrm{(}\mathit{g}\mathrm{)}$ (since we have two constraints ${\mathtt{atleast}}_2\mathrm{(}\mathit{f}\mathrm{)}$ and ${\mathtt{atleast}}_1\mathrm{(}\mathit{f}\mathrm{)}$ , the last one can be removed).

3. For the remainder of the process, $\mathrm{(}\mathrm{(}\mathit{f}\otimes \mathit{C}\mathrm{)}\vee \mathtt{\text{state}}\mathrm{)}\otimes \mathrm{(}\mathit{g}\vee \mathit{h}\mathrm{)}$ , only f and $\mathtt{\text{state}}$ can be chosen. Let us assume that the internal action $\mathtt{\text{state}}$ is picked for execution. The system now checks whether an execution of the remaining part of the process, $\mathrm{(}\mathit{g}\vee \mathit{h}\mathrm{)}$ , exists given the updated set of constraints $\mathtt{absence}\mathrm{(}\mathit{e}\mathrm{)}\wedge {\mathtt{atleast}}_2\mathrm{(}\mathit{f}\mathrm{)}\wedge \mathtt{absence}\mathrm{(}\mathit{g}\mathrm{)}$ . It is easy to see that $\mathrm{(}\mathit{g}\vee \mathit{h}\mathrm{)}$ cannot execute to satisfy ${\mathtt{atleast}}_2\mathrm{(}\mathit{f}\mathrm{)}$ because there is no f in $\mathrm{(}\mathit{g}\vee \mathit{h}\mathrm{)}$ . Therefore, $\mathtt{\text{state}}$ is rejected. The only other way to proceed is for the service to pick f (recall that f can be executed only by the service). Proceeding as before, the proof theory would check if f can execute. There are no constraints to prevent that, so the system updates the constraints and checks if a legal continuation is possible. The update replaces ${\mathtt{atleast}}_2\mathrm{(}\mathit{f}\mathrm{)}$ with ${\mathtt{atleast}}_1\mathrm{(}\mathit{f}\mathrm{)}$ , since executing f means that the number of required occurrences of f decreases by 1. The remaining part of the process, $\mathit{C}\otimes \mathrm{(}\mathit{g}\vee \mathit{h}\mathrm{)}$ has a legal execution {f, h} with respect to the updated set of constraints $\mathtt{absence}\mathrm{(}\mathit{e}\mathrm{)}\wedge {\mathtt{atleast}}_1\mathrm{(}\mathit{f}\mathrm{)}\wedge \mathtt{absence}\mathrm{(}\mathit{g}\mathrm{)}$ , so f is accepted.

4. To proceed, we need to expand C using the rule in (3), which gives us $\mathrm{(}\mathrm{(}\mathit{f}\otimes \mathit{C}\mathrm{)}\vee \mathtt{\text{state}}\mathrm{)}\otimes \mathrm{(}\mathit{g}\vee \mathit{h}\mathrm{)}$  – the same process as in the previous step. Although the set of constraints has now changed, because of ${\mathtt{atleast}}_1\mathrm{(}\mathit{f}\mathrm{)}$ the task f must still be executed for the same reasons as in the previous step. This task is accepted because a legal continuation exists, and now the set of constraints gets changed to $\mathtt{absence}\mathrm{(}\mathit{e}\mathrm{)}\wedge \mathtt{absence}\mathrm{(}\mathit{g}\mathrm{)}$ .

5. Now the remainder of the process is $\mathrm{(}\mathit{C}\vee \mathtt{\text{state}}\mathrm{)}\otimes \mathrm{(}\mathit{g}\vee \mathit{h}\mathrm{)}$ and $\mathtt{\text{state}}$ can be successfully picked for execution and the remainder of the process becomes $\mathit{g}\vee \mathit{h}$ . Either g can now be attempted by the client or h by the service. However, the constraint $\mathtt{absence}\mathrm{(}\mathit{g}\mathrm{)}$ prevents the former, so the service proceeds by picking h and, since no constraint prevents it from going ahead, it is executed. At this point, the remainder of the process is empty and we are done.

Note that other executions are also possible and could have been taken. For instance, if the service continued to press initiative in step 2, it could have picked f and the execution could have become a, f, d, f, f, h or a, f, f, d, f, h.

As we saw above, both service contracting and contract execution rely on the same inference rules which do not explicitly differentiate between client and service tasks, however the difference plays out in the way the inference rules are applied.

5.2. Proof system

Let $\mathcal{C}\in \mathcal{C}\mathcal{ONSTR}$ be a constraint (which can be composite), where $\mathcal{C}\mathcal{ONSTR}$ includes both the service policy and the client contract requirements. Let G be a service process and G and $\mathcal{C}$ satisfy the service contracts assumption. We consider the following reasoning problems in ServLog:

1. Contracting: The problem of determining if contracting for a service is possible amounts to finding out if there is an execution of the CTR formula $\mathit{G}\wedge \mathcal{C}$ . Formally, contracting aims to determine if there is a path on which $\mathit{G}\wedge \mathcal{C}$ is true in every multi-path structure that makes all composite task definitions true.

2. Contract Execution: The problem of contract execution amounts to producing an interactive proof that $\mathit{G}\wedge \mathcal{C}$ can execute along some path. In that proof, the client and the service take turns that are prescribed by the process specification and by the ownership of the primitive tasks, as illustrated in the previous subsection. This proof must be constructive – a sequence of applications of the inference rules of CTR, which starts with an axiom and ends with the aforesaid formula $\mathit{G}\wedge \mathcal{C}$ . Each such proof provides a way to execute the process without violating any of the constraints in $\mathcal{C}$ .

The rest of this section develops a proof theory for formulas of the form $\mathit{G}\wedge \mathcal{C}$ , where G is a service process and $\mathcal{C}\in \mathcal{C}\mathcal{ONSTR}$ .

To simplify matters, we will assume that the service process G has no disjunctions in the rule bodies and in its CTR goal part. This does not limit the generality, as such disjunctions can always be eliminated through a simple transformation similar to the one in classical logic. For instance, the disjunction in $$\begin{array}{c}\mathit{p}\leftarrow \mathit{q}\otimes \mathrm{(}\mathit{r}\vee \mathit{s}\mathrm{)}\otimes \mathit{t}\hfill \end{array}$$ can be eliminated by transforming this rule into $$\begin{array}{l}\mathit{p}\leftarrow \mathit{q}\otimes \mathit{newpred}\otimes \mathit{t}\\ \mathit{newpred}\leftarrow \mathit{r}\\ \mathit{newpred}\leftarrow \mathit{s}\end{array}$$

Hot components  We recall the notion of hot components of a CTR goal from [11]: hot(ψ) is a set of subformulas of ψ that are “ready to be executed” and corresponds to the notion of goal selection in SLD-style resolution proof theories. Hot components are defined inductively as follows:

1. hot(()) = {}, where () is the empty goal

2. hot(ψ) = {ψ}, if ψ is an atomic formula

3. hot( ${\mathit{\psi }}_1\otimes \cdots \otimes {\mathit{\psi }}_{\mathit{n}}$ ) = hot( ${\mathit{\psi }}_1$ )

4. hot( ${\mathit{\psi }}_1\mid \cdots \mid {\mathit{\psi }}_{\mathit{n}}$ ) = hot( ${\mathit{\psi }}_1$ ) $\cup \cdots \cup$ hot( ${\mathit{\psi }}_{\mathit{n}}$ )

5. hot( $\odot \mathit{\psi }$ ) = { $\odot \mathit{\psi }$ }

Additional constraints  The set of constraints is changing as tasks in the process execute. The exact mechanism is explained in the inference rule “executing primitive update tasks,” below. It involves three new constraints: $\mathtt{force}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\mathrm{)}$ , $\mathtt{suspend}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\mathrm{)}$ , and , plus a generalization of the constraint $\mathtt{before}$ , which allows exceptions. We did not introduce these before, since the new constraints are technical means by which the proof theory works and they are unlikely to be employed by users directly.

The meaning of the constraint $\mathtt{force}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\mathrm{)}$ , where $\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}$ is a task pattern for a primitive update, is that the very next task to be executed must match $\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}$ . More precisely, an execution $⟨{\mathbf{\text{s}}}_1\mathrm{,}{\mathbf{\text{s}}}_2\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{n}}⟩$ satisfies $\mathtt{force}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\mathrm{)}$ if ${\mathbf{\text{s}}}_1\stackrel{\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_2$ holds and $\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}$ matches $\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}$ .

The constraint $\mathtt{suspend}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\mathrm{)}$ means that no task that matches $\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}$ can execute at the current state. Formally, an execution $⟨{\mathbf{\text{s}}}_1\mathrm{,}{\mathbf{\text{s}}}_2\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{n}}⟩$ , such that ${\mathbf{\text{s}}}_1\stackrel{\mathit{r}\mathrm{(}\bar{\mathit{V}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_2$ holds for some task atom $\mathit{r}\mathrm{(}\bar{\mathit{V}}\mathrm{)}$ , satisfies $\mathtt{suspend}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\mathrm{)}$ if $\mathit{r}\mathrm{(}\bar{\mathit{V}}\mathrm{)}$ does not match $\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}$ .

The constraint says that $\mathit{q}\mathrm{(}{\bar{\mathit{u}}}^{\prime }\mathrm{)}$ must be immediately preceded by $\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}$ unless it is the first task to be executed. That first task can be a q-task, if it matches $\mathit{q}\mathrm{(}{\bar{\mathit{u}}}^{\prime }\mathrm{)}$ . Formally, an execution $⟨{\mathbf{\text{s}}}_1\mathrm{,}{\mathbf{\text{s}}}_2\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{n}}⟩$ satisfies this constraint if and only if either $⟨{\mathbf{\text{s}}}_1\mathrm{,}{\mathbf{\text{s}}}_2\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{n}}⟩$ satisfies $\mathtt{right}\text{\_}\mathtt{before}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\leftarrow \mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)}\mathrm{)}$ or ${\mathbf{\text{s}}}_1\stackrel{\mathit{q}\mathrm{(}\bar{\mathit{V}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_2$ holds, where $\mathit{q}\mathrm{(}\bar{\mathit{V}}\mathrm{)}$ matches $\mathit{q}\mathrm{(}{\bar{\mathit{u}}}^{\prime }\mathrm{)}$ , and $⟨{\mathbf{\text{s}}}_2\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{n}}⟩$ satisfies $\mathtt{right}\text{\_}\mathtt{before}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}\leftarrow \mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)}\mathrm{)}$ .

The generalization of $\mathtt{before}$ has the following syntax: $$\begin{array}{}\text{(6)}& \mathtt{before}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}⇠\mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)}\setminus \{\mathit{q}\mathrm{(}\overline{{\mathit{u}}_1}\mathrm{)}\mathrm{,}\dots \mathrm{,}\mathit{q}\mathrm{(}\overline{{\mathit{u}}_{\mathit{n}}}\mathrm{)}\left\}\mathrm{\right)}\end{array}$$ where $\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}$ , $\mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)}$ , and $\mathit{q}\mathrm{(}\overline{{\mathit{u}}_1}\mathrm{)}\mathrm{,}\dots \mathrm{,}\mathit{q}\mathrm{(}\overline{{\mathit{u}}_{\mathit{n}}}\mathrm{)}$ , $\mathit{n}⩾0$ ( $\mathit{n}=0$ means that the sets of exceptions are empty), are task patterns. The use of “∖” here indicates that $\mathtt{before}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)}⇠\mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)}\mathrm{)}$ must hold, except for the tasks that match one of the exceptions $\mathit{q}\mathrm{(}\overline{{\mathit{u}}_1}\mathrm{)}\mathrm{,}\dots \mathrm{,}\mathit{q}\mathrm{(}\overline{{\mathit{u}}_{\mathit{n}}}\mathrm{)}$ .

Formally, an execution $⟨{\mathbf{\text{s}}}_1\mathrm{,}\dots \mathrm{,}{\mathbf{\text{s}}}_{\mathit{m}}⟩$ satisfies the constraint (6) if and only if whenever there is a state ${\mathbf{\text{s}}}_{\mathit{i}}$ in this execution such that ${\mathbf{\text{s}}}_{\mathit{i}}\stackrel{\mathit{q}\mathrm{(}\bar{\mathit{U}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{\mathit{i}+1}$ and $\mathit{q}\mathrm{(}\bar{\mathit{U}}\mathrm{)}$ matches $\mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)}$ but $\mathit{none}$ of the $\mathit{q}\mathrm{(}\overline{{\mathit{u}}_{\mathit{i}}}\mathrm{)}$ ’s then there is j, $\mathit{j}\mathrm{<}\mathit{i}$ , such that ${\mathbf{\text{s}}}_{\mathit{j}}\stackrel{\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}}{⟶}{\mathbf{\text{s}}}_{\mathit{j}+1}$ holds and $\mathit{p}\mathrm{(}\bar{\mathit{T}}\mathrm{)}$ matches $\mathtt{\text{refine}}\mathrm{(}\mathit{p}\mathrm{(}\bar{\mathit{t}}\mathrm{)};\mathit{q}\mathrm{(}\bar{\mathit{U}}\mathrm{)}\mathrm{,}\mathit{q}\mathrm{(}\bar{\mathit{u}}\mathrm{)}\mathrm{)}$ .

Note that, when the set of exceptions is empty, the constraint (6) reduces to the old form of the $\mathtt{before}$ -constraint. Therefore, to simplify the language, in the rest of this section we will be using only the generalized form of this constraint.

Substitutions  As usual in logic proof theories, we will rely on the notion of substitution, which is a mapping from variables to terms. If σ is a substitution and ψ is a service process or a term then we write $\mathit{\psi }\mathit{\sigma }$ for the result of applying the substitution σ to ψ. We call $\mathit{\psi }\mathit{\sigma }$ an instance of ψ. If $\mathit{\psi }\mathit{\sigma }$ has no variables left, we say that $\mathit{\psi }\mathit{\sigma }$ is a ground instance and that σ is a ground substitution.

Sequents  Let $\mathbf{\text{P}}$ be a set of composite task definitions. The proof theory manipulates expressions of the form $\mathbf{\text{P}}\mathrm{,}\mathbf{\text{s}}\text{ ---}⊢\mathrm{(}\exists \mathrm{)}\mathit{\psi }\wedge \mathcal{C}$ , called sequents, where $\mathbf{\text{P}}$ is a set of task definitions, $\mathbf{\text{s}}$ is an identifier for the underlying database state, ψ is a CTR goal, and $\mathcal{C}$ is a (possibly composite) constraint, which may include the constraints in $\mathcal{C}\mathcal{ONSTR}$ as well as the new constraints ( $\mathtt{force}$ , $\mathtt{suspend}$ , etc.) introduced just above. Informally, a sequent is a statement that $\mathrm{(}\exists \mathrm{)}\mathit{\psi }$ , which is defined by the rules in $\mathbf{\text{P}}$ , can execute along some path that starts at state $\mathbf{\text{s}}$ so that all the constraints in $\mathcal{C}$ will be satisfied. Each inference rule has two sequents, one above the other. This is interpreted as: if the upper sequent is inferred, then the lower sequent should also be inferred. As in classical logic, any instance of an answer-substitution is a valid answer to a query.

The inference system presented here extends the inference system for Horn CTR [11] with two additional inference rules (Rules 2 and 3). Other rules from [11] (e.g., Rule 6) are also significantly modified. The new system reduces to the old one when the constraint $\mathcal{C}$ is a CTR tautology ( $\mathtt{path}$ ). The new system also extends and simplifies the proof theory developed in [39].

All rules and the axioms operate with constraints, which get modified as a result of the rule application. However, some of the rules require the constraint to be a conjunction of the existence, serial, and the additional constraints introduced in this section. We call such constraints conjunctive. A conjunctive constraint can be viewed as a set, so we will often write $\mathit{c}\in \mathcal{C}$ meaning that c is a conjunct in $\mathcal{C}$ .

The notion of a proof  A proof of a sequent seq is a series of sequents, ${\mathit{seq}}_0\mathrm{,}{\mathit{seq}}_1\mathrm{,}\dots \mathrm{,}{\mathit{seq}}_{\mathit{n}-1}\mathrm{,}{\mathit{seq}}_{\mathit{n}}$ , where ${\mathit{seq}}_{\mathit{n}}=\mathit{seq}$ and each ${\mathit{seq}}_{\mathit{i}}$ is either an axiom-sequent (below) or is derived from earlier sequents by one of the inference rules below.

Axiom  All axioms have the form $\mathbf{\text{P}}\mathrm{,}\mathbf{\text{s}}\text{ ---}⊢\mathrm{(}\mathrm{)}\wedge \mathcal{C}$ , where $\mathbf{\text{s}}$ is a database state identifier and $\mathcal{C}$ is a conjunctive constraint that does not contain constraints of the form $\mathtt{force}\mathrm{(}\overline{\mathit{r}}\mathrm{)}$ , ${\mathtt{atleast}}_{\mathit{k}}\mathrm{(}\overline{\mathit{r}}\mathrm{)}$ , and ${\mathtt{exactly}}_{\mathit{k}}\mathrm{(}\overline{\mathit{r}}\mathrm{)}$ , where $\mathit{k}⩾1$ .

Inference rules  In Rules 1–7 below, σ denotes a substitution, ψ and ${\mathit{\psi }}^{\prime }$ are service processes, $\mathcal{C}$ and ${\mathcal{C}}^{\prime }$ are constraints, $\mathbf{\text{s}}$ , ${\mathbf{\text{s}}}_1$ , ${\mathbf{\text{s}}}_2$ are database state identifiers, and p is a task.

Eliminating disjunctive constraints: Let ψ be a CTR goal and ${\mathcal{C}}^{\prime }$ a disjunct in the disjunctive normal form of $\mathcal{C}$ (i.e., ${\mathcal{C}}^{\prime }$ is a conjunctive constraint). Then Note that ${\mathcal{C}}^{\prime }$ is a conjunction of existence and serial constraints.

Solving builtin tests: Let χ be a conjunction of builtin test tasks. Suppose there is a ground substitution σ such that $\mathit{\chi }\mathit{\sigma }$ evaluates to true. Then

Commutativity with respect to builtin tests: Let χ be a conjunction of builtin test tasks and ψ a CTR goal. Then

Applying composite task definitions: Let r ← β be a rule in $\mathbf{\text{P}}$ , and assume that its variables have been renamed so that none are shared with ψ. If p and r unify with the most general unifier σ then where ${\mathit{\psi }}^{\prime }$ is obtained from ψ by replacing a hot occurrence of p with β.

Executing query tasks: Suppose that $\mathit{p}\mathit{\sigma }$ and ${\mathit{\psi }}^{\prime }\mathit{\sigma }$ share no variables and either (i) p is a primitive query task such that (∃) $\mathit{p}\mathit{\sigma }$ is true in the state $\mathbf{\text{s}}$ ; or (ii) $\mathit{p}=\mathtt{\text{state}}$ and σ is the identity substitution. Then where ${\mathit{\psi }}^{\prime }$ is obtained from ψ by deleting a hot occurrence of p.

Executing primitive update tasks: Let $\mathit{p}\mathit{\sigma }$ be a primitive update task such that ${\mathbf{\text{s}}}_1\stackrel{\mathit{p}\mathit{\sigma }}{⟶}{\mathbf{\text{s}}}_2$ , $\mathit{p}\in \mathrm{hot}\mathrm{(}\mathit{\psi }\mathrm{)}$ , and $\mathcal{C}$ has no constraint of either of the forms below. In the description below, we assume that $\overline{\mathit{p}}$ is a task pattern such that $\mathit{p}\mathit{\sigma }$ matches $\overline{\mathit{p}}$ and that $\overline{\mathit{r}}$ denotes an arbitrary task pattern:

$\mathtt{absence}\mathrm{(}\overline{\mathit{p}}\mathrm{)}$

$\mathtt{suspend}\mathrm{(}\overline{\mathit{p}}\mathrm{)}$

$\mathtt{force}\mathrm{(}\overline{\mathit{r}}\mathrm{)}$ such that $\mathit{p}\mathit{\sigma }$ does not match $\overline{\mathit{r}}$

$\mathtt{before}\mathrm{(}\overline{\mathit{r}}⇠\overline{\mathit{p}}\setminus \{{\overline{\mathit{p}}}_1\mathrm{,}\dots \mathrm{,}{\overline{\mathit{p}}}_{\mathit{k}}\}\mathrm{)}\mathit{k}⩾0$ and $\mathit{p}\mathit{\sigma }$ matches neither $\overline{\mathit{r}}$ nor any of the ${\overline{\mathit{p}}}_{\mathit{i}}$ ’s

$\mathtt{right}\text{\_}\mathtt{before}\mathrm{(}\overline{\mathit{r}}\leftarrow \overline{\mathit{p}}\mathrm{)}$

, where $\mathit{p}\mathit{\sigma }$ does not match ${\overline{\mathit{p}}}^{\prime }$ .

Then the inference rule has the following form: where $\mathcal{C}$ is a conjunctive constraint, ${\mathit{\psi }}^{\prime }$ is obtained from ψ by deleting the hot component p, and ${\mathcal{C}}^{\prime }$ is constructed out of $\mathcal{C}$ as follows.

Initially, ${\mathcal{C}}^{\prime }$ is empty (a tautology, $\mathtt{path}$ ). Then constraints are added to it (as conjuncts) according to the cases below. (Again, in all these cases, we assume that $\mathit{p}\mathit{\sigma }$ matches $\overline{\mathit{p}}$ and $\overline{\mathit{r}}$ , $\overline{\mathit{s}}$ are arbitrary task patterns.)

• If ${\mathtt{atleast}}_{\mathit{n}}\mathrm{(}\overline{\mathit{p}}\mathrm{)}\in \mathcal{C}$ , where $\mathit{n}\mathrm{>}1$ , add the following to ${\mathcal{C}}^{\prime }$ :

• If ${\mathtt{exactly}}_{\mathit{n}}\mathrm{(}\overline{\mathit{p}}\mathrm{)}\in \mathcal{C}$ , where $\mathit{n}\mathrm{>}1$ , add the following to ${\mathcal{C}}^{\prime }$ :

• If ${\mathtt{exactly}}_1\mathrm{(}\overline{\mathit{p}}\mathrm{)}\in \mathcal{C}$ , add the following to  ${\mathcal{C}}^{\prime }$ :

• If $\mathtt{after}\mathrm{(}\overline{\mathit{p}}⇢\overline{\mathit{r}}\mathrm{)}\in \mathcal{C}$ , add the following to  ${\mathcal{C}}^{\prime }$ :

• If , add the following to ${\mathcal{C}}^{\prime }$ :

• If $\mathtt{right}\text{\_}\mathtt{after}\mathrm{(}\overline{\mathit{p}}\to \overline{\mathit{r}}\mathrm{)}\in \mathcal{C}$ , add the following to ${\mathcal{C}}^{\prime }$ :

• If $\mathtt{before}\mathrm{(}\overline{\mathit{p}}⇠\overline{\mathit{r}}\setminus \{{\overline{\mathit{r}}}_1\mathrm{,}\dots \mathrm{,}{\overline{\mathit{r}}}_{\mathit{k}}\}\mathrm{)}\in \mathcal{C}$ , add the following to ${\mathcal{C}}^{\prime }$ :

• If $\mathtt{not}\text{\_}\mathtt{right}\text{\_}\mathtt{after}\mathrm{(}\overline{\mathit{p}}\nrightarrow \overline{\mathit{r}}\mathrm{)}\in \mathcal{C}$ , add the following to ${\mathcal{C}}^{\prime }$ :

• If $\mathtt{right}\text{\_}\mathtt{before}\mathrm{(}\overline{\mathit{p}}\leftarrow \overline{\mathit{r}}\mathrm{)}\in \mathcal{C}$ , add the following to ${\mathcal{C}}^{\prime }$ :

• If , add the following to ${\mathcal{C}}^{\prime }$ :

• If $\mathtt{between}\mathrm{(}\overline{\mathit{p}}⇢\overline{\mathit{r}}⇠\overline{\mathit{s}}\mathrm{)}\in \mathcal{C}$ , add the following to ${\mathcal{C}}^{\prime }$ :

• If , add the following to ${\mathcal{C}}^{\prime }$ :

• For all other constraints in $\mathcal{C}$ , copy them over to ${\mathcal{C}}^{\prime }$ , but leave out the constraints of the form:

Executing atomic tasks: If $\odot \mathit{\alpha }$ is a hot component in ψ then where ${\mathit{\psi }}^{\prime }$ is obtained from ψ by deleting a hot occurrence of $\odot \mathit{\alpha }$ .

Theorem 1.

The above inference system is sound and complete for proving constrained service processes, if the service processes and the constraints satisfy the service contracts assumptions.

Proof.

Soundness of the inference system is proved in Appendix A and completeness in B.  □

Example.

The following example illustrates the inference procedure. $$\begin{array}{l}\mathtt{\text{Goal }}\mathit{G}\mathtt{\text{:}}\exists ?\mathit{x}\mathrm{\left(}\mathrm{\right(}\mathit{p}\mathrm{(}?\mathit{x}\mathrm{)}\otimes \mathit{q}\mathrm{)}\mid \mathit{r}\mathrm{(}?\mathit{x}\mathrm{)}\mathrm{)}\\ \mathtt{\text{Rules:}}\\ \mathit{r}\mathrm{(}?\mathit{x}\mathrm{)}\leftarrow \mathrm{(}\mathit{x}\mathit{y}\mathit{z}\mathrm{(}?\mathit{y}\mathrm{,}?\mathit{z}\mathrm{)}\otimes \mathit{s}\mathrm{(}?\mathit{x}\mathrm{,}?\mathit{y}\mathrm{,}?\mathit{z}\mathrm{)}\\ \phantom{\mathit{r}\mathrm{(}?\mathit{x}\mathrm{)}\leftarrow }\otimes \mathit{r}\mathrm{(}?\mathit{y}\mathrm{)}\mathrm{)}\\ \mathit{r}\mathrm{(}?\mathit{x}\mathrm{)}\leftarrow \mathtt{\text{state}}\\ \mathtt{\text{Constraint }}\mathcal{C}\mathtt{\text{:}}\\ \mathrm{\left(}{\mathtt{atleast}}_2\mathrm{\right(}\mathit{s}\mathrm{(}\text{\_}\mathrm{,}\text{\_}\mathrm{,}\text{\_}\mathrm{)}\mathrm{)}\\ \vee \mathtt{before}\mathrm{(}\mathit{p}\mathrm{(}\text{\_}\mathit{x}\mathrm{)}⇠\mathit{s}\mathrm{(}\text{\_}\mathit{x}\mathrm{,}1\mathrm{,}\text{\_}\mathit{z}\mathrm{)}\mathrm{)}\mathrm{)}\end{array}$$ Here p, q, and s are assumed to be primitive tasks, and in the case of p and s they can be executed with any integer argument. Furthermore, in this example we assume that the execution of p, s, and q modifies the database, as follows: $\mathit{p}\mathrm{(}1\mathrm{)}$ adds $\mathit{x}\mathit{y}\mathit{z}\mathrm{(}3\mathrm{,}7\mathrm{)}$ ; $\mathit{s}\mathrm{(}1\mathrm{,}3\mathrm{,}7\mathrm{)}$ adds $\mathit{x}\mathit{y}\mathit{z}\mathrm{(}2\mathrm{,}7\mathrm{)}$ ; $\mathit{s}\mathrm{(}3\mathrm{,}2\mathrm{,}7\mathrm{)}$ adds $\mathit{a}\mathit{b}\mathit{c}\mathrm{(}1\mathrm{)}$ ; and q deletes $\mathit{x}\mathit{y}\mathit{z}\mathrm{(}3\mathrm{,}7\mathrm{)}$ . These assumptions were needed in order to show that the constraint is satisfied in this example. If we did not make these assumptions, then the constraint might not be satisfied in which case the inference procedure would not infer the constraint. The goal G can be executed in several ways such that $\mathcal{C}$ is satisfied. We show one possibility, which corresponds to one derivation of the sequent $\mathbf{\text{P}}$ , $\mathbf{\text{s}}\text{ ---}⊢\mathit{G}\wedge \mathcal{C}$ , where $\mathbf{\text{s}}$ is an identifier for $\{\}$ , the empty state. In this derivation, we use the top-down method, i.e., we start with the goal and apply the inference rules backwards. Each sequent is derived from the previous one by an inference rule. The deduction succeeds when the last sequent is an axiom. We start with the sequent $$\begin{array}{ll}\hfill \mathit{P}\mathrm{,}\{\}\text{ ---}& ⊢\mathrm{(}\exists ?\mathit{x}\mathrm{(}\mathrm{(}\mathit{p}\mathrm{(}?\mathit{x}\mathrm{)}\otimes \mathit{q}\mathrm{)}\mid \mathit{r}\mathrm{(}?\mathit{x}\mathrm{)}\mathrm{\left)}\mathrm{\right)}\\ \hfill & \wedge \mathrm{\left(}{\mathtt{atleast}}_2\mathrm{\right(}\mathit{s}\mathrm{(}\text{\_}\mathrm{,}\text{\_}\mathrm{,}\text{\_}\mathrm{)}\mathrm{)}\\ \hfill & \vee \mathtt{before}\mathrm{(}\mathit{p}\mathrm{(}\text{\_}\mathit{x}\mathrm{)}⇠\mathit{s}\mathrm{(}\text{\_}\mathit{x}\mathrm{,}1\mathrm{,}\text{\_}\mathrm{)}\mathrm{)}\mathrm{)}\end{array}$$ Here, instead of a state identifier ( $\mathbf{\text{s}}$ ) we put the corresponding database state ({ }) explicitly. To make the sequent easier to read, we will continue doing this in the rest of this example.

Hot components: $\{\mathit{p}\mathrm{(}?\mathit{x}\mathrm{)}\mathrm{,}\mathit{r}\mathrm{(}?\mathit{x}\mathrm{)}\}$ . By inference rule 1 (eliminating disjunctive constraints) we obtain: $$\begin{array}{ll}\hfill \mathit{P}\mathrm{,}\{\}\text{ ---}⊢& \mathrm{(}\exists ?\mathit{x}\mathrm{(}\mathrm{(}\mathit{p}\mathrm{(}?\mathit{x}\mathrm{)}\otimes \mathit{q}\mathrm{)}\mid \mathit{r}\mathrm{(}?\mathit{x}\mathrm{)}\mathrm{\left)}\mathrm{\right)}\\ \hfill & \wedge {\mathtt{atleast}}_2\mathrm{(}\mathit{s}\mathrm{(}\text{\_}\mathrm{,}\text{\_}\mathrm{,}\text{\_}\mathrm{)}\mathrm{)}\end{array}$$

Hot components: $\{\mathit{p}\mathrm{(}?\mathit{x}\mathrm{)}\mathrm{,}\mathit{r}\mathrm{(}?\mathit{x}\mathrm{)}\}$ . By inference rule 4 (composite task definitions) we obtain: $$\begin{array}{ll}\hfill \mathit{P}\mathrm{,}\{\}\text{ ---}& ⊢\mathrm{(}\exists ?\mathit{x}\mathrm{,}?\mathit{y}\mathrm{,}?\mathit{z}\mathrm{(}\mathit{p}\mathrm{(}?\mathit{x}\mathrm{)}\otimes \mathit{q}\mathrm{)}\\ \hfill & \mid \mathrm{(}\mathit{x}\mathit{y}\mathit{z}\mathrm{(}?\mathit{y}\mathrm{,}?\mathit{z}\mathrm{)}\otimes \mathit{s}\mathrm{(}?\mathit{x}\mathrm{,}?\mathit{y}\mathrm{,}?\mathit{z}\mathrm{)}\otimes \mathit{r}\mathrm{(}?\mathit{y}\mathrm{)}\mathrm{)}\mathrm{)}\\ \hfill & \wedge {\mathtt{atleast}}_2\mathrm{(}\mathit{s}\mathrm{(}\text{\_}\mathrm{,}\text{\_}\mathrm{,}\text{\_}\mathrm{)}\mathrm{)}\end{array}$$ Hot components: $\{\mathit{p}\mathrm{(}?\mathit{x}\mathrm{)}\mathrm{,}\mathit{x}\mathit{y}\mathit{z}\mathrm{(}?\mathit{y}\mathrm{,}?\mathit{z}\mathrm{)}\}$ . By inference rule 6, choosing $\mathit{p}\mathrm{(}?\mathit{x}\mathrm{)}$ and executing this primitive task with the argument $?\mathit{x}=1$ , we obtain (recall that the execution of $\mathit{p}\mathrm{(}1\mathrm{)}$ adds the fact $\mathit{x}\mathit{y}\mathit{z}\mathrm{(}3\mathrm{,}7\mathrm{)}$ to the database): $$\begin{array}{ll}\hfill \mathit{P}\mathrm{,}\{\mathit{x}\mathit{y}\mathit{z}\mathrm{(}3\mathrm{,}7\mathrm{)}\}\text{ ---}⊢& \mathrm{(}\exists ?\mathit{y}\mathrm{,}?\mathit{z}\mathit{q}\\ \hfill & \mid \mathrm{(}\mathit{x}\mathit{y}\mathit{z}\mathrm{(}?\mathit{y}\mathrm{,}?\mathit{z}\mathrm{)}\otimes \mathit{s}\mathrm{(}1\mathrm{,}?\mathit{y}\mathrm{,}?\mathit{z}\mathrm{)}\\ \hfill & \otimes \mathit{r}\mathrm{(}?\mathit{y}\mathrm{)}\mathrm{\left)}\mathrm{\right)}\\ \hfill & \wedge {\mathtt{atleast}}_2\mathrm{(}\mathit{s}\mathrm{(}\text{\_}\mathrm{,}\text{\_}\mathrm{,}\text{\_}\mathrm{)}\mathrm{)}\end{array}$$ Hot components: $\{\mathit{q}\mathrm{,}\mathit{x}\mathit{y}\mathit{z}\mathrm{(}?\mathit{y}\mathrm{,}?\mathit{z}\mathrm{)}\}$ . By inference rule 5 (executing query tasks): $$\begin{array}{ll}\hfill \mathit{P}\mathrm{,}\{\mathit{x}\mathit{y}\mathit{z}\mathrm{(}3\mathrm{,}7\mathrm{)}\}\text{ ---}⊢& \mathrm{(}\mathit{q}\mid \mathrm{(}\mathit{s}\mathrm{(}1\mathrm{,}3\mathrm{,}7\mathrm{)}\otimes \mathit{r}\mathrm{(}3\mathrm{)}\mathrm{)}\mathrm{)}\\ \hfill & \wedge {\mathtt{atleast}}_2\mathrm{(}\mathit{s}\mathrm{(}\text{\_}\mathrm{,}\text{\_}\mathrm{,}\text{\_}\mathrm{)}\mathrm{)}\end{array}$$ Hot components: $\{\mathit{q}\mathrm{,}\mathit{s}\mathrm{(}1\mathrm{,}3\mathrm{,}7\mathrm{)}\}$ . By inference rule 6 applied to the primitive task $\mathit{s}\mathrm{(}1\mathrm{,}3\mathrm{,}7\mathrm{)}$ and the earlier assumption, this execution adds the fact $\mathit{x}\mathit{y}\mathit{z}\mathrm{(}2\mathrm{,}7\mathrm{)}$ to the database: $$\begin{array}{l}\mathit{P}\mathrm{,}\{\mathit{x}\mathit{y}\mathit{z}\mathrm{(}3\mathrm{,}7\mathrm{)}\mathrm{,}\mathit{x}\mathit{y}\mathit{z}\mathrm{(}2\mathrm{,}7\mathrm{)}\}\text{ ---}⊢\\ \mathrm{(}\mathit{q}\mid \mathit{r}\mathrm{(}3\mathrm{)}\mathrm{)}\wedge {\mathtt{atleast}}_1\mathrm{(}\mathit{s}\mathrm{(}\text{\_}\mathrm{,}\text{\_}\mathrm{,}\text{\_}\mathrm{)}\mathrm{)}\end{array}$$ Hot components: $\{\mathit{q}\mathrm{,}\mathit{r}\mathrm{(}3\mathrm{)}\}$ . By inference rule 6 applied to the primitive task q (which, as mentioned above, deletes $\mathit{x}\mathit{y}\mathit{z}\mathrm{(}3\mathrm{,}7\mathrm{)}$ ): $$\begin{array}{ll}\hfill \mathit{P}\mathrm{,}\{\mathit{x}\mathit{y}\mathit{z}\mathrm{(}2\mathrm{,}7\mathrm{)}\}& \text{ ---}⊢\\ \hfill & \mathit{r}\mathrm{(}3\mathrm{)}\wedge {\mathtt{atleast}}_1\mathrm{(}\mathit{s}\mathrm{(}\text{\_}\mathrm{,}\text{\_}\mathrm{,}\text{\_}\mathrm{)}\mathrm{)}\end{array}$$ Hot components: $\{\mathit{r}\mathrm{(}3\mathrm{)}\}$ . By inference rule 4 (composite task definitions): $$\begin{array}{ll}\hfill \mathit{P}\mathrm{,}\{\mathit{x}\mathit{y}\mathit{z}\mathrm{(}2\mathrm{,}7\mathrm{)}\}\text{ ---}⊢& \mathrm{(}\exists ?\mathit{y}\mathrm{,}?\mathit{z}\mathrm{(}\mathit{x}\mathit{y}\mathit{z}\mathrm{(}?\mathit{y}\mathrm{,}?\mathit{z}\mathrm{)}\\ \hfill & \otimes \mathit{s}\mathrm{(}3\mathrm{,}?\mathit{y}\mathrm{,}?\mathit{z}\mathrm{)}\otimes \mathit{r}\mathrm{(}?\mathit{y}\mathrm{)}\mathrm{\left)}\mathrm{\right)}\\ \hfill & \wedge {\mathtt{atleast}}_1\mathrm{(}\mathit{s}\mathrm{(}\text{\_}\mathrm{,}\text{\_}\mathrm{,}\text{\_}\mathrm{)}\mathrm{)}\end{array}$$ Hot components: $\{\mathit{x}\mathit{y}\mathit{z}\mathrm{(}?\mathit{y}\mathrm{,}?\mathit{z}\mathrm{)}\}$ . By inference rule 5 (executing query tasks) and choosing $\mathit{x}\mathit{y}\mathit{z}\mathrm{(}?\mathit{y}\mathrm{,}?\mathit{z}\mathrm{)}$ : $$\begin{array}{ll}\hfill \mathit{P}\mathrm{,}\{\mathit{x}\mathit{y}\mathit{z}\mathrm{(}2\mathrm{,}7\mathrm{)}\}\text{ ---}⊢& \mathrm{(}\mathit{s}\mathrm{(}3\mathrm{,}2\mathrm{,}7\mathrm{)}\otimes \mathit{r}\mathrm{(}2\mathrm{)}\mathrm{)}\\ \hfill & \wedge {\mathtt{atleast}}_1\mathrm{(}\mathit{s}\mathrm{(}\text{\_}\mathrm{,}\text{\_}\mathrm{,}\text{\_}\mathrm{)}\mathrm{)}\end{array}$$ Hot components: $\{\mathit{s}\mathrm{(}3\mathrm{,}2\mathrm{,}7\mathrm{)}\}$ . By inference rule 6 for executing the primitive task $\mathit{s}\mathrm{(}3\mathrm{,}2\mathrm{,}7\mathrm{)}$ and by the earlier assumption, it adds the fact $\mathit{a}\mathit{b}\mathit{c}\mathrm{(}1\mathrm{)}$ to the database: $$\begin{array}{c}\mathit{P}\mathrm{,}\{\mathit{x}\mathit{y}\mathit{z}\mathrm{(}2\mathrm{,}7\mathrm{)}\mathrm{,}\mathit{a}\mathit{b}\mathit{c}\mathrm{(}1\mathrm{)}\}\text{ ---}⊢\mathit{r}\mathrm{(}2\mathrm{)}\end{array}$$ Hot components: $\{\mathit{r}\mathrm{(}2\mathrm{)}\}$ . By inference rule 4 (composite task definitions), where we use the second rule for r: $$\begin{array}{c}\mathit{P}\mathrm{,}\{\mathit{x}\mathit{y}\mathit{z}\mathrm{(}2\mathrm{,}7\mathrm{)}\mathrm{,}\mathit{a}\mathit{b}\mathit{c}\mathrm{(}1\mathrm{)}\}\text{ ---}⊢\mathtt{\text{state}}\end{array}$$ Hot components: $\{\mathtt{\text{state}}\}$ . By rule 5 applied to $\mathtt{\text{state}}$ we derive: $$\begin{array}{c}\mathit{P}\mathrm{,}\{\mathit{x}\mathit{y}\mathit{z}\mathrm{(}2\mathrm{,}7\mathrm{)}\mathrm{,}\mathit{a}\mathit{b}\mathit{c}\mathrm{(}1\mathrm{)}\}\text{ ---}⊢\mathrm{(}\mathrm{)}\end{array}$$ During the deduction, we executed the following sequence of primitive tasks: $$\begin{array}{l}\{\mathit{p}\mathrm{(}1\mathrm{)}\mathrm{,}\mathit{x}\mathit{y}\mathit{z}\mathrm{(}3\mathrm{,}7\mathrm{)}\mathrm{,}\mathit{s}\mathrm{(}1\mathrm{,}3\mathrm{,}7\mathrm{)}\mathrm{,}\mathit{q}\mathrm{,}\mathit{x}\mathit{y}\mathit{z}\mathrm{(}2\mathrm{,}7\mathrm{)}\mathrm{,}\\ \mathit{s}\mathrm{(}3\mathrm{,}2\mathrm{,}7\mathrm{)}\mathrm{,}\mathtt{\text{state}}\}\end{array}$$ It is easy to see that this sequence indeed satisfies the constraint $\mathcal{C}$ , which required $\mathit{s}\mathrm{(}\text{\_}\mathrm{,}\text{\_}\mathrm{,}\text{\_}\mathrm{)}$ to be executed at least twice.

5.3. Decidability and complexity

In general, query answering in CTR is semi-decidable [11], like in classical logic, so no effective procedure exists to answer all possible queries and terminate. Appendices A and B show that the same is true for ServLog. In [8], various subsets of CTR were investigated for their decidability and complexity properties. One important restriction studied there is called full boundedness. In terms of ServLog, this roughly means that every update task must diminish some bounded from below, discrete measure (e.g., a positive integer measure). In that case, the CTR proof procedure is data-complete for NP [8] (i.e., NP-complete when the rules are fixed but data is allowed to vary). Fortunately, all existing workflow modeling systems are implicitly based on the assumption that any useful workflow must be fully bounded (where the bounds can be defined for different processes). Typically this is manifested by imposing upper bounds on the number of iterations, the number of steps, and other similar restrictions. It is also easy to instrument ServLog service processes so that they become fully bounded. For instance, primitive update tasks could be forced to diminish a global discrete and bounded resource. More importantly, the recent trend in logic programming is to avoid restricting the expressive power of programs by curtailing the usefulness of logical frameworks with restrictions, such as full boundedness. Instead, new approaches aim to develop tools for detecting non-terminating behavior and help the programmer correct the problem [23,31]. It is our contention that this is a more productive direction for Transaction Logic-based approaches than the restriction-based approaches. We should also note that some decidability results developed for other approaches carry over to ServLog – see the discussion of artifact systems [16] in Section 6.

6. Related work

ServLog builds on the service contracting framework that was partially developed in [39,40], greatly expanding and generalizing it, while at the same time simplifying the technical details. The major simplifications and extensions include:

• Removing the unique task occurrence restriction and obviating the need for complex simplification transformations.

• Tasks are no longer limited to propositional constants. This provides the ability to represent complex data flow among tasks as well as general transitional constraints.

• General iterative and even mutually recursive tasks in the specification of service processes.

• Generalization of the proof theory, which now deals with the many new additions to the language, and handles constrained (non-Horn) formulas, which previous CTR proof theory was not able to handle.

• Proofs of soundness and completeness for the generalized proof theory.

The present paper significantly extends this proof theory to formulas that contain the ∧ connective thus enabling execution of constrained transactions, which are non-Horn. We also deal with a much larger class of constraints than [17,39], including iterative processes.

Declare [45] is a service flow language that is closely related to ServLog. It uses Linear Temporal Logic to formalize service flows and automata theory to enact service specifications. The relations between tasks are described entirely in terms of constraints. Apart from the obvious radical differences in the formalisms, some other important differences are worth noting. First, the constraint algebra $\mathcal{C}\mathcal{ONSTR}$ of ServLog is more expressive than the one used in Declare. Second, by combining constraints with service processes (conditional control flow and data flow), ServLog incorporates current practices in workflow modeling. Third, data flow and conditional control flow are easily available in ServLog, while they have not been developed in the context of Declare. Declare was also formalized using Abductive Logic Programming in [34]. While this formalization supports different verification tasks, the focus remains on modeling service flow exclusively in terms of constraints and does not deal with control and data flow.

In [48 ,49] the authors propose a combination of colored Petri nets, Declare, and DCR graphs as a way of modeling procedural processes with data support. This combination can be seen as either “adding declarative control-flow to CP-nets” or as “adding data-flow to declarative formalisms.” From the modeling perspective, the approach requires the user to be familiar with three formalisms, as opposed to our framework where all aspects are represented within a single logical language. The authors do not provide a precise formalization of the combination of the three languages, so it is unclear how certain elements such as atomic transactions, hierarchical definitions of tasks, and constraints over complex tasks can be expressed in the combination of those three languages. From the analysis point of view, the authors address the problem of simulation: checking whether a transition is enabled in the CP-net model, and subsequently whether it is also allowed according to the declarative constraint. This is done using model checking. Our approach differs conceptually in that we rely on a logical proof theory as opposed to model checking.

In the same spirit of extending Declare with data elements, [33] extends the Declare notation by allowing activities to have associated multiple ports (denoting events associated to the activity lifecycle) and constraints to be attached to ports thereby allowing data-aware conditions. These extensions are then formalized in the Event Calculus (EC). In terms of modeling, the focus remains on modeling service flow exclusively in terms of constraints and this does not address the aforesaid limitations with respect to control and data flow (e.g., it is unclear how elements such as hierarchical definitions of tasks can be achieved with the proposed extensions). For reasoning, the paper defers to generic EC reasoners, which are significantly more complicated than those for CTR.

Another related approach to service modeling and verification is based on the business artifact model [16,19,29]. In this approach, tasks (which they call “services”) are represented as transformations on objects, called artifacts and they have pre- and post-conditions. In addition, various constraints can be specified using Linear Temporal Logic (like Declare) where first-order statements are allowed in place of propositions. In ServLog, artifact-based systems correspond to a very special form of service processes of the following form: $$\begin{array}{l}\begin{array}{cc}\hfill \mathit{serv}\mathrm{(}?\mathit{X}\mathrm{)}\leftarrow & \mathit{termination}\text{\_}\mathit{condition}\mathrm{(}?\mathit{X}\mathrm{)}\hfill \\ \hfill \mathit{serv}\mathrm{(}?\mathit{X}\mathrm{)}\leftarrow & {\mathit{precond}}_1\mathrm{(}?\mathit{X}\mathrm{)}\otimes {\mathit{task}}_1\mathrm{(}?\mathit{X}\mathrm{,}?\mathit{Y}\mathrm{)}\hfill \\ \hfill & \otimes {\mathit{postcond}}_1\mathrm{(}?\mathit{X}\mathrm{,}?\mathit{Y}\mathrm{)}\otimes \mathit{serv}\mathrm{(}?\mathit{Y}\mathrm{)}\hfill \\ \hfill \mathit{serv}\mathrm{(}?\mathit{X}\mathrm{)}\leftarrow & {\mathit{precond}}_2\mathrm{(}?\mathit{X}\mathrm{)}\otimes {\mathit{task}}_2\mathrm{(}?\mathit{X}\mathrm{,}?\mathit{Y}\mathrm{)}\hfill \\ \hfill & \otimes {\mathit{postcond}}_2\mathrm{(}?\mathit{X}\mathrm{,}?\mathit{Y}\mathrm{)}\otimes \mathit{serv}\mathrm{(}?\mathit{Y}\mathrm{)}\hfill \end{array}\\ \cdots \end{array}$$

The artifacts are represented here via variables, but they can also be represented as data items passed around via the underlying database. While the control structure of artifact systems is a small subset of what ServLog services can have, the constraints used in those systems form a superset of the constraints in ServLog: they can be arbitrary LTL formulas. (It is not clear, however, whether this generality makes a difference in practice.) It is interesting to note that the decidability results from [19] carry over from artifact systems to the special case of the ServLog service processes described above and thus give us a decidable subset of Transaction Logic that is different from the one mentioned in Section 5.3.

An emerging area related to our work is that of compliance checking between business processes and business contracts. For example, in [25,26] both processes and contracts are represented in a formal language called FCL. FCL is based on a formalism for the representation of contrary-to-duty obligations, i.e., obligations that arise when other obligations are violated as typically happens with penalties embedded in contracts. Based on this, the authors give a semantic definition for compliance, but no practical algorithms. In contrast, ServLog provides a proof theory for verifying feasibility of service contracting as well as for contract execution.

Several other approaches to service contracting and contract execution are relevant to our work [2,3,5,14], but not directly related. Most of these present logical modeling languages for contracts in various settings. Being based on normative deontic notions of obligation, prohibition, and permission, we believe that these works are complementary to ours and the approaches could be combined.

Other popular tools for process modeling are based on Petri nets, process algebras, and temporal logic. A related area of research is data-centric business and service modeling and verification, for which a representative approach is [47]. Approaches in this area primarily combine databases and model checking techniques for the purpose of automated verification. The advantage of CTR over these approaches is that it is a unifying formalism that integrates a number of process modeling paradigms ranging from conditional control flows to data flows to hierarchical modeling to constraints, and even to game-theoretic aspects of multiagent processes (see, for example, [18]). Moreover, as shown in [17], CTR modeling sometimes leads to algorithms with better known complexity for special cases than general model checking.

Finally, it is worth mentioning our work in the context of general AI techniques on reasoning about actions. A key differentiation of our approach based on CTR is that, while many works in AI focus on reasoning about actions, CTR also has constructs for defining transactions and executing them. These issue and further comparison are discussed in detail in the original and follow-up papers [6,9–11,37].

7. Conclusions

The main contribution of this paper is ServLog, a unifying logical framework for semantics-aware services addressing two core aspects of services: modeling and contracting. In particular, this work adds a few new building blocks to the theoretical foundations for service contracting. It offers an expressive set of modeling primitives and addresses a wide variety of issues in service contracts. These primitives range from complex process description (including iteration and conditional transitions between tasks) to temporal and data constraints. Despite its expressive power, ServLog still provides a reasoning procedure for automated service contracting.

In the context of established business process languages (e.g., BPMN, WS-BPEL), ServLog not only captures typical procedural constructs found in such languages, but also greatly extends them, enables declarative specification and reasoning, and opens the way for automatic generation of business processes from service contracts. Furthermore, in the context of Semantic Web Services, ServLog complements established approaches such as OWL-S and WSMO, which primary focused on semantic annotations for Web services, and brings new directions for research in Semantic Web Services related to service contracts.

The approach presented in this paper has been implemented for the propositional case (when tasks do not have parameters) in the GEECoP (Graphical Editor and Engine for Constrained Processes)14

¹⁴

http://sourceforge.net/projects/gecop/.

tool with promising results (further described in [44]).

Future work may include support for reasoning about quality of service (QoS) and non-functional properties in service contracts – see, e.g., [15] for an example of a framework for QoS-based Web service contracting, which could be combined with ServLog, and a more complete implementation of the reasoning framework based on recent results on efficient implementation of Transaction Logic [21]. Another challenging issue is generation of service contracts in ServLog from informal, often ambiguous, natural language contracts. It would be also interesting to do a methodological comparison of the expressive power of ServLog with workflow specification languages based on automata, pre/post conditions, and temporal constraints. In this respect, the recent framework introduced in [1] for comparing distinct workflow models by means of views might be relevant. Explicitly treating violations and reasoning about the effects of violations in contracts is also an interesting direction for further research in ServLog. Service discovery is complementary to the problem of service contracting addressed by ServLog. Some approaches to semantic service discovery are based on Transaction Logic (e.g. [30]) and could be combined with ServLog. Such a combination would be yet another intriguing continuation for the present work. ServLog, as a logical framework for specification of and reasoning about service contracts, is orthogonal to implementation issues such as centralized or distributed provisioning of services. ServLog can be instantiated in different settings; for example, when different tasks are provisioned in a distributed or decentralized environment. Studying the implications of instantiating ServLog in different environments is interesting from a practical perspective. We are also investigating applicability of ServLog and CTR to other areas such as smart contracts15

¹⁵

http://szabo.best.vwh.net/smart_contracts_idea.html.

in the context of cryptocurrencies.16

¹⁶

See for example Bitcoin contracts at https://en.bitcoin.it/wiki/Contracts.

Here, ServLog could prove to be a useful approach for modeling and reasoning about distributed cryptocurrency contracts.17

¹⁷

For a relevant related idea, see [4], where the authors proposed timed automata for formalizing Bitcoin contracts.