|
|
|
Intitulé:
Efficient Emptiness Check for Timed Büchi Automata du groupe Modélisation et Verification
|
Date | 2010-12-02 11:30-12:45 |
Titre | Efficient 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. |
Lieu | Salle 076, LaBRI, Rez-de-chaussée |
Orateur | Frédéric Herbreteau |
Email | fh@labri.fr |
Url | LaBRI |
Aucun document lié à cet événement. RetourRetour à l'index
| |