Decision Diagram Algorithms for Logic and Timed Verification

Symbolic verification has received much attention from both academia and industry in the past two decades. In particular, techniques based on decision diagrams have been successfully applied to various asynchronous and synchronous models.Decision diagrams can compactly encode sets and relations, or vectors and matrices. For canonicity, variables associated to the nodes must be found in a predefined order on any path from the root, and duplicate nodes cannot be present. In addition, a reduction rule is enforced, the simplest being the quasi-reduced rule, where no variable is ever skipped. However, more efficient rules exist, where edges skip redundant nodes. With the fully-reduced rule, a node is redundant if all its outgoing edges point to the same node. With the zero-suppressed rule, a node is redundant if only its 0-edge is not pointing to a pre-defined default terminal node. None of these rules, however, is particularly effective when encoding transition relations of asynchronous systems or rate matrices of Markov models. We then introduce an identity-reducedrule, which generalizes Kronecker encodings to take advantage of state variables that remain unchanged after an event occurrence, and a c-reducedrule, which generalizes the zero-suppressed rule, and propose a new generally-reduced form of decision diagrams where each variable uses a specific reduction rule. We then illustrate the effectiveness of this new canonical form of decision diagrams with a wide set of applications.State-space generation is usually the first and fundamental step for symbolic verification. Generally-reduced decision diagrams allow a more efficient symbolic state-space generation for general asynchronous systems by allowing on-the-fly extension of the state variable domains. After implementing both breadth-first and saturation-based state-space generation with this new data structure, we are able to exhibit substantial efficiency improvements with respect to traditional decision diagrams. Since previous works demonstrated that saturation outperforms breadth-first approaches, saturation with this new structure is now arguably thestate-of-the-art algorithm for symbolic state-space generation of asynchronous systems. When state-space generation completes, we also obtain the complete transition relation which can be used forfurther analysis.For synchronous systems, we study a type of timed Petri nets, which extends the traditional Petri nets to explicitly include real time in the model. We consider two fundamental reachability problems for timed Petri nets with positive integer firing times: timed reachability (find all markings where the model can be at a given finite time) and earliest reachability (find the minimum time when each reachable marking is entered). For these two problems, we define efficient symbolic algorithms that make use of bothgenerally-reduced decision diagrams without edge value and edge-valued decision diagrams, which associate integer value to the edges of decision diagrams. Runtime results on an extensive suite of models are provided to show the effectiveness and capability of our algorithm to cope with large state spaces.Then, we study the use of decision diagrams in stochastic models. We present a new type of edge-valued decision diagrams which can be used to encode non-negative real-valued functions. We then utilize it in a new approximate numerical solution algorithm for general structured ergodic models. The approximation uses a state-space encoding provided by decision diagrams and a transition rate matrix encoding provided by these new edge-valued decision diagrams. The new method retains the favorable properties of a previously proposed Kronecker-based approximation, while eliminating the need for a Kronecker-consistent model decomposition. Removing this restriction allows for a greater utilization of event locality, which facilitates both state-space generation and transition rate matrix generation, thus extends the applicability of this algorithm to larger and more complex models.All these algorithms are implemented based on our newly-designed Decision Diagram Library (DDL), which provides a user-friendly interface to create and manipulate generally-reduced decision diagrams with or without edge value It is the first library written for this purpose. This library is written in C++ and we adopt smart pointers for decision diagram node interface, similar to those in the Boost libraries, which automatically handle reference counts and garbage collection; this technique prevents memory leak and simplifies the interface, which greatly facilitate library users.All above algorithms are integrated into our verification tool Smart version 2