On the Undecidability of Universality for Timed Automata with Minimal Resources

Abstract

In 1994 Alur and Dill introduced timed automata and showed that universality was undecidable there. Since then it has been shown that under certain restrictions the problem becomes decidable. But the frontier between decidability and undecidability is still vast. We aim at narrowing this gap considerably. Our main accomplishment is to prove that universality stays undecidable over weakly monotonic time when restricting to a single state, a single symbol and clock comparisons to 0 and 1 only. We further propose that over strongly monotonic time the problem stays undecidable for timed automata with one state and one symbol only.