Nicolas Markey

Résumé

We introduce a new formalism called automata over a timed domain which provides an adequate framework for the determinization of timed systems. In this formalism, determinization w.r.t. timed language is always possible at the cost of changing the timed domain. We give a condition for determinizability of automata over a timed domain without changing the timed domain, which allows us to recover several known determinizable classes of timed systems, such as strongly-non-zeno timed automata, integer-reset timed automata, perturbed timed automata, etc. Moreover in the case of timed automata this condition encompasses most determinizability conditions from the literature.

@inproceedings{formats2017-BJM,
  author =              {Bouyer, Patricia and Jaziri, Samy and Markey,
                         Nicolas},
  title =               {On the determinization of timed systems},
  editor =              {Abate, Alessandro and Geeraerts, Gilles},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'17)},
  acronym =             {{FORMATS}'17},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {10419},
  pages =               {25-41},
  year =                {2017},
  month =               sep,
  doi =                 {10.1007/978-3-319-65765-3_2},
  abstract =            {We introduce a new formalism called \emph{automata
                         over a timed domain} which provides an adequate
                         framework for the determinization of timed systems.
                         In~this formalism, determinization w.r.t. timed
                         language is always possible at the cost of changing
                         the timed domain. We~give a condition for
                         determinizability of automata over a timed domain
                         without changing the timed domain, which allows us
                         to recover several known determinizable classes of
                         timed systems, such as strongly-non-zeno timed
                         automata, integer-reset timed automata, perturbed
                         timed automata, etc. Moreover in the case of timed
                         automata this condition encompasses most
                         determinizability conditions from the literature.},
}