We consider the optimal-reachability problem for a timed automaton with respect to a linear cost function which results in a weighted timed automaton. Our solution to this optimization problem consists of reducing it to computing (parametric) shortest paths in a finite weighted directed graph. We call this graph a parametric sub-region graph. It refines the region graph, a standard tool for the analysis of timed automata, by adding the information which is relevant to solving the optimal-reachability problem. We present an algorithm to solve the optimal-reachability problem for weighted timed automata that takes time exponential in O(n(|δ(A)|+|wmax|)), where n is the number of clocks, |δ(A)| is the size of the clock constraints and |w max| is the size of the largest weight. We show that this algorithm can be improved, if we restrict to weighted timed automata with a single clock. In case we consider a single starting state for the optimal-reachability problem, our approach yields an algorithm that takes exponential time only in the length of clock constraints. © 2003 Elsevier B.V. All rights reserved.
Alur, R., La Torre, S., & Pappas, G. J. (2004). Optimal paths in weighted timed automata. Theoretical Computer Science, 318(3), 297–322. https://doi.org/10.1016/j.tcs.2003.10.038