基于不完全Kripke结构三值逻辑的模型检验

模型检验技术是形式化验证中比较成熟的技术,但随着设计系统规模的增加,状态爆炸已成为其发展的一个主要问题.为解决此问题,本文提出对系统进行抽象,建立不完全的状态模型,在此状态模型上来验证表示其属性的逻辑公式.这样一个逻辑公式的真值除了真、假外,还出现了第三种情况：未知,即在这个状态模型下无法确定其真值,需要更多的状态信息才能确定.本文还讨论了二值逻辑的模型检验技术,在此基础上给出了基于不完全状态空间的三值逻辑的模型检验算法,此算法与二值逻辑模型检验算法相比,没有带来时间复杂度的增加,最后给出了三值逻辑模型检验算法的应用.     

模态转移系统的三值逻辑模型检验

分析了现有的模型检验技术应用于模态转移系统的三值逻辑公式的模型检验中存在的问题.提出了把模态转移系统转换成Kripke结构的算法以及三值逻辑公式转换成2个二值逻辑的算法,经过转换后可用现有的模型检验技术进行模型检验.用该算法转换后,状态数、转移数和原子命题数目与原模型呈线性关系,没有增加模型检验的复杂度.     

一种三值逻辑的NP完全问题与判定问题

本文建立了一种三值逻辑——中介逻辑的三值语义,证明了其命题演算MP与MP的可满足问题是NP完全的且其谓词演算(带或不带等词)MF,MF与ME的判定问题是算法不可解的。     

基于动态Kripke语义直接模型检测及其应用分析

在过去的20年里,基于Kdpkc语义结构的模型检测技术在集成电路设计,网络协议分析,程序正确性验证及程序错误发现等方面证明了其有效性和能力．最近,在诸如使用SAT分析工具、有界模型检测等避免OBDDs的模型检测研究方面取得了相当大的进展提出的动态Knpke 语义结构是让原子命题集合AP可以改变．基于这个方法,提出了一个直接模型检测算法．     

三值逻辑证明系统及正例与反例的提取

三值逻辑模型检验是对更高层的模型抽象验证的一种方法,对其验证中常常需要给出正例和反例.为此,讨论了三值逻辑模型检验以及正例和反例的提取,并在给出一套三值逻辑证明规则的基础上形成一个证明系统;运用该系统可以证明模型是否满足某个性质;在证明过程中为存在路径量词提取正例,为全称路径量词提取反例.正例和反例的提取可给模型的细化指明方向.最后通过实例给出了该证明系统在数字逻辑电路验证中的应用.     

一种三值逻辑电路的模拟方法

本文介绍一种三值逻辑电路的模拟方法，它是通过构造模拟三值逻辑电路的基本元件。这些元件以所构造模拟保持信号连接线作为计算对象，使模拟的各个功能由保持信号关系的过程来模拟。     

基于模糊逻辑的几类Kripke结构之间的关系

根据初始状态、状态之间的转换关系和命题赋值函数是否为分明的,模糊Kripke结构可分为8类。提出将模糊计算树逻辑作为判断模糊Kripke结构之间是否是等价的依据;详细讨论了8种模糊Kripke结构之间的关系。这些结论为设计应用中模型的合理选取提供了理论依据,也为解决模糊计算树逻辑的模型检测问题提供了一种新的方法。     

一种基于投影时序逻辑模型检测的入侵检测方法

基于时序逻辑模型检测的入侵检测技术降低了误用检测的漏报率,然而却几乎不能描述并发攻击和分段攻击,因而对这些复杂的攻击模式漏报率仍很高。本文针对该问题,提出了一种基于投影时序逻辑模型检测的入侵检测方法。对若干复杂攻击实例的检测表明,新方法可有效降低对并发攻击和分段攻击的漏报率。     

一种基于对称三值逻辑的多值学习网络

采用对称三值逻辑的数元｛１↑－，０，１｝作为信息存储的基本单位，本文提出一种用于逼近非线性函数的多值学习网络（ＫＬＮ）。该网络由多个既关联又独立的子网络构成，而每个子网络包含一个权值存储单元组和一个阈值存储单元组。所需的数学运算仅为整数的加法和逻辑判断，因而非常简单。在此基础上，研究了具有自学习功能的多值逻辑学习控制策略。仿真结果表明ＫＬＮ对非线性函数具有良好的学习和表达能力，并对复杂非线性系统具     

基于余归纳的最小Kripke结构的求解

