Symbolic model checking: 10^20 states and beyond
The work
| Authors | Jerry R. Burch; E. M. Clarke; Kenneth L. McMillan; David L. Dill; L.J. Hwang |
|---|---|
| Editors | |
| Type | misc |
| Year | 1990 |
| Also known as | burch2002symbolic |
| Citekey | burch1990symbolic |
Where it appeared
| Published in | Proceedings - Symposium on Logic in Computer Science |
|---|---|
| Publisher | Institute of Electrical and Electronics Engineers |
| Pages | 428--439 |
Identifiers
| DOI | 10.1109/lics.1990.113767 |
|---|---|
| OpenAlex | W4253970047 |
Access
| Landing page | https://doi.org/10.1109/lics.1990.113767 |
|---|
Related
| Distinct from | burch1992symbolic |
|---|
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
A general method that represents the state space symbolically instead of explicitly is described. The generality of the method comes from using a dialect of the mu-calculus as the primary specification language. A model-checking algorithm for mu-calculus formulas which uses R.E. Bryant's (1986) binary decision diagrams to represent relations and formulas symbolically is described. It is then shown how the novel mu-calculus model checking algorithm can be used to derive efficient decision procedures for CTL model checking, satisfiability of linear-time temporal logic formulas, strong and weak observational equivalence of finite transition systems, and language containment of finite omega -automata. This eliminates the need to describe complicated graph-traversal or nested fixed-point computations for each decision procedure. The authors illustrate the practicality of their approach to symbolic model checking by discussing how it can be used to verify a simple synchronous pipeline.>
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-27 10:36 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@misc{burch1990symbolic,
title = {Symbolic model checking: 10^20 states and beyond},
author = {Jerry R. Burch and E. M. Clarke and Kenneth L. McMillan and David L. Dill and L.J. Hwang},
year = {1990},
journal = {Proceedings - Symposium on Logic in Computer Science},
publisher = {Institute of Electrical and Electronics Engineers},
pages = {428--439},
doi = {10.1109/lics.1990.113767},
}
This record lives at https://refs.drheap.org/burch1990symbolic/ and will keep
doing so. It used to be called burch2002symbolic, and those addresses still resolve to this one.