Evènement pour le groupe Modélisation et Verification


Date 2009-05-28  11:00-12:15
TitreWhen 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. 
LieuSalle 076, LaBRI, Rez-de-chaussée 
OrateurNathalie Bertrand 
Emailnathalie.bertrand@irisa.fr 
UrlIRISA, Rennes, France 



Aucun document lié à cet événement.

Retour
Retour à l'index