= Symbolic model checking
<Symbolic model checking> verifies a <Transition system> by representing sets of <state (computer science)>[states] and transitions as formulas or decision structures rather than enumerating each <state (computer science)>[state] separately. Encode a current <state (computer science)>[state] by bits $x$ and its successor by bits $x'$. A formula $T(x,x')$ describes the <transition relation>. If $R(x)$ denotes currently reachable <state (computer science)>[states], the next reachable set is
$$
R_{\mathrm{new}}(x')=I(x')\lor\exists x\,[R(x)\land T(x,x')].
$$
Iterating 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 variable>[Boolean] structure is favorable. A system with $n$ <Boolean variable>[Boolean] <state (computer science)>[state] components has up to $2^n$ <state (computer science)>[states], so sharing structure can be decisive. The representation can nevertheless become exponentially large, and variable ordering strongly affects a <binary decision diagram>[decision diagram]'s size. Symbolic representation mitigates <state-space explosion>; it does not abolish it.
Back to article page
