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. The fixed point co...
%0 Generic
%1 Burch90symbolicmodel
%A Burch, J. R.
%A Clarke, E. M.
%A Mcmillan, K. L.
%A Dill, D. L.
%A Hwang, L. J.
%D 1990
%K bdd modelchecking spin symbolic
%T Symbolic Model Checking: 10 20 States and Beyond
%U http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.1489
%X 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. The fixed point co...
@misc{Burch90symbolicmodel,
abstract = {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. The fixed point co...},
added-at = {2009-12-08T23:26:14.000+0100},
author = {Burch, J. R. and Clarke, E. M. and Mcmillan, K. L. and Dill, D. L. and Hwang, L. J.},
biburl = {https://www.bibsonomy.org/bibtex/2244d456db3f5721934fd616e27ed2161/giuliano.losa},
description = {Symbolic Model Checking: 10 20 States and Beyond},
interhash = {1b3466d7869f713c03910da6e8357665},
intrahash = {244d456db3f5721934fd616e27ed2161},
keywords = {bdd modelchecking spin symbolic},
timestamp = {2009-12-08T23:26:14.000+0100},
title = {Symbolic Model Checking: 10 20 States and Beyond},
url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.1489},
year = 1990
}