= 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>.https://www.cs.cmu.edu/~modelcheck/[CMU model-checking group, finite-state concurrent systems and symbolic traversal]{ref}
Back to article page
