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.     

A Comparison of Free BDDs and Transformed BDDs

Ordered binary decision diagrams (OBDDs) introduced by Bryant (IEEE Trans. on Computers, Vol. 35, pp. 677–691, 1986) have found a lot of applications in verification and CAD. Their use is limited if the OBDD size of the considered functions is too large. Therefore, a variety of generalized BDD models has been presented, among them FBDDs (free BDDs) and TBDDs (transformed BDDs). Here the quite tight relations between these models are revealed and their advantages and disadvantages are discussed.     

Multiway Decision Graphs for Automated Hardware Verification

Traditional ROBDD-based methods of automated verification suffer from the drawback that they require a binary representation of the circuit. To overcome this limitation we propose a broader class of decision graphs, called Multiway Decision Graphs (MDGs), of which ROBDDs are a special case. With MDGs, a data value is represented by a single variable of abstract type, rather than by 32 or 64 boolean variables, and a data operation is represented by an uninterpreted function symbol. MDGs are thus much more compact than ROBDDs, and this greatly increases the range of circuits that can be verified. We give algorithms for MDG manipulation, and for implicit state enumeration using MDGs. We have implemented an MDG package and provide experimental results.     

Polynomial-Size Binary Decision Diagrams for the Exactly Half-<Emphasis Type="Italic">d</Emphasis>-Hyperclique Problem Reading Each Input Bit Twice

A binary decision diagram (BDD) is a graph-based data structure representing Boolean functions; ℓ-BDDs are BDDs with an additional restriction that each input bit can be tested at most ℓ times. A d-uniform hypergraph H on N vertices is an exactly half-d-hyperclique if N/2 of its vertices form a hyperclique and the remaining vertices are isolated. Wegener [J. ACM 35(2), 461–471 (1988)] conjectured that there is no polynomial-size (d−1)-BDD for the Exactly half-d-hyperclique problem. We refute this conjecture by constructing polynomial-size (syntactic) 2-BDDs for the Exactly half-d-hyperclique problem for every d≥2. Institute for Theoretical Computer Science (ITI) is supported by Ministry of Education of Czech Republic as projects LN00A056 and 1M0545.     

Free binary decision diagrams for the computation of EAR n

Free binary decision diagrams (FBDDs) are graph-based data structures representing Boolean functions with the constraint (additional to binary decision diagram) that each variable is tested at most once during the computation. The function EAR_n is the following Boolean function defined for n × n Boolean matrices: EAR_n(M) = 1 iff the matrix M contains two equal adjacent rows. We prove that each FBDD computing EAR_n has size at least and we present a construction of such diagrams of size approximately .     

VLSI设计形式化验证方法的综述

在本文中，作者讨论了形式验证的理论，并综述了各种形式验证的方法、系统及一些重要的应用，对形式验证的发展趋势也做了论述。     

Extended BDDs: Trading of canonicity for structure in verification algorithms

We present an extension to binary decision diagrams (BDDs) that exploits the information contained in the structure of a given circuit to produce a compact,semicanonical, representation. The resulting XBDDs (extended BDDs) retain many of the advantages of BDDs, while at the same time allowing one to deal with larger circuits.We propose algorithms for verification of combinational circuits based on XBDDs that overcome the exponential growth in the number of nodes in the BDDs for some specific circuits such as the multipliers. While the approach remains cpu-time intensive, we believe it is the first to exactly verify the most difficult (median) output of a 16-bit multiplier. Experimental results are presented to support our claim that the XBDD approach is the best for multiplier verification.     

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.     

Verifying Temporal Properties of Reactive Systems: A STeP Tutorial

We review a number of formal verification techniques supported by STeP, the Stanford Temporal Prover, describing how the tool can be used to verify properties of several versions of the Bakery Mutual exclusion algorithm for mutual exclusion. We verify the classic two-process algorithm and simple variants, as well as an atomic parameterized version. The methods used include deductive verification rules, verification diagrams, automatic invariant generation, and finite-state model checking and abstraction.     

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

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

基于XYZ/E描述和验证容错系统

研究使用XYZ/E描述和验证容错系统.基于XYZ/E中可执行程序P对应的状态转换系统对其错误环境F建模,通过错误转换给出错误影响程序P_F;基于P,F和恢复算法R,通过容错转换给出容错程序P_F-R;定义了程序P,Q之间两种求精关系:容错求精和向后恢复求精,基于这两种求精关系可直接从程序P的规范推导出程序Q满足的一些性质.     

Symbolic Reasoning with Weighted and Normalized Decision Diagrams

