As discrete–state systems are pervasive in our society, it is essential that we model and analyze them effectively, both prior to putting them in operation and during their useful life. The size of their state space, however, is a huge obstacle in practice. Often, the “easy” way to tackle this problem is to use some type of simulation, but this technique has obvious limitations. For performance analysis, simulation can at best offer only a statistical approximation, i.e., confidence intervals, while, for logic analysis, the situation is even worse, as it can only find errors, not prove correctness. Ultimately, these limitations stem from the same source: simulation only visits a fraction of the reachable states. Indeed, the fraction of the states that can actually be explored in a reasonable amount of time becomes exponentially smaller as the complexity of the system being modeled (measured in number of components, parts, etc.) increases.