When are timed automata determinizable?

Christel BaierChristel Baier, Nathalie BertrandNathalie Bertrand, Patricia BouyerPatricia Bouyer, Thomas BrihayeThomas Brihaye

DOI Link

Christel Baier, Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye
When are timed automata determinizable?
Proc. of the 36th International Colloquium on Automata, Languages and Programming (ICALP), volume 5556 of Lecture Notes in Computer Science, 43--54, 2009. Springer

Details
Bibtex

KurzfassungAbstract
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).
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-02930-1_4.

@inproceedings{BBBB2009,
  author    = {Christel Baier and Nathalie Bertrand and Patricia Bouyer and
               Thomas Brihaye},
  title     = {When are timed automata determinizable?},
  booktitle = {Proc. of the 36th International Colloquium on Automata, Languages
               and Programming (ICALP)},
  series    = {Lecture Notes in Computer Science},
  volume    = {5556},
  publisher = {Springer},
  year      = {2009},
  pages     = {43--54},
  doi       = {10.1007/978-3-642-02930-1_4}
}