Seminarium Teoria Automatów

Prelegent: Slawomir Lasota

For timed automata with two clocks emptyness in decidable but universality and containment are not. We will show that all these problems are decidable for alternating timed automata, but with only one clock. The non-primitive-recursive complexity will be shown. On infinite words, universality (and containment) will be shown undecidable for one-clock Buechi automata. We will also discuss relationships with timed temporal logics, possible extensions of our results and open problems.