Binary Decision Diagrams: An Algorithmic Basis for Symbolic Model Checking
The work
| Authors | Randal E. Bryant |
|---|---|
| Editors | |
| Type | incollection |
| Year | 2018 |
| Also known as | anon2018binary |
| Citekey | bryant2018binary |
Where it appeared
| Published in | Handbook of Model Checking |
|---|---|
| Publisher | Springer International Publishing |
| Pages | 191--217 |
Identifiers
| DOI | 10.1007/978-3-319-10575-8_7 |
|---|
Related
| Distinct from | biere1999symbolic |
|---|---|
| Distinct from | bradley2011satbased |
| Distinct from | bryant1986graphbased |
| Distinct from | bryant1987boolean |
| Distinct from | bryant1987cosmos |
| Distinct from | bryant1991methodology |
| Distinct from | burch1992symbolic |
| Distinct from | manjrekar2025automating |
| Distinct from | plassanconclusive |
From unpaywall.
Abstract
Binary decision diagrams provide a data structure for representing and manipulating Boolean functions in symbolic form. They have been especially effective as the algorithmic basis for symbolic model checkers. A binary decision diagram represents a Boolean function as a directed acyclic graph, corresponding to a compressed form of decision tree. Most commonly, an ordering constraint is imposed among the occurrences of decision variables in the graph, yielding ordered binary decision diagrams (OBDD). Representing all functions as OBDDs with a common variable ordering has the advantages that (1) there is a unique, reduced representation of any function, (2) there is a simple algorithm to reduce any OBDD to the unique form for that function, and (3) there is an associated set of algorithms to implement a wide variety of operations on Boolean functions represented as OBDDs. Recent work in this area has focused on generalizations to represent larger classes of functions, as well on scaling implementations to handle larger and more complex problems.
A copy is held
pdf, 283.1 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via unpaywall |
|---|---|
| Added | 2026-09-16 06:34 UTC |
| Approved by | a person 2026-10-02 10:00 UTC |
Filed under
Cite it as
@incollection{bryant2018binary,
title = {Binary Decision Diagrams: An Algorithmic Basis for Symbolic Model Checking},
author = {Randal E. Bryant},
year = {2018},
booktitle = {Handbook of Model Checking},
publisher = {Springer International Publishing},
pages = {191--217},
doi = {10.1007/978-3-319-10575-8_7},
}
This record lives at https://refs.drheap.org/bryant2018binary/ and will keep
doing so. It used to be called anon2018binary, and those addresses still resolve to this one.