NIST

model checking

(algorithm)

Definition: Efficiently deciding whether a temporal logic formula is satisfied in a finite state machine model.

See also Kripke structure, BDD.

Note: Model checking is increasingly used in the formal verification of hardware and software. The decision process often uses some form of binary decision diagram (BDD).

Author: SKS

Implementation

Model checkers: Spin and SMV.
Go to the Dictionary of Algorithms and Data Structures home page.

If you have suggestions, corrections, or comments, please get in touch with Paul E. Black.

Entry modified 17 December 2004.
HTML page formatted Tue Dec 6 16:16:32 2011.

Cite this as:
Sandeep Kumar Shukla, "model checking", in Dictionary of Algorithms and Data Structures [online], Paul E. Black, ed., U.S. National Institute of Standards and Technology. 17 December 2004. (accessed TODAY) Available from: http://www.nist.gov/dads/HTML/modelcheckng.html

to NIST home page