In previous work, we proposed a “saturation” algorithm for symbolic state-space generation characterized by the use of multi-valued decision diagrams, boolean Kronecker operators, event locality, and a special iteration strategy. This approach outperforms traditional BDD-based techniques by several orders of magnitude in both space and time but, like them, assumes a priori knowledge of each submodel’s state space. We introduce a new algorithm that merges explicit local statespace discovery with symbolic global state-space generation. This relieves the modeler from worrying about the behavior of submodels in isolation.