Skip to Main content Skip to Navigation
Conference papers

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).
Document type :
Conference papers
Complete list of metadata
Contributor : Nathalie Bertrand Connect in order to contact the contributor
Submitted on : Thursday, October 15, 2009 - 11:29:04 AM
Last modification on : Tuesday, March 30, 2021 - 12:12:08 PM

Links full text



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. pp.43-54, ⟨10.1007/978-3-642-02930-1_4⟩. ⟨inria-00424351⟩



Record views