一种求解认知难题的模型检测方法

用公告逻辑建模并求解和与积认知难题.提出一种动态认知模型,将环境认知模型与公告导致的认知模型线性组合,从而在时态认知逻辑模型检测技术中扩展支持公告逻辑的建模与验证.该模型检测方法不仅可以用于搜索认知难题的所有解,而且可以验证相关的时态认知性质,这一特性是当前认知逻辑模型检测工具MCK、MCMAS和DEMO不能完全支持的.作者采用OBDD开发了相关的符号化模型检测工具MCTK并对和与积难题进行建模和验证,实验结果说明了文中方法的正确性和高效性.     

符号化模型检测CTL

提出了一个关于时态逻辑CTL＊ 的符号化模型检测算法.该算法通过所谓的tableau构造方法来判定一个有限状态系统是否满足CTL＊规范. 根据该理论,作者已实现了一个基于OBDD技术的CTL＊符号化模型检测工具MCTK,并完成了相当数量的实验.到目前为止,已知有名的符号化模型检测工具,如SMV和NuSMV等, 都只能对CTL＊的子集逻辑（如CTL,LTL）进行检测,而文中算法的结果是令人满意的,并且当规范不是特别复杂时, 高效的CTL＊符号化模型检测是可能的.     

基于时态测试器的实时分支时态逻辑模型检测

基于自动机理论的模型检测技术在形式化验证领域处于核心地位, 然而传统自动机在时态算子上不具备可组合性, 导致各种时态逻辑的模型检测算法不能有机整合.本文为了实现集成限界时态算子的实时分支时态逻辑RTCTL*的高效模型检测, 提出一种RTCTL*正时态测试器构造方法, 以及相关符号化模型检测算法.证明了所提出的RTCTL*正时态测试器构造方法是完备的.也证明了该算法时间复杂度与被验证系统呈线性关系, 与公式长度呈指数关系.我们基于JavaBDD软件包成功开发了该算法的模型检测工具MCTK 2.0.0.我们完成了MCTK与著名的符号化模型检测工具nuXmv之间的实验对比分析工作, 结果表明MCTK虽然在内存消耗上要多于nuXmv, 但是MCTK的时间复杂度双指数级小于nuXmv, 使得利用MCTK验证大规模系统的实时时态性质成为可能.     

基于模糊自适应免疫算法的非线性系统模型参数估计

复杂生产工艺中非线性系统的模型参数估计是系统建模优化问题中的难点, 为避免优化算法过早收敛于错误的参数估计值, 根据生物免疫机理和模糊逻辑原理提出了一种新颖的模糊自适应免疫算法, 该算法采用混沌超变异操作增强算法搜索能力, 并用免疫网络调节策略保持抗体群的多样性, 同时采用模糊逻辑调节算法参数以提高算法的自适应能力. 函数优化仿真结果表明其具有较好的收敛性能, 并能够克服早收敛问题. 最后将其成功应用于重油热解非线性模型参数估计中, 验证了该算法解决实际建模问题的可行性和有效性.     

模糊计算树逻辑的符号模型检测

对含有模糊不确定性信息的系统进行模型检测时,状态空间爆炸问题成为了亟待解决的主要问题.将形式化的系统模型用拟布尔公式表示,用多终端二叉决策图来对拟布尔公式进行存储.对模糊计算树逻辑的不动点语义给出了解释和证明,然后给出模糊计算树逻辑的符号化模型检测算法,最后通过一个实例验证算法的正确性.该算法可有效缓解对模糊模型检测验证时的状态空间爆炸问题,并扩展了模型检测的应用范围.     

基于微粒群算法的非线性系统建模方法研究

针对非线性系统多模型自适应控制中的模型覆盖问题,提出一种基于微粒群算法的多模型建模方法.首先,对非线性系统定义了基于混合逻辑模型的多模型描述,建立了非线性系统的混合线性多模型;然后,基于微粒群优化算法对非线性系统进行优化建模,在保证建模准确性的同时采用最少的子模型逼近非线性系统;最后,通过一个仿真算例表明了该建模方法的有效性.     

