N.: Timed automata with observers under energy constraints

In this paper, we study one-clock priced timed automata in which prices can grow linearly (p ̇ = k) or exponentially (p ̇ = kp), with discontinuous updates on edges. We propose EXPTIME algorithms to decide the existence of controllers that ensure existence of infinite runs or reachability of some goal location with non-negative observer value all along the run. These algorithms consist in computing the optimal delays that should be elapsed in each location along a run, so that the final observer value is maximized (and never goes below zero). 1