1. Introduction

A key aspect in Web services behavior (described by services choreography) is contracting them to (i) make all parties compatible, (ii) guarantee expected QoS parameters, and (iii) ensure every participating service to terminate in a correct state. It is generally accepted that semantic Web services (SWS) should be based on a formalism with a well-defined model-theoretic semantics, particularly, on some sort of logics [2]. Given that DLs are usually considered as the underpinning of many W3C standard languages, it is quite natural and promising to resort to a variant of DLs to model a semantic Web services contract (SWSc). Our present work extends the classical DLs with concrete domain and action theory, which makes it feasible to integrate planning and process modeling into DLs yet still retain decidable reasoning ability.

2. The Framework

Intuitively, there exist multiple-parties constraints of web services in a SWSc, which bring to existing DLs more challenges. In particular, we consider the following aspect(s):

A1. The actions specified by a services contract are required to be coordinated (e.g., ordered) and all the constraints need to be represented. Meanwhile, the underlying logic should also retain the decidable reasoning ability for all the represented "knowledge". The case of possessing sufficient expressive power for establishing QoS requirements is also analogous.

Example 1. Consider the motivation example as in Figure 1. Apparently, the completion of a deposit by the user should precede the computer delivery, which is followed by the completion of the entire payment. Moreover, the user must complete the entire payment within 12 hours after the computer delivery.

Figure 1: Motivating Example

Theoretically, combining original DLs with so-called "concrete domain" is a sound approach to satisfy the requirements as depicted in A1. However, [3] demonstrates that in the context of general TBoxes, if the concrete domain provides a unary predicate for equality with 0, a binary equality predicate, and a binary predicate for incrementation, then concept satisfiability and subsumption are undecidable. This result actually rules out the possibility of combining general TBoxes with more powerful concrete domains. In the sequel, we disallow general TBoxes in our framework but adopt acyclic TBoxes instead. The concrete domain in our framework sits on the basis of [3] and [4], and is defined as follows:

    

   
   

We denote our underlying logic as ALCQO(Q^*) with its syntax and Tarski-style semantics shown in Table 1 (f , g and U denote abstract feature, concrete feature, and feature path, respectively).

Theorem 1. (Decidability) An ALCQO(Q^*)-concept satisfiability is decidable.

Table 1. Syntax and Semantics of ALCQO(Q^*)

Example 1 revisited. At first, we introduce three types of concrete features: atTime, lBound, and rBound, whose intuitive meanings are the occurring time, the left and right bound of occurring time interval. We denote an abstract feature c_Deli as an abbreviation for computer delivery. Similarly, we denote c_Pay and interval as abbreviations for complete payment and the allowed time interval between c_Deli and c_Pay, respectively. Therefore, from the perspective of computer purchase service(CP), the interactions among these services can be specified as follows:

3. Action Theory

In this section, we start with providing some very practical scenarios to illustrate the significance of actions.

A2. The so-called "state of the world" (SoW) is generally assumed to be altered through invoking a service operation, viz. the SoW for a services contract is not permanent. If the underlying logic can entail the current state of a contract, the effect produced by an action should also be entailed by the "updated" SoW.

Example 2. Consider again the CP service. If the computer delivery is executed successfully, it will cause some effect to the other involved parties, e.g. the computer ownership will be changed. Therefore, the preconditions of next action should be satisfied, otherwise the entire services contract may be blocked at certain state. Meanwhile, it also needs to ensure that the contract can actually enter into some expected state eventually.

Our action theory is based on [1]. Considering the main features of semantic Web services, an action is defined as follows:

   

   
   

Example 3. Consider an ABox as {user(peter), hasDeposit(peter,A1),amount(A1,amt), =1000(amt), computer(L3YG), vendor(CP), own(CP,L3YG), bank(Deutsche), affiliated(A1,Deutsche)}, and action computer delivery can be described as follows (input and output are omitted for simplicity):

Definition 3. A Semantic Web Services contract (SWSc) is represented as a triple SC =< T, A, ACT > such that:

(1). T corresponds to a terminology box (TBox) in DLs, which describes the skeleton of the contract.
(2). A stands for an axiom box (ABox).
(3). ACT describes all the legal actions to be executed in SC. These actions can "drive" a contract’s state to be transitioned.

Intuitively, T plays the role of orchestrating a set of specified actions, A represents the current state of the entire contract, and ACT provides the descriptions of a set of actions. The interplay among them is thus obvious and natural, since TBoxes coordinate the action set, and ABoxes can be updated through the execution of an action. The formal semantics of our SC is defined as follows:

In our framework, we consider state transition as ABox updates, i.e. if a SC enforces an action successfully, it is regarded as updating the ABox from the current state to a new state. Based on the above definitions, we can obtain the following lemma.

Lemma 1. (Indeterminism) The update result of an ABox after an action is applied is indeterministic, i.e. there may exist more than one possible state to be the consequence of an update.

Lemma 2. The amount of possible consequent states through applying an action to the current state is finite.

Due to the decidability of ALCQO(Q^*) itself and the finite consequent states due to ABoxes updating strategy, we can obtain:

Theorem 2. (Well-defined) Given a services contract SC, checking its consistency, executability, and projection is decidable.

4. Conclusion And Future Work

In this paper, we restrict the underpinning of our framework to a comparatively simple yet quite expressive Description Logic, viz., ALCQO. Meanwhile, we have incorporated concrete domain and action theory into ALCQO, so as to equip it with the abilities to describe, coordinate, and trace the dynamic behaviors of all involved parties.

In future, we will try to work out the tight complexity bounds of action reasoning, and implement some practical algorithms.

5. References

[1] F. Baader, C. Lutz, M. Milicic, U. Sattler, and F. Wolter.Integrating Description Logics and Action Formalisms: First Results. In Proc. AAAI 2005, pages 572–577, July 2005.

[2] H. Davulcu, M. Kifer, and I.V.Ramakrishnan. CTR-S: A Logic for Specifying Contracts in Semantic Web Services. In Proc. WWW 2004, pages 144–153. ACM, May 2004.

[3] C. Lutz. Description Logics with Concrete Domains - A Survey. Advances in Modal Logic, 4:265–296, 2003.

[4] C. Lutz. Combining interval-based temporal reasoning with general tboxes. Artificial Intelligence, 152(2):235–274, 2004.