Symbolic model checking

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.