Complexity of synthesis of composite service with correctness guarantee  

作　　者：DENG Ting HUAI JinPeng WO TianYu 

机构地区：[1]State Key Laboratory of Software Development Environment,Beihang University Beijing 100191,China [2]School of Mathematics and System Science,Beihang University,Beijing 100191,China [3]School of Computer Science and Engineering,Beihang University,Beijing 100191,China

出　　处：《Science China(Information Sciences)》2012年第3期638-649,共12页中国科学（信息科学）（英文版）

基　　金：supported by National Basic Research Program of China (Grant No. 2011CB302602);National Nature Science Foundation of China (Grant No. 61103031);Project of NLSDE (Grant Nos. SKLSDE-2010-ZX-01, SKLSDE-2010ZX-03)

摘　　要：How to compose existing web services automatically and to guarantee the correctness of the design （e.g. temporal constraints specified by temporal logic LTL, CTL or CTL＊） is an important and challenging problem in web services. Most existing approaches use the process in conventional software development of design, verification, analysis and correction to guarantee the correctness of composite services, which makes the composition process both complex and time-consuming. In this paper, we focus on the synthesis problem of composite service; that is, for a given set of services and correctness constraint specified by CTL or CWL＊ formula, a composite service is automatically constructed which guarantees that the correctness is ensured. We prove that the synthesis problem for CTL and CTL＊ are complete for EXPTIME and 2EXPTIME, respectively. Moreover, for the case of synthesis failure, we discuss the problem of how to disable outputs of environment （i.e. users or services） reasonably to make synthesis successful, which are also proved complete for EXPTIME and 2EXPTIME for CTL and CTL＊, respectively.How to compose existing web services automatically and to guarantee the correctness of the design （e.g. temporal constraints specified by temporal logic LTL, CTL or CTL＊） is an important and challenging problem in web services. Most existing approaches use the process in conventional software development of design, verification, analysis and correction to guarantee the correctness of composite services, which makes the composition process both complex and time-consuming. In this paper, we focus on the synthesis problem of composite service; that is, for a given set of services and correctness constraint specified by CTL or CWL＊ formula, a composite service is automatically constructed which guarantees that the correctness is ensured. We prove that the synthesis problem for CTL and CTL＊ are complete for EXPTIME and 2EXPTIME, respectively. Moreover, for the case of synthesis failure, we discuss the problem of how to disable outputs of environment （i.e. users or services） reasonably to make synthesis successful, which are also proved complete for EXPTIME and 2EXPTIME for CTL and CTL＊, respectively.

关 键 词：business protocol composite service SYNTHESIS ENVIRONMENT branching temporal logic 

分 类 号：TP393[自动化与计算机技术—计算机应用技术] TP311.56[自动化与计算机技术—计算机科学与技术]