具有过去时态算予的计算树逻辑模型检测

在计算树逻辑（CTL）中引入过去时态算子，得到了表达力更强的属性规约语言CTLP，给出了CTLP的模型检测算法及其固定点刻画。该算法的复杂性和CTL一样。固定点刻画使得CTLP的符号模型检测过程能够实现，从而有效克服了模型检测中的状态爆炸问题。     

具有过去时态算子的计算树逻辑模型检测

在计算树逻辑(CTL)中引入过去时态算子,得到了表达力更强的属性规约语言CTLP,给出了CTLP 的模型检测算法及其固定点刻画.该算法的复杂性和CTL一样.固定点刻画使得CTLP的符号模型检测过程能够实现,从而有效克服了模型检测中的状态爆炸问题.     

基于模糊决策过程的模糊计算树逻辑模型检测

针对由数据表述产生的不确定性模糊系统的模型检测问题,给出模糊计算树逻辑模型检测算法。首先,引入模糊决策过程作为此类系统的模型,其最大特点是在迁移过程中对动作的不确定性选择和状态表述的模糊性。然后,在模糊决策过程基础上,给出模糊计算树逻辑的语法和语义。最后,给出模糊计算树逻辑模型检测算法,该算法是将模糊计算树逻辑模型检测问题转换为模糊矩阵的合成运算,其优势是时间复杂度低、计算过程较为简洁。     

直觉模糊测度的计算树逻辑

建立了直觉模糊Kripke结构(intuitionistic fuzzy Kripke structure,IFKS)模型,提出了基于直觉模糊Kripke结构的直觉模糊测度空间理论,阐述了IFKS的一系列性质。证明了任一路径转移的直觉模糊可达度(intuitionistic fuzzy probability,IFP)为初始状态的直觉模糊测度与各转移的IFP所取下确界,任一状态出发的所有路径上路径转移的IFP为所有路径可达度的上确界。给出了路径转移矩阵P及其传递闭包P~+的概念,给出了通过计算路径转移矩阵传递闭包,计算路径可达度的算法,并分析了算法的复杂度。提出了直觉模糊计算树逻辑(intuitionistic fuzzy computation tree logic,IFPCTL)理论,讨论了一组IFPCTL、可能测度计算树逻辑(possibilistic computation tree logic,PoCTL)和经典计算树逻辑(computation tree logic,CTL)公式的等价性。最后给出了一组等价的IFPCTL和PoCTL公式以及一组不等价的IFPCTL和CTL公式。     

概率计算树逻辑的限界模型检测

为了缓解概率计算树逻辑模型检测中的状态空间爆炸问题,提出了概率计算树逻辑的限界模型检测技术.该技术首先定义概率计算树逻辑的限界语义,并证明其正确性;之后,通过实例说明在传统限界模型检测中,以路径长度作为判断检测过程终止的标准已经失效,基于数值计算中牛顿迭代法的终止准则,设计了新的终止判断标准;然后提出基于线性方程组求解的限界模型检测算法;最后,通过3个测试用例说明,概率计算树逻辑限界模型检测方法在反例较短的情况下能够快速完成检测过程,而且比概率计算树逻辑的无界模型检测算法所需求得的状态空间要少.     

具有多值决策过程的广义可能性计算树逻辑模型检测

模型检测是一种自动验证软硬件系统行为的有效技术。为了对包含非确定性信息、不一致信息的并发系统进行形式化验证,在可能性理论、多值逻辑的基础上,研究了具有多值决策过程的广义可能性多值计算树逻辑模型检测算法,及其在检验非确定性系统中的具体应用。首先构造了多值决策过程作为系统模型,用多值计算树逻辑描述系统属性。然后给出具有多值决策过程的广义可能性多值计算树逻辑的模型检测算法,该算法将模型检测的具体问题转换为多项式时间内的模糊矩阵运算。最后就包含非确定性选择的多值系统的模型检测问题,给出一个具体的应用实例。     

广义可能性决策过程的计算树逻辑模型检测

模型检测作为一种形式化验证技术,已被广泛应用于各种并发系统的正确性验证。针对具有非确定性选择和广义可能性分布的并发系统,引入广义可能性决策过程作为此类系统的模型;给出描述其性质的规范语言广义可能性计算树逻辑的概念;研究此类系统的广义可能性计算树逻辑模型检测问题。结论表明,其模型检测算法的时间复杂度也为多项式时间。所获得的结果扩大了广义可能性测度在模型检测中的应用范围。     

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

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

