When are timed automata determinizable?

Abstract : In this paper, we propose an abstract procedure which, given a timed automaton, produces a language-equivalent deterministic infinite timed tree. We prove that under a certain boundedness condition, the infinite timed tree can be reduced into a classical deterministic timed automaton. The boundedness condition is satisfied by several subclasses of timed automata, some of them were known to be determinizable (event-clock timed automata, automata with integer resets), but some others were not. We prove for instance that strongly non-Zeno timed automata can be determinized. As a corollary of those constructions, we get for those classes the decidability of the universality and of the inclusion problems, and compute their complexities (the inclusion problem is for instance EXPSPACE-complete for strongly non-Zeno timed automata).
Type de document :
Communication dans un congrès
36th International Colloquium on Automata, Languages and Programming (ICALP'09), Jul 2009, Rhodes, Greece. Springer, 5556, pp.43-54, 2009, LNCS. 〈10.1007/978-3-642-02930-1_4〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00424351
Contributeur : Nathalie Bertrand <>
Soumis le : jeudi 15 octobre 2009 - 11:29:04
Dernière modification le : jeudi 11 janvier 2018 - 06:20:13

Identifiants

Collections

Citation

Christel Baier, Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye. When are timed automata determinizable?. 36th International Colloquium on Automata, Languages and Programming (ICALP'09), Jul 2009, Rhodes, Greece. Springer, 5556, pp.43-54, 2009, LNCS. 〈10.1007/978-3-642-02930-1_4〉. 〈inria-00424351〉

Partager

Métriques

Consultations de la notice

260