1. A computerized method comprising: receiving a state space and plural state groupings; and selecting states from a frontier set and performing the following until the frontier set is empty, when a state selected from the frontier set provides a transition to a next state, and the next state provides a variable-value assignment corresponding to at least one of the plural state groupings that is not yet in set V, then the next state is added to the frontier set and to set V, and the transition is added to set T, and when a state selected from the frontier set fails to provided an unexplored transition, removing the state from the frontier set.