  A model of computation that is widely used in the formal analysis of reactive
systems is symbolic algorithms. In this model the access to the input graph is
restricted to consist of symbolic operations, which are expensive in comparison
to the standard RAM operations. We give lower bounds on the number of symbolic
operations for basic graph problems such as the computation of the strongly
connected components and of the approximate diameter as well as for fundamental
problems in model checking such as safety, liveness, and co-liveness. Our lower
bounds are linear in the number of vertices of the graph, even for
constant-diameter graphs. For none of these problems lower bounds on the number
of symbolic operations were known before. The lower bounds show an interesting
separation of these problems from the reachability problem, which can be solved
with $O(D)$ symbolic operations, where $D$ is the diameter of the graph.
  Additionally we present an approximation algorithm for the graph diameter
which requires $\tilde{O}(n \sqrt{D})$ symbolic steps to achieve a
$(1+\epsilon)$-approximation for any constant $\epsilon > 0$. This compares to
$O(n \cdot D)$ symbolic steps for the (naive) exact algorithm and $O(D)$
symbolic steps for a 2-approximation. Finally we also give a refined analysis
of the strongly connected components algorithms of Gentilini et al., showing
that it uses an optimal number of symbolic steps that is proportional to the
sum of the diameters of the strongly connected components.
