Evènement pour le groupe Modélisation et Verification


Date 2010-12-02  11:30-12:45
TitreEfficient Emptiness Check for Timed Büchi Automata 
RésuméThe Büchi non-emptiness problem for timed automata concerns deciding if a given automaton has an infinite non-Zeno run satisfying the Büchi accepting condition. The standard solution to this problem involves adding an auxiliary clock to take care of the non-Zenoness. In this talk, we show that this simple transformation may sometimes result in an exponential blowup. Then, we propose a method avoiding this blowup. However, in many cases, no extra construction is needed to ascertain non-Zenoness. Hence, we finally present an on-the-fly algorithm for the non-emptiness problem, using an efficient non-Zenoness construction only when required. 
LieuSalle 076, LaBRI, Rez-de-chaussée 
OrateurFrédéric Herbreteau 
Emailfh@labri.fr 
UrlLaBRI 



Aucun document lié à cet événement.

Retour
Retour à l'index