inria-00524830, version 2
A game approach to determinize timed automata
Nathalie Bertrand a, 1Amélie Stainer
a, 1Thierry Jéron
a, 1Moez Krichen 2
N° RR-7381 (2010)
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 paper, we propose 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 the determinization procedure of [BBBB09a] and more precise than the approximation algorithm of [KT09]. Moreover, we explain how to extend our method to deal with invariants and $\varepsilon$-transitions, and also consider other useful approximations: under-approximation, and combination of under- and over-approximations.
- a – INRIA
- 1 : VERTECS (INRIA)
- INRIA
- 2 : Institut Supérieur d'Informatique et de Multimédia de Sfax (ISIMS)
- University of Sfax, Tunisia
- Domaine : Informatique/Informatique et langage
Informatique/Théorie et langage formel
- Référence interne : RR-7381
- Versions disponibles : v1 (11-10-2010) v2 (25-10-2010)
- inria-00524830, version 2
- http://hal.inria.fr/inria-00524830
- oai:hal.inria.fr:inria-00524830
- Contributeur : Nathalie Bertrand
- Soumis le : Lundi 25 Octobre 2010, 11:07:46
- Dernière modification le : Vendredi 15 Avril 2011, 10:54:06