Several variants of Bryant's ordered binary decision diagrams have been suggested in the literature to reason about discrete functions. In this paper, we introduce a generic notion of weighted decision diagrams that captures many of them and present criteria for canonicity. As a special instance of such weighted diagrams, we introduce a new BDD-variant for real-valued functions, called normalized algebraic decision diagrams. Regarding the number of nodes and arithmetic operations like addition and multiplication, these normalized diagrams are as efficient as factored edge-valued binary decision diagrams, while several other operators, like the calculation of extrema, minimum or maximum of two functions or the switch from real-valued functions to boolean functions through a given threshold, are more efficient for normalized diagrams than for their factored counterpart.     

On the use of MTBDDs for performability analysis and verification of stochastic systems

This paper describes how to employ multi-terminal binary decision diagrams (MTBDDs) for the construction and analysis of a general class of models that exhibit stochastic, probabilistic and non-deterministic behaviour. It is shown how the notorious problem of state space explosion can be circumvented by compositionally constructing symbolic (i.e. MTBDD-based) representations of complex systems from small-scale components. We emphasise, however, that compactness of the representation can only be achieved if heuristics are applied with insight into the structure of the system under investigation. We report on our experiences concerning compact representation, performance analysis and verification of performability properties.     

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

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

String-matching with OBDDs

Ordered binary decision diagrams (OBDDs) are a very popular graph representation for Boolean functions. They can be viewed as finite automata recognizing sets of strings of a fixed length, where the letters of the input strings are read at most once in a predefined ordering. The string matching problem with string w as pattern, consists of determining, given an input string, whether or not it contains w as substring. We show that for a fraction of orderings tending to 1 when n increases arbitrarily, the minimal size of an OBDD solving the string matching problem for strings of length n has a growth which is an exponential in n.     

针对递归函数的高级综合编译优化算法

为了消除高级综合中的递归函数调用,提出一种基于函数调用图(FCG)和分支决策的编译优化算法.首先在LLVM编译器架构下给出FCG的中间结构,将递归调用转换为非递归函数的嵌套调用,然后借助决策树的构造规则去除函数体中的分支判断及未调用的子支,最后采用子函数复用、资源预评估的方法控制实现电路的规模.实验结果表明,与内联展开算法RecursionHW相比,采用该算法综合后的逻辑单元数平均减少63％,时钟频率平均提高3.2倍,并且高级综合的总时长随递归深度的增大而呈指数级减少.     

Using XBDDs and ZBDDs in points‐to analysis

Binary decision diagrams (BDDs) have recently become widely accepted as a space‐efficient method of representing relations in points‐to or reference analyses. When BDDs are used to represent relations, each element of a domain is assigned a bit pattern to represent it, but not every bit pattern represents an element. The circuit design, model checking, and verification communities have achieved significant reductions in BDD sizes using several techniques to reduce the overhead of these don't‐care bit patterns. We adapt these techniques to BDD‐based program analysis, and we study their effect on the BDD size in this context. Specifically, we compare the effectiveness of Coudert and Madre's restrict operation and the use of zero‐suppressed BDDs (ZBDDs) to represent relations. Using don't‐care BDDs (XBDDs) and ZBDDs to reduce the size of the relations allows a compiler or other software analysis tools to analyze larger programs with greater precision. Our experimental evaluation considers both context‐insensitive and context‐sensitive program analyses. We also provide a metric that can be used to estimate whether ZBDDs will be more compact than BDDs for a given analysis. Copyright © 2008 John Wiley & Sons, Ltd.     

Introduction to the OBDD algorithm for the ATP community

We describe in terms familiar to the automated reasoning community the graph-based algorithm for deciding propositional equivalence published by R. E. Bryant in 1986. Such algorithms, based onordered binary decision diagrams orOBDDs, are among the fastest known ways to decide whether two propositional expressions are equivalent and are generally hundreds or thousands of times faster on such problems than most automatic theorem-proving systems. An OBDD is a normalized IF (if-then-else) expression in which the tests down any branch are ascending in some previously chosen fixed order. Such IF expressions represent a canonical form for propositional expressions. Three coding tricks make it extremely efficient to manipulate canonical IF expressions. The first is that two canonicalized expressions can be rapidly combined to form the canonicalized form of their disjunction (conjunction, exclusive-or, etc.) by exploiting the fact that the tests are ordered. The second is that every distinct canonical IF expression should be assigned a unique integer index to enable fast recognition of identical forms. The third trick is that the operation in which one combines canonicalized subterms term should be memo-ized or cached so that if the same operation is required in the future its result can be looked up rather than recomputed.This work was supported in part at Computational Logic, Inc., by the National Computer Security Center (Contract MDA904-92-C-5167). The views and conclusions contained in this document are those of the author and should not be interpreted as representing the official policies, either expressed or implied, of Computational Logic, Inc., the National Computer Security Center, or the U.S. Government.