Binary decision diagram

Sinnamon, R., Andreas, J., January 1996. Fault tree analysis and binary decision diagrams. In Proceedings of the Reliability and Maintainability Symposium. 

Symbolic model checking makes excessive use of Boolean functions. ROBDDs (R.E. Bryant 1986) are a compact and efficient representation of these functions. In contrast to ROBDDs, multi terminal binary decision diagrams (MTBDD) (E. Clarice et al. 1993,R.I. Baharetal. 1993) representpseuribBoo/ean ncrions. These functions map bit vectors to a finite set of elements. 

Binary Decision Diagrams (BDDs) are a canonical representation of Boolean functions /(xi, 2j 2 3,..., Xn) in the form of directed acyclic graphs. The reader should refer to [4] and [5] for a tutorial introduction to BDDs. 

P. Arunachalam, C. Chase, and D. Moundanos. Distributred Binary Decision Diagrams for Verification of Large Circuits. In Proc, IEEE ICCD 96, pages 365-370, Austin, Texas, USA, October 1996. 

P. Ashar and M. Cheong. Efficient Breadth-First Manipulation of Binary Decision Diagrams. In Proc. lEEE/ACM ICCAD 94y pages 622-627, San Jose, CA, USA, November 1994. 

R. E. Bryant. Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Computing Surveys 24(3) 293-318, September 1992. 

S. Kimura and E. M. Clarke. A Parallel Algorithm for Constructing Binary Decision Diagrams. In Proc. IEEE ICCD 90, pages 220-223, November 1990. 

N. Ishiura, H. Sawada, and S. Yajima. Minimization of binary decision diagrams based on exchanges of variables. International Conference on Computer-Aided Design, pages 472-475,1991. 

Y.T. Lai and S. Sastry. Edge-valued binary decision diagrams for multi-level hierarchical verification. ACM/IEEE Design Automation Conference, pages 608-613, June 1992. 

A big step forward was made when McMillan (1993) proposed a new model checking algorithm for CTL, based on fixpoint computations of sets of states. In this algorithm, called symbolic model checking, binary decision diagrams (Bryant 1986) are used to represent both the transitions and the states of the model. Since sets of states are represented in intention by their characteristic functions, the size of the verified model is not bound by the memory of the computer carrying the verification and it is possible to verify systems that have several orders of magnitude more states. 

Outline In Sections 2 to 5, we overview the foundations of symbolic model checking Kripke structures, the class of models considered binary decision diagrams, an efficient data structure to represent such structures elements of fixpoint theory in lattices syntax and semantics of computation tree logic. In Section 6, we present the main result of the paper a sufficient condition for a given property to be an invariant of a given model. We also show how to incorporate the computation of this sufficient condition in CTL model checking. 

Binary Decision Diagrams (BDDs for short) form a heuristically efficient data structure to represent formulas of the propositional logic. Let P be a totally ordered finite set of boolean propositions. Let / be a boolean formula over P, bdd f) is the BDD representing /, and bdd f) is the size if this BDD. Bryant (1986) showed that BDDs axe a canonical representation two equivalent formulas are represented with the same BDD ... 

CheckOff-M represents designs internally using efficient implementations of Ordered Binary Decision Diagrams (OBDDs). 

Xing, L. (2008). An efficient binary-decision-diagram-based approach for network reliability and sensitivity analysis. IEEE Trans, on Systems, Man, and Cybernetics—part A Systems and Humans 38(1), 105-115. 

The network reliabUity is represented as a logical OR of all the paths acting in an active redundancy. A passive redundancy with imperfect switching would have been more realistic but more complicated to evaluate. There exist different techniques for computing Ax y(t) such as the inclusion-exclusion principle (Ru-bino, 1998) or the binary decision diagram (Rauzy, 1993) (Liudong, 2008). Here, the present paper takes into account the behavior of each sensor of WSN. For this reason, each boolean function of each monitored point... 

Liudong Xing (2008). An efficient binary-decision-diagram-based approach for network reliability and sensitivity analysis. 

A somewhat related approach that has been applied successfully is the so-called implicit enumeration technique [10] based on exploring the state space in a breadth-first manner and thereby treating sets of states collectively. In such a tool, sets of states are conveniently represented by a binary decision diagram (BDD) data structure. However, it has been shown [8] that a proof checker for PTL can be implemented using basically the same techniques, and... 

ETA is a very valuable system to analyze consequences as an outcome of a failure, undesired event, or an accidental event outlined in Chapter 11. This is a binary-based, logical system. The binary decision diagram (BDD), discussed in Clause 5 of Chapter 1, can be used to obtain outcome details. To get a general idea about ETA, refer to Fig. V/2.1-1. 

J. D. Andrews, S.J. Dunnett, Event Tree Analysis Using Binary Decision Diagrams, Lough-... 

Y. Matsunaga and M. Fujita, Multi-Level Logic Optimization Using Binary Decision Diagrams, ICCAD-89, pp. 556-559, Nov. 1989. 

Andrews, J.D. Dunnett, S.J. 2000. Event-tree analysis using binary decision diagrams. IEEE Transactions on Reliability 49(2) 230-238. 

A SLIM model can be evaluated using model checking techniques, in order to guarantee that it satisfies the required functional properties. To this aim, the model can be translated into a Labeled Transition System (LTS) and exhaustively analyzed by the model checker to check whether the properties hold. If a property does not hold, a counterexample trace can be generated to show an execution trace of the model that violates the property. To cope with the state explosion problem, advanced techniques can be applied, in particular sjun-bolic techniques based on Binary Decision Diagrams (BDD) [9] and SAT-based Bounded Model Checking [4,5,22,18] (BMC). Verification can also benefit from advanced techniques for compihng temporal properties into a symbolic LTS [12]. 

Independent of how the internal failure modes are merged and what other abstraction algorithms are applied, the mapping between the realization and the specification must be specified as part of the realization. Additionally, the kind of relation must be specified as part of the specification. Only in this way is it possible to guarantee traceability and to check if the assumed relation between failure realization and specification is true. For example, if modularization is used, the internal modules of the failure realization and the corresponding internal failure modes of the specification must be known in order to check equivalence. This is also true if the internal failure modes are only renamed from the realization to the specification. To efficiently check the equivalence or other qualitative relations between failure specification and realization. Binary Decision Diagrams (BDDs) are used. 

Remenyte-Prescott, R., Andrews, J. Prime Implicants for modularized non-coheient fault tress using binary decision diagrams. Int. J. Reliability and Safety 1(4), 446-464 (2007)... 

---