正确性保证的组合服务综合问题复杂度研究

被引：1

作者：

邓婷 ^{[1
,2
]}

怀进鹏 ^{[1
,3
]}

沃天宇 ^{[1
,3
]}

机构：

[1] 国家软件开发环境重点实验室

[2] 北京航空航天大学数学与系统科学学院

[3] 北京航空航天大学计算机学院

来源：

中国科学:信息科学 | 2012年 / 42卷 / 07期

关键词：

业务协议; Web服务; 组合服务; 综合; 环境; 时态逻辑;

D O I：

暂无

中图分类号：

TP393.09 [];

学科分类号：

摘要：

Web服务应用中一个富有挑战性的关键问题是:如何自动组合已有的Web服务并保证组合的正确性(如以时态逻辑LTL,CTL,CTL*等公式规范的时态性质).现有研究工作大多延用传统软件开发中的设计、验证、分析和纠错的过程,这使得组合过程既复杂又低效.文中研究了基于CTL与CTL*的组合服务综合问题,即利用已有Web服务自动生成满足给定的CTL,CTL*逻辑公式的组合服务,从而可以无需另外的验证过程,避免反复进行组合.证明了以CTL与CTL*逻辑公式为组合需求时,组合服务综合问题分别为EXPTIME–完全和2EXPTIME–完全问题.同时讨论了当综合失败时,如何通过合理限制环境(即服务的交互对象,如用户或其他服务)的输出使得综合成功,并证明了该问题关于CTL与CTL*逻辑公式同样分别为EXPTIME–完全和2EXPTIME–完全问题.

引用

页码：789 / 802

页数：14

共 6 条

[1]

An automata-theoretic approach to branching-time model checking [J].

Kupferman, O ;

Vardi, MY ;

Wolper, P .

JOURNAL OF THE ACM, 2000, 47 (02) :312-360

[2]

Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin; McNaughton and Safra.[J].David E. Muller;Paul E. Schupp.Theoretical Computer Science.1995, 1

[3]

A Deductive Approach to Program Synthesis.[J].Zohar Manna;Richard Waldinger.ACM Transactions on Programming Languages and Systems (TOPLAS).1980, 1

[4]

AutoSyn:A new approach to automated synthesis of composite web services with correctness guarantee.[J]..Science in China(Series F:Information Sciences).2009, 09

[5]

用描述逻辑进行语义Web服务组合 [J].

王杰生 ;

李舟军 ;

李梦君 .

软件学报, 2008, (04) :967-980

[6]

基于Petri网的Web服务自动组合研究 [J].

钱柱中 ;

陆桑璐 ;

谢立 .

计算机学报, 2006, (07) :1057-1066

← 1 →