What are the limitations of symbolic model checking?

Question

What are the limitations of the Symbolic Model Checking?

As far as I know, "state-space explosion" can still happen by this technique but it can explore much larger state space.

So, is the Symbolic Model Checking always better than the conventional model checking? If not, when to apply which one?

By the conventional model checking I mean: Clarke Jr, Edmund M., et al. Model checking. MIT press.

And by Symbolic model checking I mean: McMillan, Kenneth L. "Symbolic model checking." Symbolic Model Checking. Springer, Boston, MA, 1993. 25-60.

Answer 1

The primary limitation is that it can be more complicated to use.

Answer 2

• Limitation due to constraint solvers: The symbolic states are described by constraints. To validate a property on these states a constraint solver is used. Of course all limitations of these solvers apply. For example the non-linear arithmetic of the real numbers is undecidable in general. And the development of these solvers is extremely difficult and a lot is still left to be improved.

• Limitation due to the full directed graph: Symbolic model checking is still practically usable only on simpler programs. Even in the symbolic case a very large transition system is generated for a complexer program (e.g. a web browser) and there are too many symbolic states for the model checking algorithm to be computed. The algorithm demands to really check them all.

So for a concrete constraint solver like Z3 you can probably construct a pathologic case from these limitations which is solved slower or not at all symbolically, while the simple algorithm might succeed. But it is not possible to prove such a case in general.