Fifth Annual IEEE Symposium on

Logic in Computer Science (LICS 1990)

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.


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


    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}