工作流时序约束模型分析与验证方法

为了解决工作流时间建模与时序一致性验证问题,以时序逻辑和模型检查为基础,提出了一种工作流时间建模与时序一致性验证方法.该方法用一阶逻辑描述工作流模型及其时间信息,用时序逻辑描述工作流的时序约束,用模型检查算法对时序约束进行验证与分析.该方法不是针对某一种时序约束提出来的,而是能够验证任何用时序逻辑描述的工作流时序约束.该方法还能够对未通过验证的时序约束提供工作流运行实例作为反例,帮助用户定位模型的问题.以一个工作流时间建模和时序一致性验证的实例证实了所提出方法的有效性.     

大型Web站点逻辑域挖掘算法

通过进一步发展Wen-Syan Li等人提出的Web站点逻辑域理论,该文提出Web站点逻辑域核模型及建立在其上的逻辑域挖掘算法。该算法通过对Web站点超链接的图结构进行运算,得到Web站点逻辑域。与Wen-Syan Li算法对比测试,结果表明在获得相同逻辑域个数的情况下,克服了其采用启发式方法所带来的效率问题。在对4个大型Web站点的单独测试中,平均能够达到85%的逻辑域挖掘精度。     

基于模糊白适应免疫算法的非线性系统模型参数估计

复杂生产工艺中非线性系统的模型参数估计是系统建模优化问题中的难点,为避免优化算法过早收敛于错误的参数估计值,根据生物免疫机理和模糊逻辑原理提出了一种新颖的模糊自适应免疫算法,该算法采用混沌超变异操作增强算法搜索能力,并用免疫网络调节策略保持抗体群的多样性,同时采用模糊逻辑调节算法参数以提高算法的自适应能力．函数优化仿真结果表明其具有较好的收敛性能,并能够克服早收敛问题．最后将其成功应用于重油热解非线性模型参数估计中,验证了该算法解决实际建模问题的可行性和有效性．     

基于可靠性图的可靠性评估算法的研究

对可靠性评估算法的研究是可靠性研究的重要组成部分.在已有工作的基础上,提出了一种改进的建模方法是N-存在门逻辑的可靠性模型.该模型同时考虑到门逻辑关系和组件间的依赖对系统可靠性的影响,并给出了一个统一的算法思想.该算法与存在门逻辑的可靠性图方法进行了纵向对比,与COBAREA方法进行了横向对比,对比结果表明了该算法可有效地计算出系统的可靠性,且精确度更高.     

A first-order coalition logic for BDI-agents

Coalition logic (CL) enables us to model the strategic abilities and specify what a group of agents can achieve whatever the other agents do. However, some rational mental attitudes of the agents are beyond the scope of CL such as the prestigious beliefs, desires and intentions (BDI) which is an interesting and useful epistemic notion and has spawned substantial amount of studies in multi-agent systems. In this paper, we introduce a first-order coalition BDI (FCBDI) logic for multi-agent systems, which provides a semantic glue that allows the formal embedding and interaction of BDI, coalition and temporal operators in a first-order language. We further introduce a semantic model based on the interpreted system model and present an axiomatic system that is proved sound and complete with respect to the semantics. Finally, it is shown that the computational complexity of its model checking in finite structures is PSPACE-complete.     

多Agent信念逻辑及其在概率意义下的推广

首先建立了一种多Agent信念逻辑MBL(multi-agentbelieflogic),在经典信念逻辑基础上增加了普遍信念算子和公共信念算子,给出MBL的Kripke语义与广义Aumann语义,讨论了两者的等价性,证明了MBL对于上述两种语义的可靠性和完备性.其次,建立了一种多Agent概率信念逻辑MPBL(multi-agentprobabilisticbelieflogic),通过在广义Aumann语义基础上引入概率空间,给出了MPBL的概率Aumann语义,证明了它的可靠性,并给出MPBL的一些推论.     

