Binary Decision Diagrams

DOI10.1007/978-3-319-10575-8_7zbMath1392.68151OpenAlexW2804240010MaRDI QIDQ3176365

Randal E. Bryant

Publication date: 20 July 2018

Published in: Handbook of Model Checking (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-10575-8_7

Mathematics Subject Classification ID

Data structures (68P05)

Related Items (9)

Temporal Logic and Fair Discrete Systems ⋮ Combining Model Checking and Deduction ⋮ Generating Extended Resolution Proofs with a BDD-Based SAT Solver ⋮ Exploiting Asymmetry in Logic Puzzles: Using ZDDs for Symbolic Model Checking Dynamic Epistemic Logic ⋮ Unnamed Item ⋮ Approximate verification of strategic abilities under imperfect information ⋮ Generating extended resolution proofs with a BDD-based SAT solver ⋮ Dual proof generation for quantified Boolean formulas with a BDD-based solver ⋮ Application of dynamic evidential networks in reliability analysis of complex systems with epistemic uncertainty and multiple life distributions

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Symbolic model checking: \(10^{20}\) states and beyond
• Reduction of OBDDs in linear time
• A theory of timed automata
• Binary decision diagrams in theory and practice
• Efficient manipulation of decision diagrams
• BDD-Based Symbolic Model Checking
• Propositional SAT Solving
• Satisfiability Modulo Theories
• Model Checking Real-Time Systems
• On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
• A View from the Engine Room: Computational Support for Symbolic Model Checking
• Graph-Based Algorithms for Boolean Function Manipulation
• Binary Decision Diagrams
• Improving the variable ordering of OBDDs is NP-complete
• Minimization of free BDDs
• Finding the optimal variable ordering for binary decision diagrams
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Theory and Applications of Satisfiability Testing

This page was built for publication: Binary Decision Diagrams