Hello,

For the next meeting, we will discuss the attached paper and I'll host the discussion. The meeting will take place in Room 349 on Monday, December 11th at noon.

Abstract: 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 sur- prising, 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 algorithm. We also show that the language inclusion problem is decidable if the only con- stant 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.

See you, Kyveli