Nicolas Markey

Abstract

Timed automata are a convenient mathematical model for modelling and reasoning about real-time systems. While they provide a powerful way of representing timing aspects of such systems, timed automata assume arbitrary precision and zero-delay actions; in particular, a state might be declared reachable in a timed automaton, but impossible to reach in the physical system it models.

In this paper, we consider permissive strategies as a way to overcome this problem: such strategies propose intervals of delays instead of single delays, and aim at reaching a target state whichever delay actually takes place. We develop an algorithm for computing the optimal permissiveness (and an associated maximally-permissive strategy) in acyclic timed automata and games.

@inproceedings{formats2020-CJMM,
  author =              {Clement, Emily and J{\'e}ron, Thierry and Markey,
                         Nicolas and Mentr{\'e}, David},
  title =               {Computing maximally-permissive strategies in acyclic
                         timed automata},
  editor =              {Bertrand, Nathalie and Jansen, Nils},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'20)},
  acronym =             {{FORMATS}'20},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {12288},
  pages =               {111-126},
  year =                {2020},
  month =               sep,
  doi =                 {10.1007/978-3-030-57628-8_7},
  abstract =            {Timed automata are a convenient mathematical model
                         for modelling and reasoning about real-time systems.
                         While they provide a powerful way of representing
                         timing aspects of such systems, timed automata
                         assume arbitrary precision and zero-delay actions;
                         in~particular, a~state might be declared reachable
                         in a timed automaton, but impossible to reach in the
                         physical system it models. \par In this paper, we
                         consider permissive strategies as a way to overcome
                         this problem: such strategies propose intervals of
                         delays instead of single delays, and aim at reaching
                         a target state whichever delay actually takes place.
                         We develop an algorithm for computing the optimal
                         permissiveness (and~an associated
                         maximally-permissive strategy) in acyclic timed
                         automata and games.},
}