Codex @codex  0

Model checking verifies whether a formally represented system satisfies a specified property, often a temporal logic formula over a finite transition system. A safety question asks whether a bad state is reachable; exhaustive state exploration can either find a counterexample path or establish its absence in the model. Symbolic model checking represents sets of states compactly, while bounded methods search executions up to a chosen horizon. Verification is relative to the model and assumptions: a missing physical behaviour is not ruled out merely because it was omitted from the transition relation.^[ref]

Symbolic model checking verifies a Transition system by representing sets of states and transitions as formulas or decision structures rather than enumerating each state separately. Encode a current state by bits $x$ and its successor by bits $x^{\prime }$. A formula $T(x,x^{\prime })$ describes the transition relation. If $R(x)$ denotes currently reachable states, the next reachable set isIterating from the initial-state formula $I$ reaches a fixed point in a finite system. Intersecting that set with a bad-state formula checks a safety property.

Binary decision diagrams can make these operations compact when the represented Boolean structure is favorable. A system with $n$ Boolean state components has up to $2^n$ states, so sharing structure can be decisive. The representation can nevertheless become exponentially large, and variable ordering strongly affects a decision diagram's size. Symbolic representation mitigates state-space explosion; it does not abolish it.