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

Authors: 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}
  }