|
Evènement pour le groupe Modélisation et Verification
Date | 2009-05-28 11:00-12:15 |
Titre | When are Timed Automata Determinizable? |
Résumé | We describe an abstract procedure which, given a timed automaton, produces a language-equivalent deterministic infinite timed tree. Under a certain boundedness condition, the infinite timed tree can be reduced into a classical deterministic timed automaton. The boundedness condition we exhibit 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).
This is a joint work with C. Baier, P. Bouyer and T. Brihaye. |
Lieu | Salle 076, LaBRI, Rez-de-chaussée |
Orateur | Nathalie Bertrand |
Email | nathalie.bertrand@irisa.fr |
Url | IRISA, Rennes, France |
Aucun document lié à cet événement. RetourRetour à l'index
| |