Résumé | Timed automata are frequently used to model real-time systems.
Their determinization is a key issue for several validation problems.
However, not all timed automata can be determinized, and determinizability
itself is undecidable. In this talk, we will present a game-based algorithm
which, given a timed automaton,
tries to produce a language-equivalent deterministic timed automaton,
otherwise a deterministic over-approximation. Our method subsumes two
recent contributions: it is at once more general than a recent determinization
procedure and more precise than the existing over-approximation algorithm.Then, we will explain how this method can be adapted to be usefull for test generation.
This talk is a joint work with Nathalie Bertrand, Thierry Jéron and Moez Krichen. Papers will be presented at FoSSaCs'11 and TACAS'11. |