%0 Conference Proceedings
%F icalp09
%A Baier, C.
%A Bertrand, N.
%A Bouyer, P.
%A Brihaye, Th.
%T When are timed automata determinizable?
%B 36th International Colloquium on Automata, Languages and Programming (ICALP'09)
%V 5556
%P 43-54
%S LNCS
%C Rhodes, Greece
%X 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)
%U http://www.irisa.fr/vertecs/Publis/Ps/BBBB-icalp09.pdf
%U http://dx.doi.org/10.1007/978-3-642-02930-1_4
%8 July
%D 2009