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.     

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.     

A new verification technique for large processes based on identification of relevant tasks

Verification recently has become a challenging topic for business process languages. Verification techniques like model checking allow to ensure that a process complies with domain-specific requirements, prior to the execution. To execute full-state verification techniques like model checking, the state space of the process needs to be constructed. This tends to increase exponentially with the size of the process schema, or it can even be infinite. We address this issue by means of requirements-specific reduction techniques, i.e., reducing the size of the state space without changing the result of the verification. We present an approach that, for a given requirement the system must fulfill, identifies the tasks relevant for the verification. Our approach then uses these relevant tasks for a reduction that confines the process to regions of interest for the verification. To evaluate our new technique, we use real-world industrial processes and requirements. Mainly because these processes make heavy use of parallelization, full-state-search verification algorithms are not able to verify them. With our reduction in turn, even complex processes with many parallel branches can be verified in less than 10 s.     

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.     

Probabilistic symbolic model checking with PRISM: a hybrid approach

In this paper we present efficient symbolic techniques for probabilistic model checking. These have been implemented in PRISM, a tool for the analysis of probabilistic models such as discrete-time Markov chains, continuous-time Markov chains and Markov decision processes using specifications in the probabilistic temporal logics PCTL and CSL. Motivated by the success of model checkers such as SMV which use BDDs (binary decision diagrams), we have developed an implementation of PCTL and CSL model checking based on MTBDDs (multi-terminal BDDs) and BDDs. Existing work in this direction has been hindered by the generally poor performance of MTBDD-based numerical computation, which is often substantially slower than explicit methods using sparse matrices. The focus of this paper is a novel hybrid technique which combines aspects of symbolic and explicit approaches to overcome these performance problems. For typical examples, we achieve a dramatic improvement over the purely symbolic approach. In addition, thanks to the compact model representation using MTBDDs, we can verify systems an order of magnitude larger than with sparse matrices, while almost matching or even beating them for speed.     

Symbolic Graphs: Linear Solutions to Connectivity Related Problems

The importance of symbolic data structures such as Ordered Binary Decision Diagrams (OBDD) is rapidly growing in many areas of Computer Science where the large dimensions of the input models is a challenging feature: OBDD based graph representations allowed to define truly new standards in the achievable dimensions for the Model Checking verification technique. However, OBDD representations pose strict constraints in the algorithm design issue. For example, Depth-First Search (DFS) is not feasible in a symbolic framework and, consequently, many state-of-the-art DFS based algorithms (e.g., connectivity procedures) cannot be easily rearranged to work on symbolically represented graphs. We devise here a symbolic algorithmic strategy, based on the new notion of spine-set, that is general enough to be the engine of linear symbolic step algorithms for both strongly connected components and biconnected components. Our procedures improve on previously designed connectivity symbolic algorithms. Moreover, by an application to the so-called “bad cycle detection problem”, our technique can be used to efficiently solve the emptiness problem for various kinds of ω-automata. This work is a revised and extended version of [22,23]. It is partially supported by the projects PRIN 2005015491 and BIOCHECK.     

Test sequence generation and model checking using dynamic transition relations

The task of finding a set of test sequences that provides good coverage of industrial circuits is infeasible because of the size of the circuits. For small critical subcircuits of the design, however, designers can create a set of test sequences that achieve good coverage. These sequences cannot be used on the full design because the inputs to the subcircuit may not be accessible. In this work we present an efficient test generation algorithm that receives a test sequence created for the subcircuit and finds a test sequence for the full design that reproduces the given sequence on the subcircuit. The algorithm uses a new technique called dynamic transition relations to increase its efficiency .The most common and most expensive step in our algorithm is the computation of the set of predecessors of a set of states. To make this computation more efficient we exploit a partitioning of the transition relation into a set of simpler relations. At every step we use only those that are necessary, resulting in a smaller relation than the original one. A different relation is used for each step, hence the name dynamic transition relations. The same idea can be used to improve symbolic model checking for the temporal logic CTL.We have implemented the new method in SMV and run it on several large circuits. Our experiments indicate that the new method can provide gains of up to two orders of magnitude in time and space during verification. These results show that dynamic transition relations can make it possible to verify circuits that were previously unmanageable due to their size and complexity .     

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.     

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.     

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.     

