State-space explosion

State-space explosion is the rapid growth of a model's possible global configurations as its components are combined. If $n$ independent components each have two local states, their Cartesian product has $2^n$ global states. Thirty such components already permit $1073741824$ combinations, before accounting for additional data values.

Model checking must establish a property over relevant reachable behavior, so checking one representative execution is insufficient. The reachable subset can be much smaller than the full product, and symbolic representations can compactly describe many configurations at once. However, compactness depends on structure; it is not a universal removal of exponential difficulty. The practical aim is to exploit shared structure without omitting behavior needed for the claimed formal verification.^[ref]