Partial Deduction for Assisting Automated Semantic Web Service Composition

摘要

Industry has recently recognised the need for additional descriptions of Web services beyond those provided by WSDL documents and tModels in UDDI. These descriptions should facilitate discovery, integration and composition of Web services in a more efficient way than supported currently. This need sheds light to the progress on Semantic Web services as provided by initiatives like WSMO and OWL-S. By now many methods have been proposed for composing Web services automatically from existing OWLS and WSML-like Web service descriptions. The methods range from AI planning (Wu et al. 2003; McDermott 2002) to automated theorem proving (McIlraith & Son 2002; Rao, Kungas, & Matskin 2005) and graph search algorithms. However, the usability of these methods is greatly affected by two constraints. Firstly, it is assumed that developers provide consistent declarative descriptions of Web services. Secondly, it is assumed that there exists a universal set of atomic Web services, which would facilitate the composition of all other Web services. In this paper we are going to tackle these two issues. We apply partial deduction for identifying potential inconsistencies in Web service descriptions. Our method also determines atomic Web services, which should be implemented in order to compose a required composite Web service. We have earlier demonstrated (Rao, Kungas, & Matskin 2005) how linear logic (Girard 1987) (LL) theorem proving can be applied for automated Web service synthesis. At the same time we proposed a formalism (Kungas & Matskin 2005) of partial deduction (PD) for LL. While the former article (Rao, Kungas, & Matskin 2005) provides a process for automated Web service composition, the latter article (Kungas & Matskin 2005) provides a formalism for facilitating interactive composition. In this article we combine these results and propose heuristics for enhancing the Web service composition process. The heuristics determine how the system should perform if theorem proving would not lead to any composition. We apply LL theorem proving and PD for planning as proposed in (Kungas 2003). The generic Web services composition process is presented in Figure 1. First, a description of existing Web services is translated into extralogical axioms of LL, and the requirements to the composite services are specified in form of a LL sequent to be proven. Then LL theorem proving is applied to determine whether a composition can be found. If no composition is found, PD and gap detection are applied iteratively. While PD generates all possible gaps, gap detection selects most desirable ones according to a particular heuristic.