Nicolas Markey

Abstract

Weighted timed automata extend timed automata with cost variables that can be used to model the evolution of various quantities. Although cost-optimal reachability is decidable (in polynomial space) on this model, it becomes undecidable on weighted timed games. This paper studies cost-optimal reachability problems on weighted timed automata and games under robust semantics. More precisely, we consider two perturbation game semantics that introduce imprecisions in the standard semantics, and bring robustness properties w.r.t. timing imprecisions to controllers. We give a polynomial-space algorithm for weighted timed automata, and prove the undecidability of cost-optimal reachability on weighted timed games, showing that the problem is robustly undecidable.

@inproceedings{formats2013-BMS,
  author =              {Bouyer, Patricia and Markey, Nicolas and Sankur,
                         Ocan},
  title =               {Robust Weighted Timed Automata and Games},
  editor =              {Braberman, V{\'\i}ctor and Fribourg, Laurent},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'13)},
  acronym =             {{FORMATS}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8053},
  pages =               {31-46},
  year =                {2013},
  month =               aug,
  doi =                 {10.1007/978-3-642-40229-6_3},
  abstract =            {Weighted timed automata extend timed automata with
                         cost variables that can be used to model the
                         evolution of various quantities. Although
                         cost-optimal reachability is decidable (in
                         polynomial space) on this model, it becomes
                         undecidable on weighted timed games. This paper
                         studies cost-optimal reachability problems on
                         weighted timed automata and games under robust
                         semantics. More precisely, we consider two
                         perturbation game semantics that introduce
                         imprecisions in the standard semantics, and bring
                         robustness properties w.r.t. timing imprecisions to
                         controllers. We give a polynomial-space algorithm
                         for weighted timed automata, and prove the
                         undecidability of cost-optimal reachability on
                         weighted timed games, showing that the problem is
                         robustly undecidable.},
}