Paper: Symbolic model checking: 10 states and beyond (at LICS 1990)
Authors: Burch, J.R. Clarke, E.M. McMillan, K.L. Dill, D.L. Hwang, L.J.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 = {Burch, J.R. and Clarke, E.M. and McMillan, K.L. and Dill, D.L. and Hwang, L.J.}, title = {Symbolic model checking: 10 states and beyond}, booktitle = {Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1990}, year = 1990, editor = {John Mitchell}, month = {June}, pages = {428--439}, location = {Philadelphia, PA, USA}, publisher = {IEEE Computer Society Press} }