2.00 p.m.
Efficient Emptiness Check for Timed Buechi Automata
B. Srivathsan
LaBRI, Bordeaux, France.
12-08-10

---

Abstract

The Buechi non-emptiness problem for timed automata concerns deciding if a given automaton has an infinite non-Zeno run satisfying the Buechi accepting condition. The standard solution to this problem involves adding an auxiliary clock to take care of the non-Zenoness. In this paper, we show that this simple transformation may sometimes result in an exponential blowup. We propose a method avoiding this blowup.

This is joint work with F. Herbretau and Igor Walukiewicz.