Jump to : Download | Abstract | Contact | BibTex reference | EndNote reference |
Download paper Adobe portable document format (pdf)
Copyright noticeThis material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
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).
Nathalie Bertrand
nathalie.bertrand@irisa.fr
@InProceedings{icalp09,
Author = {Baier, C. and Bertrand, N. and Bouyer, P. and Brihaye, Th.},
Title = {When are timed automata determinizable? },
BookTitle = {36th International Colloquium on Automata, Languages and Programming (ICALP'09), LNCS No 5556},
Pages = {43--54},
Address = {Rhodes, Greece},
Month = {July},
Year = {2009}
}
Get EndNote Reference (.ref)