基于描述逻辑的模糊ER模型的表示与推理

重点分析了将ER模型分别转化为描述逻辑ALNUI知识库和DLR知识库的不同之处.在深入研究了描述逻辑DLR的基础之上,对DLR进行了模糊化扩展,提出了一种新的模糊描述逻辑FDLR(fuzzyDLR).定义了FDLR的语法结构、语义解释以及知识库的形式,研究了如何将模糊ER模型转化为FDLR的知识库.通过一个转化实例例证了FDLR能够很好地对模糊ER模型进行表示,并利用FDLR的推理机制研究了模糊ER模型的自动推理问题,同时给出了上述转化和推理问题的正确性证明.     

基于描述逻辑的模糊ER模型

分析了描述逻辑ALNUI与ER模型的关系,特别是如何将ER模型转化为ALNUI的知识库,从而利用ALNUI的推理机制对ER模型进行自动推理的有效性,在此基础上,进一步研究了基于描述逻辑的模糊ER模型.针对模糊ER模型的特点和需求,在描述逻辑ALNUI的基础上,对描述逻辑ALNUI进行了模糊化推广,提出了一种新的描述逻辑,即模糊描述逻辑FALNUI.研究了基于FALNUI的模糊ER模型,即研究了如何将模糊ER模型转化为FALNUI的知识库,并利用FALNUI的推理机制研究了模糊ER模型的可满足性、冗余性和包含关系等自动推理问题,证明了这些推理问题的正确性.     

基于描述逻辑的EER模型检测

首先分析基于描述逻辑的ER模型的研究现状,提出基于描述逻辑SHOIN(D)的EER模型,给出描述逻辑SHOIN(D)的语法和语义。然后研究EER模型的SHOIN(D)描述形式,以及如何将EER模型向SHOIN(D)知识库转化。最后给出EER模型可满足性、冗余性判定定理,证明了这些推理问题的正确性,并利用pellet推理机实现了EER模型可满足性和冗余性推理。     

模糊描述逻辑FALNUI的tableaux推理

分析了模糊描述逻辑FALNUI与模糊ER模型的关系,即模糊ER模型可以转化为FALNUI的知识库,并且模糊ER模型的可满足性、冗余性和包含关系等推理问题可以转化为FALNUI的包含推理问题,但FALNUI缺乏相应的推理算法.提出了一种基于描述逻辑tableaux的FALNUI的可满足性推理算法,证明了该推理算法的正确性,以及提出了FALNUI的Tbox扩展和去除方法,证明了FALNUI的包含推理问题可以转化为可满足性推理问题,并给出了FALNUI的包含推理算法.FALNUI的tableaux推理算法为模糊ER模型的可满足性、冗余性和包含关系等自动推理的实现提供了理论基础.     

带传递关系和存在量词的描述逻辑MSC推理

分析了描述逻辑非标准推理的重要性,特别分析了描述逻辑MSC推理的研究现状和存在的问题.针对目前描述逻辑MSC推理不能同时处理传递关系和存在量词的不足,研究了带传递关系和存在量词的描述逻辑εL+的MSC推理问题.提出了一种新的εL+-述图,利用描述树和描述图给出了描述逻辑εL+的MSC近似推理算法,并利用εL+-描述树同态和εL+-描述树描述图同态证明了MSC近似推理算法的正确性.作为一个附带的结果,利用εL+-描述树描述图同态给出了εL+的实例推理算法,也证明了实例推理算法的正确性.     

基于时序描述逻辑的UML状态图语义

将UML图形转换成形式化规范是一种精确UML语义、扩大形式化软件方法适用范围的有效途径。鉴于描述逻辑强的可判定推理能力,提出一种采用时序描述逻辑形式化UML状态图,对描述逻辑进行时序扩展,得到可以表示动态和时序语义的形式化规范——时序描述逻辑,给出一套UML状态图向时序描述逻辑表达式转换的规则,通过实例验证了该方法的可行性。     

基于SHOIN（D）的UML类图形式化方法

UML模型一致性自动检测的主要任务是解决形式化问题。描述逻辑是一阶谓词逻辑的可判定子集,具备强大的知识表示和推理功能。针对UML模型形式化问题,提出基于描述逻辑的形式化方法,分析UML类图各模型元素与描述逻辑SHOIN（D）的对应关系,提出UML类图的SHOIN（D）形式化方法,给出UML类图转换为SHOIN（D）知识库的正确性证明。     

一种分布式动态描述逻辑

分析了目前描述逻辑（DL）的研究现状和存在的问题，特别是动态描述逻辑（DDL）作为语义Web逻辑基础所存在的问题．针对语义Web的特点和需求，对DDL进行了扩充，提出了一种新的描述逻辑，即分布式动态描述逻辑（D3L），给出了D3L的语法和语义，并研究了D3L的推理机制，提出了两种推理方法：直接推理和转化推理．与动态描述逻辑DDL相比，该D3L可以为语义Web提供更为合理的逻辑基础，弥补了DDL作为语义Web逻辑基础的不足．     

