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

https://hal.inria.fr/inria-00424351
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

Identifiers

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

Share

Metrics

Record views

348