## Paper: Symbolic model checking: 10^20 states and beyond (at LICS 1990)

*Winner of the Test-of-Time Award in 2010***Jerry R. Burch Edmund M. Clarke Kenneth L. McMillan David L. Dill L. James Hwang**

### 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 ω-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

### BibTeX

@InProceedings{BurchClarkeMcMillan-Symbolicmodelchecki, author = {Jerry R. Burch and Edmund M. Clarke and Kenneth L. McMillan and David L. Dill and L. James Hwang}, title = {Symbolic model checking: 10^20 states and beyond}, booktitle = {Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990)}, year = {1990}, month = {June}, pages = {428--439}, location = {Philadelphia, PA, USA}, publisher = {IEEE Computer Society Press} }