Nicolas Markey

Résumé

Reachability checking is one of the most basic problems in verification. By solving this problem, one synthesizes 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 a timed automaton; with "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.

@inproceedings{icalp2012-BMS,
  author =              {Bouyer, Patricia and Markey, Nicolas and Sankur,
                         Ocan},
  title =               {Robust reachability in timed automata: a~game-based
                         approach},
  editor =              {Czumaj, Artur and Mehlhorn, Kurt and Pitts, Andrew
                         and Wattenhofer, Roger},
  booktitle =           {{P}roceedings of the 39th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'12)~-- Part~{II}},
  acronym =             {{ICALP}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7392},
  pages =               {128-140},
  year =                {2012},
  month =               jul,
  doi =                 {10.1007/978-3-642-31585-5_15},
  abstract =            {Reachability checking is one of the most basic
                         problems in verification. By solving this problem,
                         one synthesizes 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 a timed automaton;
                         with {"}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.},
}