描述Web服务的一阶动态逻辑

摘要

Web服务有几种形式化表示:WSMO(Web服务建模本体)和OWL-S(Web服务本体语言).为了分析WSML的逻辑特性,提出用一阶动态逻辑来表示WSML.这里的一阶动态逻辑与传统的PDL不同,后者是用来表示程序改变变量的动态性质的,而描述Web服务的一阶动态逻辑除了描述改变变量的程序动作的动态性质之外,还需要描述改变关系的服务动作的动态性质.给出了描述Web服务的PDL的语法和语义,并且用一个例子说明了PDL是如何表示Web服务的静态属性和动态属性的,以及改变变量和改变关系的动作的动态性质.%There are several formalizations of Web services: WSMCK Web Service Modeling Ontology) and OWL-S(Web Ontology Language for Services). To analyze the logical properties of WSML;we represented WSML in a predicate dy namic logic;where the predicate dynamic logic is different from the traditional PDL which is designed to represent dy namic properties of programs which change the assignments of variables;and the predicate dynamic logic for Web ser vices is designed to represent dynamic properties of services which change the relations. We gave the syntax and seman tics of the PDL for Web services;and an example to show how to represent the static and dynamic properties of Web services.