Nicolas Markey

Résumé

In this paper, we study one-clock priced timed automata in which prices can grow linearly (dp/dt=k) or exponentially (dp/dt=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).

@inproceedings{hscc2010-BFLM,
  author =              {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim
                         Guldstrand and Markey, Nicolas},
  title =               {Timed Automata with Observers under Energy
                         Constraints},
  editor =              {Johansson, Karl Henrik and Yi, Wang},
  booktitle =           {{P}roceedings of the 13th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'10)},
  acronym =             {{HSCC}'10},
  publisher =           {ACM Press},
  pages =               {61-70},
  year =                {2010},
  month =               apr,
  doi =                 {10.1145/1755952.1755963},
  abstract =            {In this paper, we study one-clock priced timed
                         automata in which prices can grow linearly
                         (\(\frac{dp}{dt}=k\)) or exponentially
                         (\(\frac{dp}{dt}=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).},
}