We present a new method for the symbolic construction of shortest paths in reachability graphs. Our algorithm relies on a
variant of edge-valued decision diagrams that supports efficient fixed-point iterations for the joint computation of both
the reachable states and their distance from the initial states. Once the distance function is it known, a shortest path from
an initial state to a state satisfying a given condition can be easily obtained. Using a few representative examples, we show
how our algorithm is vastly superior, in terms of both memory and space, to alternative approaches that compute the same information,
such as ordinary or algebraic decision diagrams.
Work supported in part by the National Aeronautics and Space Administration under NASA Grants NAG-1-2168 and NAG-1-02095.