Using edge-valued decision diagrams for symbolic generation of shortest paths

Abstract

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 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.