Carnegie Mellon University
file.pdf (374.07 kB)
Download file

Symbolic Model Checking: 1020 States and Beyond

Download (374.07 kB)
journal contribution
posted on 1986-01-01, 00:00 authored by J R Burch, Edmund M Clarke, K L McMillan, D L Dill, L J Hwang
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


Publisher Statement

All Rights Reserved



Usage metrics