loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
19th Annual IEEE Symposium on Logic in Computer Science (LICS'04)
On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap
Turku, Finland
July 13-July 17
ISBN: 0-7695-2192-4
Jo? Ouaknine, Carnegie Mellon University, Pittsburgh, PA
James Worrell, Tulane University, New Orleans, LA
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.
Citation:
Jo? Ouaknine, James Worrell, "On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap," lics, pp.54-63, 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), 2004
Usage of this product signifies your acceptance of the Terms of Use.