Parosh Aziz Abdulla (Uppsala University), Language Inclusion for Timed Automata

We consider the language inclusion problem for timed automata. Alur and Dill showed in 1994 that the problem is undecidable if the automata are allowed to have at least two clocks. Recently, Ouaknine and Worrell showed that the problem becomes decidable in case the automata are restricted to have single clocks.

In this presentation, we describe a zone-based algorithm for the one-clock language inclusion problem over finite words. We also show the following results:

1. Language inclusion is undecidable for single-clock timed automata over infinite words. This reveals a surprising divergence between the theory of timed automata over finite words and over infinite words

2. If epsilon-transitions or non-singular postconditions are allowed, then the one-clock language inclusion problem is undecidable over both finite and infinite words.

3. Language inclusion has non-primitive recursive complexity for single-clock timed automata over finite words.