We consider the language inclusion problem for timed automata:
given two timed automata A and B, are all the timed traces
accepted by B also accepted by A? While this problem is known to
be undecidable, we show here that it becomes decidable if A is
restricted to having at most one clock. This is somewhat surprising,
since it is well-known that there exist timed automata with a single
clock that cannot be complemented. The crux of our proof consists in
reducing the language inclusion problem to a reachability question on
an infinite graph; we then construct a suitable well-quasi-order on
the nodes of this graph, which ensures the termination of our search
We also show that the language inclusion problem is decidable if the only constant appearing among the clock constraints of A is zero. Moreover, these two cases are essentially the only decidable instances of language inclusion, in terms of restricting the various resources of timed automata.
Proceedings of LICS 04, 2004. 10 pages.
© 2004 IEEE Computer Society Press.