基于最大不动点模型的描述逻辑系统FLε的有穷基

研究了描述逻辑的有穷基问题,分析了有穷基在描述逻辑中的重要意义及其研究现状,并研究了形式概念分析中的属性蕴舍和Duguenne-Guigues基问题.利用形式概念分析中Duguenne-Guigues基存在的证明结果,在F.Baader工作基础上设置了描述逻辑的描述背景,重新定义了描述背景下的属性蕴含,证明了带循环术语的描述逻辑系统FLε存在最大不动点语义(greatest fixed-points,gfp)模型,给出了带循环术语的描述逻辑系统FLε在最大不动点模型下的有穷基的存在性定理,并证明有穷基的可靠性和完备性.描述逻辑有穷基可以帮助知识工程师构建一个更适用于推理的描述逻辑知识库.     

带n-元存在量词的描述逻辑MSC推理

分析了描述逻辑非标准推理的重要性,特别分析了描述逻辑MSC(Most Specific Concept)推理的研究现状和存在的问题.针对目前描述逻辑MSC推理不能处理n-元存在量词的不足,研究了带n-元存在量词的描述逻辑εL(n)的MSC推理问题.提出了一种新的εL(n)一描述图,利用描述树和描述图给出了描述逻辑εL(n)的MSC近似推理算法,并利用εL(n)-描述树嵌套和εL(n)-描述树描述图同态证明了MSC近似推理算法的正确性.作为一个附带的结果,利用εL(n)-描述树描述图同态给出了εL(n)-的实例推理算法,也证明了实例推理算法的正确性.     

网络协议形式化模型的分析与应用

网络协议的形式化模型是协议分析和设计的核心技术之一。论文在简要分析当前的几种常用网络协议形式化模型之后,指出时序逻辑作为网络协议形式化模型的独特优越性,然后给出用一种线性时序逻辑MPTL描述IGMP协议的具体实例。     

DTL-Real-Time Object-Z形式化规格说明语言及其责任授权模型描述

Object-Z语言缺乏完整的时态描述能力,如无法表达操作在特定时间之后执行或按某种周期执行等,也不具有操作补偿等概念。针对这些问题,在Object-Z中集成实时概念和分布式时态逻辑,提出DTL-Real-Time Object-Z规格语言,该语言能有效地描述操作的时态驱动、事件驱动、操作补偿等因素,分析和说明了该语言的语法和语义,最后通过对责任授权模型的形式化描述说明了该语言的表达能力和应用。     

Tableau-based automata construction for dynamic linear time temporal logic*

We present a tableau-based algorithm for obtaining a Büchi automaton from a formula in Dynamic Linear Time Temporal Logic (DLTL), a logic which extends LTL by indexing the until operator with regular programs. The construction of the states of the automaton is similar to the standard construction for LTL, but a different technique must be used to verify the fulfillment of until formulas. The resulting automaton is a Büchi automaton rather than a generalized one. The construction can be done on-the-fly, while checking for the emptiness of the automaton. We also extend the construction to the Product Version of DLTL.*This research has been partially supported by the project MIUR PRIN 2005 ‘Specification and verification of agent interaction protocols’.     

时态描述逻辑ALC-LTL的Tableau判定算法

时态描述逻辑ALC-LTL将描述逻辑ALC的描述能力与线性时态逻辑LTL的刻画能力结合起来,在具有较强描述能力的同时还使得可满足性问题保持在EXPTIME-完全这个级别。针对ALC-LTL缺少有效的判定算法的现状,将LTL的Tableau判定算法与描述逻辑ALC的推理机制有机地结合起来,给出了ALC-LTL的Tableau判定算法并证明了算法的可终止性、可靠性和完备性。该算法具有很好的可扩展性。当ALC-工`I'I、中的描述逻辑从ALC改变为任何一个具有可判定性特征的描述逻辑X时,只需要对算法进行简单修改,就可以得到相应的时态描述逻辑X-LTL的Tableau判定算法。     

多智体系统时序认知规范的SPIN模型检测

SPIN模型检测器主要用来检测线性时序逻辑描述的规范,而多智体系统的规范采用时序认知逻辑描述比较方便。本文着重讨论了如何利用SPIN模型检测线性时序认知逻辑的方法,根据局部命题的理论,将模型检测知识算子和公共算子表述的规范规约为模型检测线性时序逻辑的问题,从而使SPIN的检测功能由线性时序逻辑扩充到线性时序认知逻辑。本文通过一个RPC协议分析实例来说明模型检测线性时序认知逻辑的方法。