Symbolic Model Checking: 10^20 States and Beyond

Symbolic Model Checking: 10^20 States and Beyond,10.1109/LICS.1990.113767,Jerry R. Burch,Edmund Melson Clarke,Kenneth L. McMillan,L. J. Hwang

Symbolic Model Checking: 10^20 States and Beyond   (Citations: 1532)
BibTex | RIS | RefWorks Download
Many different methods have been devised for automatically verifying finite state systems by examining state-graph models of system behavior. These methods all depend on decision procedures that explicitly represent the state space using a list or a table that grows in proportion to the number of states. We describe a general method that represents the state space symbolically instead of explicitly. The generality of our method comes from using a dialect of the Mu-Calculus as the primary specification language. We describe a model checking algorithm for Mu-Calculus formulas that uses Bryant's Binary Decision Diagrams (1986) to represent relations and formulas. We then show how our new 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 for finite !-automata.
Conference: Logic in Computer Science - LICS , pp. 428-439, 1990
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
Sort by: