Nicolas Markey

Abstract

We study the model-checking problem for WMTL, a cost-extension of the linear-time timed temporal logic MTL, that is interpreted over weighted timed automata. We draw a complete picture of the decidability for that problem: it is decidable only for the class of one-clock weighted timed automata with a restricted stopwatch cost, and any slight extension of this model leads to undecidability. We finally give some consequences on the undecidability of linear hybrid automata.

@inproceedings{formats2007-BM,
  author =              {Bouyer, Patricia and Markey, Nicolas},
  title =               {Costs are Expensive!},
  editor =              {Raskin, Jean-Fran{\c c}ois and Thiagarajan, P. S.},
  booktitle =           {{P}roceedings of the 5th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'07)},
  acronym =             {{FORMATS}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4763},
  pages =               {53-68},
  year =                {2007},
  month =               oct,
  doi =                 {10.1007/978-3-540-75454-1_6},
  abstract =            {We study the model-checking problem for WMTL,
                         a~cost-extension of the linear-time timed temporal
                         logic MTL, that is interpreted over weighted timed
                         automata. We~draw a complete picture of the
                         decidability for that problem: it~is decidable only
                         for the class of one-clock weighted timed automata
                         with a restricted stopwatch cost, and any slight
                         extension of this model leads to undecidability.
                         We~finally give some consequences on the
                         undecidability of linear hybrid automata.},
}