Web服务的形式化验证

将Web服务组合建模为多智能体系统,采用时态知识逻辑模型检测工具MCTK刻画贷款协议Web服务实例,并验证相关的时态知识规范。在同一实验环境下,采用另一种时态知识逻辑模型检测工具MCMAS进行建模,并验证该实例。实验结果表明,基于MCTK的Web服务模型检测方法比基于MCMAS的方法更有效。     

多agent逻辑程序及其在协议验证中的应用

提出一种多agent逻辑程序,每个agent具有一个相信算子,讨论了其不动点语义和操作语义,证明了两种语义之间的等价性.提出了一种基于多agent逻辑程序的协议验证方法,以一种多方非否认安全协议为例,对该协议进行了形式化描述,验证了其具有不可否认性.     

Symbolic model checking for channel-based component connectors

This paper introduces a temporal logic framework to reason about the coordination mechanisms and data flow of exogenous coordination models. We take a CTL-like branching time logic, augmented with regular expressions that specify the observable I/O-operations, as a starting point. The paper provides the syntax and semantics of our logic and introduces the corresponding model checking algorithm. The second part of the paper reports an implementation that relies on a symbolic representation of the coordination network and the connected components by means of binary decision diagrams. A couple of examples are given to illustrate the efficiency of the model checking techniques and their implementation.     

On decidability and model checking for a first order modal logic for value-passing processes

A semantic interpretation of a first order extension of Hennessy-Milner logic for value-passing processes, named HML(FO), is presented. The semantics is based on symbolic transition graphs with assignment. It is shown that the satisfiability of the two-variable sub-logic HML(FO2) of HML(FO) is decidable, and the complexity discussed. Finally, a decision procedure for model checking the value-passing processes with respect to HML(FO2) is obtained.     

多智体系统中约简状态空间的限界模型检测算法

为了形式化描述多智体系统中与概率、实时、知识相关的性质,提出了一种概率实时认知逻辑PTCTLK.模型检测是验证多智体系统是否满足PTCTLK公式的主要技术,状态空间爆炸是该技术实用化的主要瓶颈,为此提出一种PTCTLK的限界模型检测算法.其基本思想是,在有限的局部可达空间中逐步搜索属性成立的证据,从而达到约简状态空间的目的.首先,将PTCTLK的模型检测问题转换为无实时算子的PBTLK的模型检测问题;其次,定义PBTLK的限界语义,并证明其正确性;然后,设计基于线性方程组求解的限界模型检测算法;最后,依据概率度量的演化规律,探索检测过程终止的判别准则.实例研究结果表明,与无界模型检测相比,在属性为真的证据较短的情况下,限界模型检测完成验证所需空间更小.     

模糊交互时态逻辑的模型检测

交互时态逻辑已被广泛应用于开放系统的规范描述,交互时态逻辑的模型检测技术是一个比较重要的验证方法。为了形式化描述和验证具有模糊不确定性信息的开放系统的性质,提出了一种模糊交互时态逻辑,并讨论了它的模型检测问题。首先,引入了模糊交互时态逻辑的基于路径和基于不动点的两种语义,证明了其等价性。然后,基于其等价性,给出了模糊交互时态逻辑的模型检测算法和复杂性分析。     

BDD Based Procedures for a Theory of Equality with Uninterpreted Functions

The logic of equality with uninterpreted functions has been proposed for verifying abstract hardware designs. The ability to perform fast satisfiability checking over this logic is imperative for such verification paradigms to be successful. We present symbolic methods for satisfiability checking for this logic. The first procedure is based on restricting analysis to finite instantiations of the variables. The second procedure directly reasons about equality by introducing Boolean-valued indicator variables for equality. Theoretical and experimental evidence shows the superiority of the second approach.