状态空间爆炸问题是模型检测的最大障碍.从余归纳（特别是余代数）的角度研究了这个问题.用余归纳的方法证明：（1） 对于任意给定的一类Kripke结构（记为K）,在互模拟等价意义下K中最小Kripke结构（记为K₀）的存在唯一性.K₀描述了K中所有Kripke结构的行为而且没有冗余的状态;（2） 对于任意的M∈K（M可能包含无穷多个状态）,在互模拟等价意义下的相对于（M且基于K₀）的最小Kripke结构（记为K_M）的存在唯一性.由此提出一种求解K_M的算法,并用Ocaml予以简单实现.其应用之一在于可以用状态空间更小的K_M代替M进行模型检测.该方法可自然地推广到基于其他类型函子的余代数结构.     

Verification of heterogeneous multi-agent system using MCMAS

The focus of the paper is how to model autonomous behaviours of heterogeneous multi-agent systems such that it can be verified that they will always operate within predefined mission requirements and constraints. This is done by using formal methods with an abstraction of the behaviours modelling and model checking for their verification. Three case studies are presented to verify the decision-making behaviours of heterogeneous multi-agent system using a convoy mission scenario. The multi-agent system in a case study has been extended by increasing the number of agents and function complexity gradually. For automatic verification, model checker for multi-agent systems (MCMAS) is adopted due to its novel capability to accommodate the multi-agent system and successfully verifies the targeting behaviours of the team-level autonomous systems. The verification results help retrospectively the design of decision-making algorithms improved by considering additional agents and behaviours during three steps of scenario modification. Consequently, the last scenario deals with the system composed of a ground control system, two unmanned aerial vehicles, and four unmanned ground vehicles with fault-tolerant and communication relay capabilities.     

A Practical Approach to Partial Functions in CVC Lite

Most verification approaches assume a mathematical formalism in which functions are total, even though partial functions occur naturally in many applications. Furthermore, although there have been various proposals for logics of partial functions, there is no consensus on which is “the right” logic to use for verification applications. In this paper, we propose using a three-valued Kleene logic, where partial functions return the “undefined” value when applied outside of their domains. The particular semantics are chosen according to the principle of least surprise to the user; if there is disagreement among the various approaches on what the value of the formula should be, its evaluation is undefined. We show that the problem of checking validity in the three-valued logic can be reduced to checking validity in a standard two-valued logic, and describe how this approach has been successfully implemented in our tool, CVC Lite.     

基于抽象和组合方法的网络协议验证

由于模型检测存在状态爆炸问题,多主体的网络协议组合模型检测往往难以进行。为了缓解该问题,分析了通信主体数量增加对状态数量的影响,提出了组合式的抽象验证方法。首先根据所需验证的LTL性质,建立各个通信主体的Kripke结构,再对该Kripke结构进行抽象;然后组合抽象模型;最后运用Spin对组合抽象模型进行检验。为验证该方法的有效性,对NSPK协议进行了检测,结果表明,该方法所需的状态空间向量长度、搜索深度、存贮和遍历的状态数都有明显减少,有利于缓解状态爆炸问题。     

可能性测度下的LTL模型检测并行化研究

分布式模型检测是一种缓解状态空间爆炸的有效途径,已有文献提出了定性的分布式模型验证算法,然而定量LTL验证算法并行化问题还未得到有效解决。对此,展开两个方面的工作:提出一种新的动态系统状态空间划分方法;在定性LTL分布式验证算法的基础上给出了定量模型检测并行化验证算法。首先,将系统模型转化为可能的Kripke结构并选取一个并发分量,依据状态之间的关系完成系统状态的分割,使得关系紧密的状态尽可能分布在同一个计算节点上;其次,调整划分结果以使得计算负载平衡;然后,将划分结果与其他并发分量的状态进行叉乘,以完成系统状态空间的划分;最后,将待检测性质用自动机表示,在两者的乘积上,利用扩展的基于嵌套DFS的分布式验证算法完成系统的定量验证。     

循环对称化简及在三值模型上的扩展

为了将对称化简扩展到更多的非对称系统上,扩展了传统的基于自同构的对称性,提出了一种称为循环对称的新的对称性.证明了采用循环对称置换群或者由一组循环对称置换所生成的置换群仍可得到与原模型互模拟的对称商结构,从而达到化简系统规模的目的.进一步地,研究如何将对称化简应用于多值模型.多值模型可以有效地表示系统中的不确定信息,正越来越多地用于软件系统的建模与分析中.针对一种具体的多值模型——三值模型,定义传统的对称化简和循环对称化简在其上面的扩展.最后,分析三值模型的商结构与由约简得到的二值模型商结构之间的关系,证明了两种途径的等价性.     

人工智能中概率逻辑的研究

概率论是在不完备的、不确定的数据中进行推理的,它是度量不确定性的重要手段。在人工智能中,研究者结合概率和逻辑各自的优点,进行概率逻辑的研究。本文介绍了传统概率逻辑的三大派别,阐述了二值逻辑概率和三值逻辑概率的发展;最后介绍了泛逻辑,通过对概率逻辑和泛逻辑学的研究,将概率逻辑纳入泛逻辑学的框架内。