@article{AlurLaTorrePappas:TCS:2004,
    Abstract = {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 |wmax| 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.},
    Author = {Alur, Rajeev and {La Torre}, Salvatore and Pappas, George J.},
    File = {Optimal paths in weighted timed automata - 1-s2.0-S0304397503005838-main - e.pdf},
    ISSN = {0304-3975},
    Journal = {Theoretical Computer Science},
    Keywords = {Hybrid systems, Model checking, Optimal reachability, Timed automata},
    Number = {3},
    Pages = {297--322},
    Title = {Optimal paths in weighted timed automata},
    URL = {https://www.sciencedirect.com/science/article/pii/S0304397503005838},
    Volume = {318},
    Year = {2004},
    bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/S0304397503005838},
    bdsk-url-2 = {https://doi.org/10.1016/j.tcs.2003.10.038},
    date-added = {2021-04-29 10:47:30 +0200},
    date-modified = {2021-04-29 10:47:42 +0200},
    doi = {10.1016/j.tcs.2003.10.038}
}

@article{AlurLaTorrePappas:TCS:2004, Abstract = {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 |wmax| 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.}, Author = {Alur, Rajeev and {La Torre}, Salvatore and Pappas, George J.}, File = {Optimal paths in weighted timed automata - 1-s2.0-S0304397503005838-main - e.pdf}, ISSN = {0304-3975}, Journal = {Theoretical Computer Science}, Keywords = {Hybrid systems, Model checking, Optimal reachability, Timed automata}, Number = {3}, Pages = {297--322}, Title = {Optimal paths in weighted timed automata}, URL = {https://www.sciencedirect.com/science/article/pii/S0304397503005838}, Volume = {318}, Year = {2004}, bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/S0304397503005838}, bdsk-url-2 = {https://doi.org/10.1016/j.tcs.2003.10.038}, date-added = {2021-04-29 10:47:30 +0200}, date-modified = {2021-04-29 10:47:42 +0200}, doi = {10.1016/j.tcs.2003.10.038} }