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).

• Type: Conference
• Year: 2010
• Where: HYBRID
• Authors: Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey
• Keywords: HYBRID 2010, Hybrid Systems, Non-negative Observer Value, Observer Value, final Observer Value