ModelChecking

Model checking is an automated formal verification technique used to determine whether a finite-state model of a system satisfies a given specification, typically expressed in temporal logic. A model checker exhaustively explores the state space of the model to verify properties such as safety and liveness, and, if a property is violated, it provides a counterexample execution trace.

Originating in the early 1980s with work by Clarke and Emerson, model checking has become a central method in formal verification. The approach treats a system as a labeled transition system or finite-state machine and evaluates whether temporal properties, often formulated in logics such as LTL (linear temporal logic) or CTL (computation tree logic), hold. Probabilistic and real-time extensions address stochastic and timing aspects of systems.

Methods used in model checking include explicit-state techniques that enumerate reachable states, and symbolic techniques that manipulate large sets of states compactly via data structures like binary decision diagrams. SAT/SMT-based model checking, abstraction and refinement (including counterexample-guided abstraction refinement), and reductions such as partial order and symmetry reductions are employed to mitigate state explosion. Extensions cover timed model checking for real-time systems and probabilistic model checking for systems with randomness, using logics such as PCTL and CSL.

Applications span hardware design and verification, communication protocols, software verification, and safety-critical embedded systems. Prominent tools include Spin, NuSMV/SMV, UPPAAL, and PRISM, each supporting different logics and modeling styles.

Limitations include the state explosion problem, significant modeling effort, and the gap between realistic systems and tractable models. Ongoing research seeks to improve scalability through compositional and parameterized verification, abstraction techniques, and integration with learning-based methods.