Nicolas Markey

Résumé

Reachability checking is one of the most basic problems in verification. By solving this problem in a game, one can synthesize a strategy that dictates the actions to be performed for ensuring that the target location is reached. In this work, we are interested in synthesizing "robust" strategies for ensuring reachability of a location in timed automata. By robust, we mean that it must still ensure reachability even when the delays are perturbed by the environment. We model this perturbed semantics as a game between the controller and its environment, and solve the parameterized robust reachability problem: we show that the existence of an upper bound on the perturbations under which there is a strategy reaching a target location is EXPTIME-complete. We also extend our algorithm, with the same complexity, to turn-based timed games, where the successor state is entirely determined by the environment in some locations.

@article{tcs563()-BMS,
  author =              {Bouyer, Patricia and Markey, Nicolas and Sankur,
                         Ocan},
  title =               {Robust Reachability in Timed Automata and Games:
                         A~Game-based Approach},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {563},
  pages =               {43-74},
  year =                {2015},
  month =               jan,
  doi =                 {10.1016/j.tcs.2014.08.014},
  abstract =            {Reachability checking is one of the most basic
                         problems in verification. By solving this problem in
                         a game, one can synthesize a strategy that dictates
                         the actions to be performed for ensuring that the
                         target location is reached. In this work, we are
                         interested in synthesizing {"}robust{"} strategies
                         for ensuring reachability of a location in timed
                         automata. By robust, we mean that it must still
                         ensure reachability even when the delays are
                         perturbed by the environment. We model this
                         perturbed semantics as a game between the controller
                         and its environment, and solve the parameterized
                         robust reachability problem: we show that the
                         existence of an upper bound on the perturbations
                         under which there is a strategy reaching a target
                         location is EXPTIME-complete. We also extend our
                         algorithm, with the same complexity, to turn-based
                         timed games, where the successor state is entirely
                         determined by the environment in some locations.},
}