Logic in Computer Science (LICS 2004)

Paper: On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap (at LICS 2004)

Authors: Joel Ouaknine James Worrell

Abstract

We consider the language inclusion problem for timed automata: given two timed automata A and B, are all the time traces accepted by B also accepted by A? While this problem is know 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 algorithm. 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.

BibTeX

  @InProceedings{OuaknineWorrell-OntheLanguageInclus,
    author = 	 {Joel Ouaknine and James Worrell},
    title = 	 {On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap},
    booktitle =  {Proceedings of the Nineteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2004},
    year =	 2004,
    editor =	 {Harald Ganzinger},
    month =	 {July}, 
    pages =      {54--63},
    location =   {Turku, Finland}, 
    publisher =	 {IEEE Computer Society Press}
  }