时态认知逻辑CTL＊K的符号化模型检查算法

时序认知逻辑是由时序逻辑和认知逻辑组合而成的逻辑,主要应用于多主体系统的规范定义.大多数时序认知逻辑是基于CTL的,表达能力有限.并且已知的一些模型检查算法存在内存不足和状态爆炸等问题.讨论了基于CTL*的时态认知逻辑cTL*K的语法、语义和模型,它能够在表达力很强的时态逻辑CTL*基础上描述智能体的知识、目标等意向特征.并给出了CTL*K的模型检查算法,其核心思想就是将CTL*K公式的检查问题转化为CTL*公式的模型检查问题,可以使检查的系统规模得以大幅度提高.并且将算法编码后容易集成到NuSMV模型检查器.     

有界模型检测同步多智体系统的时态认知逻辑

提出在同步的多智体系统中验证时态认知逻辑的有界模型检测(bounded model checking,简称BMC)算法.基于同步解释系统语义,在时态逻辑CTL*的语言中引入认知模态词,从而得到一个新的时态认知逻辑ECKL_n.通过引入状态位置函数的方法获得同步系统的智能体知识,避免了为时间域而扩展通常的时态认知模型的状态及迁移关系编码.ECKL_n的时态认知表达能力强于另一个逻辑CTLK.给出该算法的技术细节及正确性证明,并用火车控制系统实例解释算法的执行过程.     

基于时态认知逻辑的Web服务模型检测

传统模型检测技术主要采用时态逻辑描述被验证的规范,人们较少注意多智能体认知逻辑的模型检测问题.而在分布式系统领域,系统和协议的规范很适合用认知逻辑来描述.Web服务是一个典型的分布式系统.把Web服务组合建模为多智能体系统,并成功采用我们实现的时态认知逻辑符号模型检测工具MCTK验证了SAS股票分析服务实例.同时采用WSAT,WS-Engineer和SPIN 3个模型检测工具在相同实验环境下验证了该实例,实验结果表明我们的Web服务模型检测方法不仅比这3个模型检测工具更高效,而且支持认知逻辑规范的验证,这是这3个模型检测工具所不具备的.     

时态逼近关系及时态逻辑的扩充

本文提出了时态逼近关系，并给出了命题不确定性时态关系的一种分类，在Ｓｈｏｈａｍ的时态逻辑基础上，对命题和一阶两种情况，提出了能描述不确定性时态关系，基于时间点和（点对构成的）时间区间的时态逻辑（定性与定量相结合）．此外，还给出了在非确定性时态关系下用于描述命题类型的一些命题时态性质．     

智能主体的信念认知时态子结构逻辑模型*

智能主体获取信念的途径主要有两种：一种为他省,通过外界交互,从其他主体获取信息;另一种为自省,通过自己的历史数据库获取相关知识。对于主体信念的描述与刻画,两种途径缺一不可,但当前的BDI理论模型中较多地为他省系统,没有做到两者相结合。其次,在当前的许多理论模型中,通常使用的是二值逻辑、经典模态逻辑或其变形系统,使得相应的逻辑系统普遍存在逻辑全知和粗精度刻画等问题。针对上述问题进行了相关研究,采用了认知时态子结构逻辑建模的方法,表达了智能主体获得“双省”信念的方式,针对其建立了相应的逻辑系统BSoET。     

间断区间时态逻辑的语义

区间逻辑不能模拟自然语言中与,或,非时态关系,其公理系统的完备性不易保证。我们建立的间断区间时态知脚注可以克服区间逻辑的上述缺点,本文给出了间断区间逻辑的语法,语义及公理,即描述了间断区间时态逻辑的语义。     

基于时态的模糊描述逻辑初探

针对现实生活中,有许多的信息都是具有时间属性并且带有模糊、不精确的特点,在时态逻辑和模糊描述逻辑基础上,利用vager集概念,对基于时态的模糊描述逻辑系统进行了初步的研究,并给出了时态模糊描述逻辑的语法和语义的相关说明.与模糊描述逻辑FALC相比,该系统的提出在一定程度上弥补了FALC作为语义Web逻辑基础在表达时序上的空白.     

描述逻辑SHIOQ的时态扩展

分析描述逻辑时态扩展的优缺点,同时结合实际应用需求,将时间当作具体领域加入到描述逻辑中来处理,给出带时态扩展的描述逻辑SHIOQ（T）的形式化描述,并给出SHIOQ（T）中概念、关系和实例的描述形式以及它们的语义解释,从而方便地实现时态知识的表达和推理。     

Agent系统的一种面向角色的一阶分支时态逻辑

