Model checking

Summary

Model checking is the problem of deciding whether a finite model of a system satisfies a specification written in a temporal logic. The model is usually a finite Kripke structure, and the specification a formula of linear temporal logic, computation tree logic or the modal mu-calculus. It is a fully automatic method of verification: when the property fails, the algorithm can return a counterexample run.