基于动态时序描述逻辑的动作理论

动态时序描述逻辑(DLTLDL)是一类描述逻辑的动态时序扩展。提出一种基于DLTLALCIO的动态域建模方法,利用该方法可构造出刻画动态域知识的DLTLALCIO理论,并解决动作推理中的框架问题和分支问题。动作推理问题,如动作可执行性和投影问题等,可归结为关于DLTLALCIO理论的推理问题,并最终归结为DLTLALCIO的公式可满足性问题。DLTLALCIO公式可表达动作和时间约束,相对于其他基于描述逻辑的动作形式,基于DLTLALCIO的动作形式在需要执行复杂查询,尤其是含时间或动作的查询的应用场合具有更好的适用性。     

基于动态描述逻辑的语义Web服务推理

语义Web服务的提出是为了解决Web服务资源在语义Web中的自动发现、组合和执行等问题,基本思路是将本体承载的静态知识与对Web服务动态功能的描述有机地结合起来.动态描述逻辑是描述逻辑的一种动态扩展,支持面向语义Web的对动作的描述和推理.文中利用动态描述逻辑DDL(SHOIN(D))的描述和推理功能,提出对语义Web服务进行建模和推理的一种有效途径.从OWL-S中的Process Model出发,将语义Web服务建模为基于DDL(SHOIN(D))的动作理论,其中,对应于Process Model中的原子过程,可以对输入、输出、局部变量、前提条件、结果等多个方面进行建模;对应于Process Model中的复合过程,可以相应地对数据流以及顺序、选择、乱序、条件、迭代、循环等控制结构进行刻画.以建模后得到的动作理论为基础,应用动态描述逻辑的推理机制,可以分别对语义Web服务的可实现性、可执行性、投影、规划等问题进行推理.这些推理功能为语义Web服务的自动发现和自动组合提供了有效的支持.     

一类扩展的动态描述逻辑

作为描述逻辑的扩展,动态描述逻辑为语义Web服务的建模和推理提供了一种有效途径.在将语义Web服务建模为动作之后,动态描述逻辑从动作执行结果的角度提供了丰富的推理机制,但对于动作的执行过程却不能加以处理.借鉴Pratt关于命题动态逻辑的相关研究,一方面,对动态描述逻辑中动作的语义重新进行定义,将每个动作解释为由关于可能世界的序列组成的集合;另一方面,在动态描述逻辑中引入动作过程断言,用来对动作的执行过程加以刻画.在此基础上提出一类扩展的动态描述逻辑EDDL(X),其中的X表示从ALC(attributive language with complements)到SHOIN(D)等具有不同描述能力的描述逻辑.以X为描述逻辑ALCQO(attributive language with complements,qualified number restrictions and nominals)的情况为例,给出了EDDL(ALCQO)的表判定算法,并证明了算法的可终止性、可靠性和完备性.EDDL(X)可以从动作执行过程和动作执行结果两个方面对动作进行全面的刻画和推理,为语义Web服务的建模和推理提供了进一步的逻辑支持.     

语义Web服务组合中的服务建模及规划算法

Web服务的语义建模是指对Web服务的属性、功能和结构等进行语义描述,使用户能够对服务自动地定位、选择、使用和组合.本文以动作理论和描述逻辑为基础对服务的逻辑层信息(控制流和数据流)进行语义建模,用带前提和结果的原子动作描述简单服务,复杂动作描述组合服务的控制流,服务间的依赖关系描述数据流,并提出一个基本的Web服务自动组合框架.在该框架中,Web服务自动组合被划分为逻辑层和实现层2部分,于是服务的自动组合问题在逻辑上归结为一个动作规划问题,在实现上归结为一个根据动作选择具体服务的服务选择问题.最后给出一种新的自动组合规划算法,该算法充分考虑了语义推理和智能规划的结合,在对问题的描述能力和运行效率上做了较好的平衡.     

CDDL:动态描述逻辑的不确定性扩展

本体(Ontology)是语义Web中共享知识的形式化建模工具,其逻辑基础是描述逻辑.动态描述逻辑(DDL)具有同时表示静态和动态知识的优势.本文针对语义Web需要处理不确定性动态知识的需求,利用云模型对DDL进行不确定性扩展,提出了一种能够有效实现不确定性静态和动态知识进行表示和推理的不确定性动态描述逻辑CDDL.与...     

一种采用一阶动态逻辑表示的数字权限描述模型

