A Business Process (BP) is constituted by (i) data that describes the state of affairs and (ii) a set of activities (to be performed) over this data. The activities, when combined in what is usually referred to as an execution flow, achieve some business goal. When analyzing BPs, one is usually interested in querying possible execution flows to extract useful information and verifying dynamic properties over them.1 To this effect, BPs are typically modeled via high-level specifications of activities [17], which are later compiled into an executable code. Since the logics of business processes is captured by these specifications, tools for querying and analyzing possible execution flows are extremely valuable for companies [11,12,16]. Fully taking into account the presence of data significantly complicates the analysis of execution flows since it makes the system to be an infinite state one in general. On the other hand, it is often assumed that the data is simple enough and does not significantly impact on the analysis of possible execution flows. For these reasons, in the classical modeling paradigm of BPs, the data part is typically abstracted away, and the analysis is carried out under this simplification. In knowledge-intensive applications, however, where a crucial aspect of BPs is to properly represent the allowed evolutions of the data component, the classical modeling paradigm is not appropriate and one has to take fully into account data in the specification of BPs [14,13,20,1]. For example, in healthcare systems, an electronic record of a patient is the “data” to be manipulated by a process, and “activities” determine how to modify the patient's information (e.g., the registration of patient examination results). In this application scenario it is inappropriate to abstract away from patient records in process specifications. Thus, there is a need for developing and studying formalisms in which both the data component and the process component are first-class citizens. A number of recent proposals follow this approach [9,3,2], which is commonly referred to as Data-Centric Business Processes (DCBPs). The dynamic properties one is interested to verify are typically expressed in some variant of temporal logic, such as LTL, CTL, or the (first-order) -calculus [18,19], a very expressive temporal logic subsuming most of the other temporal formalisms. In the traditional BP setting, the verification of temporal properties is based on finite-state model checking [8]. However, in DCBPs, the presence of data makes the number of different states of the system potentially infinite. Hence, the verification of dynamic prop1 Note that this task is not trivial since, for instance, a given BP may have a large, possibly infinite, number of possible execution flows.
erties over DCPBs is complicated and represents a significant research challenge.
Indeed, neither finite-state model checking nor most of the current techniques for
infinitestate model checking [
In the following, we will present a simplified form of a DCPBs specification
language that is based on OWL 2 QL and that has been first introduced and studied in [
A Knowledge and Action Base (KAB) is a triple K = (T ; S0; ), where (i) T is a so-called TBox, i.e., a set of schema-level constraints representing the intensional-level knowledge about the domain of interest, (ii) S0 is a so-called ABox, i.e., a set of facts representing the initial information – the initial state of the system, and (iii) is a set of actions that specifies how the states of the system should evolve.
An action 2 is a set of effect specifications of the form qi(x) ; Si(x), where qi(x) is a query with output variables x expressed over (the alphabet of) T , and Si(x) is a set of atoms over (the alphabet of) T and x. The actions might acquire external information by means of service calls, which are modeled through function symbols.
We illustrate KABs on the following example.
Example 1. Consider the KAB Ke = (Te; S0; e) with e = f 1; 2g and Te = f(funct marriedTo); De v :Itg; S0 = fMarried(Mariano)g; 1 = CA [ fMarried(x) ; fmarriedTo(x; roG(x)); De(roG(x))gg; 2 = CA [ fMarried(x) ; fmarriedTo(x; roI(x)); It(roI(x))gg: where CA (which stands for “copy all”) is an operator that copies all the atoms of the current state to the new one. Intuitively, Te says that a person cannot have more than one spouse (the relation marriedTo is functional) and that Germans are not Italians (and vice-versa); the initial state S0 states that Mariano is married. Finally, e says that if a person, say x, is married (i.e., if Married(x) is satisfied) then one should explicitly add in the new state a fact about (i) the marriage of x , i.e., add marriedTo(x; ) atom to the new state, where the name of his/her spouse can be found via a service call in a registry office in Germany (by calling a service roG(x) as in 1), or in Italy (by calling a service roI(x) as in 2); and (ii) the nationality of the x’s wife, i.e., the wife is either German, according the action 1, or italian, according the action 2.
Intuitively, an application of an action to a state S returns a new state S0 defined
as follows. Starting from S0 = ;, for each action qi(x) ; Si(x) in , evaluate qi over
T [ S (using the certain answers semantics [
In our study of KABs, we focus on TBoxes expressed in the DL-Lite family of
description logics [
The execution flow associated with a KAB K = (T ; S0; ) is a graph G(K) whose nodes are states, reachable from S0 by “executing” actions from , and that are consistent with T . More formally, (S; S0) is an edge of G K ( ) if and only if (i) S0 can be obtained from S by applying some action 2 , and (ii) S0 [ T is a consistent KB. In Figure 1, left, there is a (fragment of) G(Ke) for Ke of Example 1. State 1 is initial and States 2-6 are reachable from it. Here we assume that States 2-5 are consistent with Te and State 6 is not; thus, State 6 is “rejected” from G(Ke) and there is no edge from State 3 to 6.
Example 3. Continuing with Example 2, the application of 2 to S1 yields the state
S2 = S1 [ fmarriedTo(Mariano; roI(Mariano)); It(roI(Mariano))g: We have that S2 [ T is inconsistent and hence S2 is rejected from G(Ke). The inconsistency comes from the fact that S2 includes both De(roG(Mariano)) and It(roI(Mariano)), which together with De v :It 2 Te leads to roG(Mariano) 6= roI(Mariano). At the same time, S2 contains both marriedTo(Mariano; roG(Mariano)) and marriedTo(Mariano; roI(Mariano)), and due to functionality of marriedTo in Te this yields that roG(Mariano) = roI(Mariano).
In [
In Example 3, the state S2 is rejected because some person would have to be both Italian and German, which contradicts the TBox. However, the inconsistency is caused only by a (small) portion of the ABox, and therefore it would be desirable not to lose the remaining consistent part and keep this state, repairing it beforehand. Indeed, it could be the case that the wife of Mariano used to be an Italian, but then she moved to Germany and changed her citizenship (or the other way around), while the information in the registry offices has not been updated. We do not have control over the offices, but we can repair the state correspondingly to the options we have, trying to remove the inconsistency while keeping at the same time as much information as possible. Example 4. The following states are possible repairs of S2 from Example 3: 1 Srep = froG(Mariano) = roI(Mariano); Married(Mariano);
De(roG(Mariano)); marriedTo(Mariano; roG(Mariano))g; 2 Srep = froG(Mariano) = roI(Mariano); Married(Mariano);
It(roI(Mariano)); marriedTo(Mariano; roI(Mariano))g: The repair Sr1ep represents the case when Mariano’s wife is German, and Sr2ep – Italian.
In Figure 1, right, we present a repair-based execution flow, where instead of rejecting the inconsistent State 6, we set as its successors its repairs, namely State 6a and State 6b, and continue to execute . 5
We are currently working on various aspects related to the specification of DCBPs and
KABs and the verification of temporal properties over them. The specific aspect that we
have discussed here, namely the adoption of a repair-based semantics to deal with the
inconsistencies arising in a state, is a particularly challenging direction. In particular, we
are interested in investigating how to extend to this new setting the decidability results
established for verification of -calculus properties over DCBPs [
This work is carried out within the EU project ACSI2, within which we are also studying uses-cases for KABs and implementing prototype verification tools. 2 http://www.acsi-project.eu/ Acknowledgements. This research has been partially supported by the EU under the ICT Collaborative Project ACSI (Artifact-Centric Service Interoperation), grant agreement n. FP7-257593.