Timed automata were introduced by Alur and Dill in the early 1990s and
have since become the most prominent modelling formalism for real-time
systems. A fundamental limit to the algorithmic analysis of timed
automata, however, results from the undecidability of the universality
problem: does a given timed automaton accept every timed word? As a
result, much research has focussed on attempting to circumvent this
difficulty, often by restricting the class of automata under
consideration, or by altering their semantics.
In this paper, we study the decidability of universality for classes
of timed automata with minimal resources. More precisely, we consider
restrictions on the number of states and clock constants, as well as
the size of the event alphabet. Our main result is that universality
remains undecidable for timed automata with a single state, over a
single-event alphabet, and using no more than three distinct clock
constants.
Proceedings of FORMATS 07, LNCS 4763, 2007. 14 pages.
PostScript /
PDF
© 2007
Springer-Verlag.