Optimal Infinite Runs in One-Clock Priced Timed Automata

We address the problem of finding an infinite run with theoptimal cost-time ratio in a one-clock priced timed automaton and pro-vide an algorithmic solution. Through refinements of the quotient graphobtained by strong time-abstracting bisimulation partitioning, we con-struct a graph with time and costs as weights and prove that the min-imum ratio properties remain unaltered, allowing algorithms for finiteweighted graphs to be applied. The resulting algorithm has an overalltime complexity of O((|Q| · (|T | + |Q|))6 ), |Q| being the number of lo-cations and |T | the number of transitions of the one-clock priced timedautomaton.