One clock priced timed automata: Model checking and optimal strategies

In this paper, we consider priced (or weighted) timed au-tomata, and prove various decidability results when the au-tomaton has only one clock: we prove that model check-ing of WCTL is decidable and that optimal costs in priced timed games are computable. In contrast, it has recently been proved that these problems are undecidable for this model as soon as the system has three clocks.