-
Selection by year
-
Selection by authors
-
Complete lists
icalp09
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: Adobe portable document (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
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)
Contact
Nathalie Bertrand http://www.irisa.fr/prive/nbertran/
BibTex Reference
@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)},
Volume = {5556},
Pages = {43--54},
Series = {LNCS},
Address = {Rhodes, Greece},
Month = {July},
Year = {2009}
}
EndNote Reference [help]
Get EndNote Reference (.ref)