In this paper we present an algorithm for efficiently computing the
minimum cost of reaching a goal state in the model of Uniformly Priced
Timed Automata (UPTA). This model can be seen as a submodel of the
recently suggested model of linearly priced timed automata, which
extends timed automata with prices on both locations and transitions.
The presented algorithm is based on a symbolic semantics of UTPA,
and an efficient representation and operations based on difference
bound matrices. In analogy with Dijkstra's shortest path algorithm,
we show that the search order of the algorithm can be chosen such
that the number of symbolic states explored by the algorithm is
optimal, to be optimal, in the sense that the number of explored
states can not be reduced by any other search order. We also present
a number of techniques inspired by branch-and-bound algorithms which
can be used for limiting the search space and for quickly finding
near-optimal solutions.
The algorithm has been implemented in the verification tool
UPPAAL. When applied on a number of experiments the presented
techniques reduced the explored state-space with up to 90%.