publication . Article . Conference object . Other literature type . 1992

Symbolic model checking: 10/sup 20/ states and beyond

Burch, J.R.; Clarke, E.M.; McMillan, K.L.; Dill, D.L.; Hwang, L.J.;
Restricted
  • Published: 01 Jun 1992 Journal: Information and Computation, volume 98, pages 142-170 (issn: 0890-5401, Copyright policy)
  • Publisher: Elsevier BV
Abstract
AbstractMany 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 Diagrans (Bryant, R. E., 1986, IEEE Trans. Com...
Subjects
free text keywords: Model checking, Discrete mathematics, Theoretical computer science, Finite-state machine, Abstraction model checking, Computation tree logic, Specification language, Computer science, Temporal logic, Binary decision diagram, Symbolic trajectory evaluation, Computational Theory and Mathematics, Information Systems, Computer Science Applications
Related Organizations
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue