Symbolic model checking: 10/sup 20/ states and beyond
Top Cited Papers
- 4 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 428-439
- https://doi.org/10.1109/lics.1990.113767
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 omega -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.<>Keywords
This publication has 8 references indexed in Scilit:
- Sequential circuit verification using symbolic model checkingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Local model checking in the modal mu-calculusLecture Notes in Computer Science, 1989
- Automatic Verification of Sequential Circuits Using Temporal LogicIEEE Transactions on Computers, 1986
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986
- Automatic verification of finite-state concurrent systems using temporal logic specificationsACM Transactions on Programming Languages and Systems, 1986
- Calculi for synchrony and asynchronyTheoretical Computer Science, 1983
- Results on the propositional μ-calculusTheoretical Computer Science, 1983
- A Calculus of Communicating SystemsLecture Notes in Computer Science, 1980