基于模糊测度的模糊分支时态逻辑模型检测

针对具有模糊性和不确定性的复杂系统的验证问题,提出一种基于模糊测度的模糊分支时态逻辑模型检测算法。首先,在模糊决策过程模型的基础上引入模糊分支时态逻辑的语法和语义。然后,给出模糊分支时态逻辑模型检测算法,该算法将模型检测问题转化为矩阵运算,具有计算方式简洁、复杂度较低的优点。最后,通过医疗专家系统的实例说明了该模型检测算法的有效性。     

Another Look at LTL Model Checking

We show how LTL model checking can be reduced to CTL model checking with fairness constraints. Using this reduction, we also describe how to construct a symbolic LTL model checker that appears to be quite efficient in practice. In particular, we show how the SMV model checking system developed by McMillan [16] can be extended to permit LTL specifications. The results that we have obtained are quite surprising. For the specifications which can be expressed in both CTL and LTL, the LTL model checker required at most twice as much time and space as the CTL model checker. We also succeeded in verifying non-trivial LTL specifications. The amount of time and space that is required is quite reasonable. Based on the examples that we considered, it appears that efficient LTL model checking is possible when the specifications are not excessively complicated.     

Symbolic Verification and Analysis of Discrete Timed Systems

This paper presents a novel approach for real-time model checking. It combines the efficiency of traditional symbolic model checking with possibilities to describe and specify real-time systems. Using multi-terminal binary decision diagrams to represent time and time intervals, it becomes possible to transfer efficient algorithms and optimization heuristics known from standard CTL model checking to real-time applications. By introducing a new variant of models called I/O-interval structures we can describe systems in a modular way. Interval structures allow model composition of real-time structures such that state explosion effects are greatly reduced. Besides model checking we also present analysis algorithms which allow to compute key properties like system latencies and minimal response times from the structures describing the system. The practical applicability is proven by experimental results, computed by the verification system RAVEN, which implements all described algorithms, including counterexample generation and waveform visualization.     

Partial-Order Reduction in Symbolic State-Space Exploration

State-space explosion is a fundamental obstacle in the formal verification of designs and protocols. Several techniques for combating this problem have emerged in the past few years, among which two are significant: partial-order reduction and symbolic state-space search. In asynchronous systems, interleavings of independent concurrent events are equivalent, and only a representative interleaving needs to be explored to verify local properties. Partial-order methods exploit this redundancy and visit only a subset of the reachable states. Symbolic techniques, on the other hand, capture the transition relation of a system and the set of reachable states as boolean functions. In many cases, these functions can be represented compactly using binary decision diagrams (BDDs). Traditionally, the two techniques have been practiced by two different schools—partial-order methods with enumerative depth-first search for the analysis of asynchronous network protocols, and symbolic breadth-first search for the analysis of synchronous hardware designs. We combine both approaches and develop a method for using partial-order reduction techniques in symbolic BDD-based invariant checking. We present theoretical results to prove the correctness of the method, and experimental results to demonstrate its efficacy.     

Symbolic Model Checking for Channel-based Component Connectors

The paper reports on the foundations and experimental results with a model checker for component connectors modelled by networks of channels in the calculus Reo. The specification formalisms is a branching time logic that allows to reason about the coordination principles of and the data flow in the network. The underlying model checking algorithm relies on variants of standard automata-based approaches and model checking for CTL-like logics. The implementation uses a symbolic representation of the network and the enabled I/O-operations by means of binary decision diagrams. It has been applied to a couple examples that illustrate the efficiency of our model checker.     

Distributed Symbolic Bounded Property Checking

In this paper we describe an algorithm for distributed, BDD-based bounded property checking and its implementation in the verification tool SymC. The distributed algorithm verifies larger models and returns results faster than the sequential version.The core algorithm distributes partitions of the state set to computation nodes after reaching a threshold size. The nodes proceed with image computation on the nodes asynchronously. The main scalability problem of this scheme is the overlap of state set partitions. We present static and dynamic overlap reduction techniques.