A BMC-based formulation for the scheduling problem of hardware systems

Hardware scheduling is a well-known and well-studied problem. This paper defines a new SAT-based formulation of automata-based scheduling and proposes for the first time a completely new resolution algorithm based on SAT solvers and bounded model checking (BMC).The new formulation is specifically suited to control-dominated applications. Alternative executions are modeled as concurrency, where alternative behaviors are followed in parallel. This approach produces single-path scheduling traces instead of standard treelike solutions, thus enabling the use of BMC. This choice, however, creates the problem that resource bounds are treated incorrectly, due to the artificial concurrency modeling alternative behaviors. We then discuss how to take this into account, either by modifying the SAT solver or by adding extra clauses. Thus we are able to exploit SAT-based BMC to find the desired minimum latency schedule.Our method shows significant improvements in terms of both computational efficiency and modeling power, when compared to the BDD-based approach, and in terms of the optimality of the results when compared to heuristic methods.     

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.     

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

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

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 .     

Simplifying process model abstraction: Techniques for generating model names

The increased adoption of business process management approaches, tools, and practices has led organizations to accumulate large collections of business process models. These collections can easily include from a hundred to a thousand models, especially in the context of multinational corporations or as a result of organizational mergers and acquisitions. A concrete problem is thus how to maintain these large repositories in such a way that their complexity does not hamper their practical usefulness as a means to describe and communicate business operations. This paper proposes a technique to automatically infer suitable names for business process models and fragments thereof. This technique is useful for model abstraction scenarios, as for instance when user-specific views of a repository are required, or as part of a refactoring initiative aimed to simplify the repository's complexity. The technique is grounded in an adaptation of the theory of meaning to the realm of business process models. We implemented the technique in a prototype tool and conducted an extensive evaluation using three process model collections from practice and a case study involving process modelers with different experience.     

Analysis and verification of real-time systems using quantitative symbolic algorithms

The task of checking if a computer system satisfies its timing specifications is extremely important. These systems are often used in critical applications where failure to meet a deadline can have serious or even fatal consequences. This paper presents an efficient method for performing this verification task. In the proposed method a real-time system is modeled by a state-transition graph represented by binary decision diagrams. Efficient symbolic algorithms exhaustively explore the state space to determine whether the system satisfies a given specification. In addition, our approach computes quantitative timing information such as minimum and maximum time delays between given events. These results provide insight into the behavior of the system and assist in the determination of its temporal correctness. The technique evaluates how well the system works or how seriously it fails, as opposed to only whether it works or not. Based on these techniques a verification tool called Verus has been constructed. It has been used in the verification of several industrial real-time systems such as the robotics system described below. This demonstrates that the method proposed is efficient enough to be used in real-world designs. The examples verified show how the information produced can assist in designing more efficient and reliable real-time systems.     

Formal verification of collaboration patterns in healthcare

We propose a computer-based framework for the formal verification of collaboration patterns in healthcare teams. In this, the patterns are constructed diagrammatically as compositions of keystones that are viewed as abstract processes. The approach provides mechanisms for ensuring that safety properties are enforced and exceptional events are handled systematically. Additionally, a fully verified, executable model is obtained as an end product, enabling a simulation of its associated collaboration scenarios.     

时间自动机的LTL性质模型检测研究

为了增强模型检测工具的检测能力,拓宽模型检测技术的应用范围,对基于时间自动机的LTL性质模型检测进行了研究,对自动机的状态空间的存储方式和状态空间的展开过程进行了分析,讨论了LTL性质模型检测工具的检测流程和检测算法的实现策略对工具检测性能的影响,针对制约模型工具的检测能力和检测效率的因素,采取了一些相应的优化改进策略.采用了BDD(二叉决策图)共享存储技术和位编码压缩存储,较有效地减小了空间消耗,缓解了模型检测中状态爆炸引起的内存空间不足问题.与DTSpin等著名的模型检测工具进行了实验比较,取得了较好的实验结果.