介绍了多Agent系统的ORGSTRUC模型,定义了角色模型、角色提供的服务以及角色间通信概念并对其形式化.首先对组织结构作出形式定义,该定义建立在角色和角色间关系的基础之上,比从Agent层次建模具有更高的抽象度,因此更适合于系统早期的分析和设计工作.在此理论基础上,提出了RASBTL逻辑来描述MAS在角色层面上的运行特性,考虑到组织结构在系统分析和设计时的重要的指导和规范作用,整个形式语言有助于对多agent系统的分析和设计.     

An Interpretation of Default Logic in Minimal Temporal Epistemic Logic

When reasoning about complex domains, where information available is usually only partial, nonmonotonic reasoning can be an important tool. One of the formalisms introduced in this area is Reiter's Default Logic (1980). A characteristic of this formalism is that the applicability of default (inference) rules can only be verified in the future of the reasoning process. We describe an interpretation of default logic in temporal epistemic logic which makes this characteristic explicit. It is shown that this interpretation yields a semantics for default logic based on temporal epistemic models. A comparison between the various semantics for default logic will show the differences and similarities of these approaches and ours.     

多视点间不一致性的认知推理

需求工程可以认为是一个知识表示,知识获取和知识分析的过程.多视点需求工程就是希望复杂系统中的不同参与者分别从自己的角度出发对预期系统进行描述,从而形成更完备的需求规约.由于多视点方法的这种特性,导致多个涉众有可能对同一问题进行描述,从而形成重叠的需求.这些重叠的需求就是涉众之间的公共知识,对公共知识的不同解释是导致需求规约中不一致问题的根源.本文对基于问题域的多视点需求建模框架进行基于时序认知逻辑的解释和推理,期望达到以下目的:1)使用户陈述的需求更加结构化;2)使用形式化的方法帮助涉众发现那些重叠的需求.     

Temporal Languages for Epistemic Programs

This paper adds temporal logic to public announcement logic (PAL) and dynamic epistemic logic (DEL). By adding a previous-time operator to PAL, we express in the language statements concerning the muddy children puzzle and sum and product. We also express a true statement that an agent’s beliefs about another agent’s knowledge flipped twice, and use a sound proof system to prove this statement. Adding a next-time operator to PAL, we provide formulas that express that belief revision does not take place in PAL. We also discuss relationships between announcements and the new knowledge agents thus acquire; such relationships are related to learning and to Fitch’s paradox. We also show how inverse programs and hybrid logic each can be used to help determine whether or not an arbitrary structure represents the play of a game. We then add a past-time operator to DEL, and discuss the importance of adding yet another component to the language in order to prove completeness.     

Compositional Verification of Multi-Agent Systems in Temporal Multi-Epistemic Logic

Compositional verification aims at managing the complexity of theverification process by exploiting compositionality of the systemarchitecture. In this paper we explore the use of a temporal epistemiclogic to formalize the process of verification of compositionalmulti-agent systems. The specification of a system, its properties andtheir proofs are of a compositional nature, and are formalized within acompositional temporal logic: Temporal Multi-Epistemic Logic. It isshown that compositional proofs are valid under certain conditions.Moreover, the possibility of incorporating default persistence ofinformation in a system, is explored. A completion operation on aspecific type of temporal theories, temporal completion, is introducedto be able to use classical proof techniques in verification withrespect to non-classical semantics covering default persistence.     

Probabilistic Dynamic Epistemic Logic

In this paper I combine the dynamic epistemic logic ofGerbrandy (1999) with the probabilistic logic of Fagin and Halpern (1994). The resultis a new probabilistic dynamic epistemic logic, a logic for reasoning aboutprobability, information, and information change that takes higher orderinformation into account. Probabilistic epistemic models are defined, and away to build them for applications is given. Semantics and a proof systemis presented and a number of examples are discussed, including the MontyHall Dilemma.     

一种带传递关系的认知描述逻辑研究

描述逻辑是语义Web的逻辑基础,它是形式化表达领域知识的一种工具.描述逻辑是一阶逻辑的可判定子集,适合对领域知识的概念术语进行建模.因为某些应用程序的需要和领域知识难以完全描述的因素,Web上有大量的不完全知识.描述逻辑基于开放世界假设,只能表达单调推理,不能处理不完全知识.在描述逻辑中加入认知运算符K可以得到认知描述逻辑.认知描述逻辑因其非单调特性和良好的时间复杂度等特点在处理不完全知识方面有较好的优势.在认知描述逻辑ALCK的基础上加入传递关系属性提出了新的认知描述逻辑语言ALCKR+,保留了描述逻辑原有的优点,增强了表达能力并通过认知查询拥有了非单调推理的能力.设计了ALCKR+的语法、语义以及表算法,给出了表算法的正确性以及可判定性证明,证明表算法的时间复杂度为PSPACE-tomplete.     

有关知道逻辑和“知道”问题的探讨

本文阐述了知道逻辑与“知道”问题之间的关系,介绍了解决知道问题的各种方法。