Nicolas Markey

Abstract

Active learning of timed languages is concerned with the inference of timed automata by observing some of the timed words in their languages. The learner can query for the membership of words in the language, or propose a candidate model and ask if it is equivalent to the target. The major difficulty of this framework is the inference of clock resets, which are central to the dynamics of timed automata but not directly observable.

Interesting first steps have already been made by restricting to the subclass of event-recording automata, where clock resets are tied to observations. In order to advance towards learning of general timed automata, we generalize this method to a new class, called reset-free event-recording automata, where some transitions may reset no clocks.

Central to our contribution is the notion of invalidity, and the algorithm and data structures to deal with it, allowing on-the-fly detection and pruning of reset hypotheses that contradict observations. This notion is a key to any efficient active-learning procedure for generic timed automata.

@inproceedings{formats2020-HJM,
  author =              {Henry, L{\'e}o and J{\'e}ron, Thierry and Markey,
                         Nicolas},
  title =               {Active learning of timed automata with unobservable
                         resets},
  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 =               {144-160},
  year =                {2020},
  month =               sep,
  doi =                 {10.1007/978-3-030-57628-8_9},
  abstract =            {Active learning of timed languages is concerned with
                         the inference of timed automata by observing some of
                         the timed words in their languages. The learner can
                         query for the membership of words in the language,
                         or propose a candidate model and ask if it is
                         equivalent to the target. The major difficulty of
                         this framework is the inference of clock resets,
                         which are central to the dynamics of timed automata
                         but not directly observable. \par Interesting first
                         steps have already been made by restricting to the
                         subclass of event-recording automata, where clock
                         resets are tied to observations. In order to advance
                         towards learning of general timed automata, we
                         generalize this method to a new class, called
                         reset-free event-recording automata, where some
                         transitions may reset no clocks. \par Central to our
                         contribution is the notion of invalidity, and the
                         algorithm and data structures to deal with it,
                         allowing on-the-fly detection and pruning of reset
                         hypotheses that contradict observations. This notion
                         is a key to any efficient active-learning procedure
                         for generic timed automata.},
}