Nicolas Markey

Résumé

We study the problems of existence and construction of infinite schedules for finite weighted automata and one-clock weighted timed automata, subject to boundary constraints on the accumulated weight. More specifically, we consider automata equipped with positive and negative weights on transitions and locations, corresponding to the production and consumption of some resource (e.g. energy). We ask the question whether there exists an infinite path for which the accumulated weight for any finite prefix satisfies certain constraints (e.g. remains between 0 and some given upper-bound). We also consider a game version of the above, where certain transitions may be uncontrollable.

@inproceedings{formats2008-BFLMS,
  author =              {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim
                         Guldstrand and Markey, Nicolas and Srba, Ji{\v
                         r}{\'\i}},
  title =               {Infinite Runs in Weighted Timed Automata with Energy
                         Constraints},
  editor =              {Cassez, Franck and Jard, Claude},
  booktitle =           {{P}roceedings of the 6th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'08)},
  acronym =             {{FORMATS}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5215},
  pages =               {33-47},
  year =                {2008},
  month =               sep,
  doi =                 {10.1007/978-3-540-85778-5_4},
  abstract =            {We~study the problems of existence and construction
                         of infinite schedules for finite weighted automata
                         and one-clock weighted timed automata, subject to
                         boundary constraints on the accumulated weight. More
                         specifically, we~consider automata equipped with
                         positive and negative weights on transitions and
                         locations, corresponding to the production and
                         consumption of some resource (\emph{e.g.}~energy).
                         We~ask the question whether there exists an infinite
                         path for which the accumulated weight for any finite
                         prefix satisfies certain constraints
                         (\emph{e.g.}~remains between~\(0\) and some given
                         upper-bound). We~also consider a game version of the
                         above, where certain transitions may be
                         uncontrollable.},
}