Jump to : Download | Abstract | Contact | BibTex reference | EndNote reference |


C. Baier, N. Bertrand, P. Bouyer, Th. Brihaye. When are timed automata determinizable?. In 36th International Colloquium on Automata, Languages and Programming (ICALP'09), LNCS, Volume 5556, Pages 43-54, Rhodes, Greece, July 2009.

Download [help]

Download paper: Doi page

Download paper: Adobe portable document (pdf) pdf

Copyright notice: This 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.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic


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 http://www.irisa.fr/prive/nbertran/

BibTex Reference

   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)},
   Volume = {5556},
   Pages = {43--54},
   Series = {LNCS},
   Address = {Rhodes, Greece},
   Month = {July},
   Year = {2009}

EndNote Reference [help]

Get EndNote Reference (.ref)