Nicolas Markey

Abstract

We consider the problems of efficiently diagnosing (and predicting) what did (and will) happen after a given sequence of observations of the execution of a partially-observable one-clock timed automaton. This is made difficult by the facts that timed automata are infinite-state systems, and that they can in general not be determinized.

We introduce timed markings as a formalism to keep track of the evolution of the set of reachable configurations over time. We show how timed markings can be used to efficiently represent the closure under silent transitions of such automata. We report on our implementation of this approach compared to the approach of [Tripakis, Fault diagnosis for timed automata, 2002], and provide some insight to a generalization of our approach to n-clock timed automata.

@article{sttt23(2)-BHJJM,
  author =              {Bouyer, Patricia and Henry, L{\'e}o and Jaziri, Samy
                         and J{\'e}ron, Thierry and Markey, Nicolas},
  title =               {Diagnosing timed automata using timed markings},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {23},
  number =              {2},
  pages =               {229-253},
  year =                {2021},
  month =               apr,
  doi =                 {10.1007/s10009-021-00606-2},
  abstract =            {We~consider the problems of efficiently diagnosing
                         (and~predicting) what did (and~will) happen after a
                         given sequence of observations of the execution of a
                         partially-observable one-clock timed automaton. This
                         is made difficult by the facts that timed automata
                         are infinite-state systems, and that they can in
                         general not be determinized. \par We~introduce timed
                         markings as a formalism to keep track of the
                         evolution of the set of reachable configurations
                         over time. We show how timed markings can be used to
                         efficiently represent the closure under silent
                         transitions of such automata. We report on our
                         implementation of this approach compared to the
                         approach of [Tripakis, Fault diagnosis for timed
                         automata,~2002], and provide some insight to a
                         generalization of our approach to {{\(n\)}}-clock
                         timed automata.},
}