针对已有数字权限描述模型的动态语义描述能力较弱问题,提出了一个能够描述权限动 作状态的数字产品权限描述模型DDRM。基于一阶动态逻辑,定义了一个用于描述数字权限概念的 一阶动态逻辑符号系统DrFDL,并在DDRM模型基础上给出了DrFDL的语义结构(该语义结构能够 反映动作的动态特性)。基于DDRM模型还给出了一个表达权限证书的文法,应用DrFDL逻辑语言 给出了该文法生成的权限证书的形式语义,并探讨了该证书的确定性和有效性。     

一种基于扩展描述逻辑的事件实例检测方法

针对事件要素之间客观存在的语义关系以及事件与事件类之间的语义关系进行研究,提出了一种基于扩展描述逻辑的事件实例检测方法。该方法利用事件中的时间、动作、环境要素对事件进行语义补充,然后利用扩展描述逻辑中概念的可满足性和概念包含的推理功能对事件实例进行检测,最后通过实验证明该方法可实现文本中的事件实例检测,准确率达到了85．12％。     

UML2.0顺序图的时序描述逻辑语义

针对UML2.0顺序图用于对象间交互行为建模时存在动态语义缺乏精确形式化描述的问题,提出一种基于时序描述逻辑的UML2.0顺序图形式化方法。对描述逻辑进行时序扩展,得到可表示动态和时序语义的形式化规范——时序描述逻辑,根据UML2.0新增的交互操作符将UML2.0顺序图分成一个或多个最大顺序片段,通过形式化最大顺序片段和交互操作符得到UML2.0顺序图的时序描述逻辑语义。实例检验结果表明,该方法具有可行性。     

基于描述逻辑规则的语义Web服务组合

针对OWL-S语义Web服务自动组合问题,提出了一种基于描述逻辑(DL)规则的建模和组合方法.将ServiceProfile中的原子服务及其输入、输出参数分别建模DL中角色和概念,将概念间上下位关系和ProcessProfile中组合流程模型建模为DL规则,以一种统一的方式刻画语义Web服务的静态功能语义和动态交互特征...     

基于动态描述逻辑DDL的动作理论

基于一阶谓词逻辑或高阶逻辑的动作理论与采用命题语言的动作理论之间存在一个关于描述和推理能力的鸿沟;作为描述逻辑的动态扩展,动态描述逻辑DDL为基于描述逻辑的动作刻画和推理提供了一种途径.系统地研究了基于DDL的动作表示和推理问题.首先,在应用描述逻辑对静态领域知识进行刻画的基础上,引入带参数的原子动作定义式和带参数的复...     

动态描述逻辑的Tableau判定算法

动态描述逻辑在描述逻辑的基础上引入了动态维,用于描述和推理动态领域的知识,但目前缺少有效的判定算法作为支撑.文中以描述逻辑ALCO的动态扩展为例,构建出动态描述逻辑D-ALCO.以D-ALCO的构建过程为基础,将ALCO的Tableau算法、命题动态逻辑的Tableau算法以及对可能模型途径的处理有机地结合起来,给出了D-ALCO的Tableau判定算法,证明了算法的可终止性、可靠性和完备性.应用该算法,可以在采用开世界假设的情况下对D-ALCO中公式的可满足性进行判定.对于D-ALCQO、D-ALCQIO等具有更强描述能力的动态描述逻辑,可以对该算法扩展后得到相应的Tableau判定算法.     

Multi-Agent Dynamic Logics with Informational Test

This paper investigates a family of logics for reasoning about the dynamic activities and informational attitudes of agents, namely the agents' beliefs and knowledge. The logics are based on a new formalisation and semantics of the test operator of propositional dynamic logic and a representation of actions which distinguishes abstract actions from concrete actions. The new test operator, called informational test, can be used to formalise the beliefs and knowledge of particular agents as dynamic modalities. This approach is consistent with the formalisation of the agents' beliefs and knowledge as K(D)45 and S5 modalities. Properties concerning informativeness, truthfulness and preservation of beliefs are proved for a derivative of the informational test operator. It is shown that common belief and common knowledge can be expressed in the considered logics. This means, the logics are more expressive than propositional dynamic logic with an extra modality for belief or knowledge. The logics remain decidable and belong to 2EXPTIME. Versions of the considered logics express natural additional properties of beliefs or knowledge and interaction of beliefs or knowledge with actions. It is shown that a simulation of PDL can be constructed in one of these extensions.