Recently, we have proposed a new design theory for timed systems.
This theory, building on Timed I/O Automata with game semantics, includes clas-
sical operators like satisfaction, consistency, logical composition and structural
composition. This paper presents a new efficient algorithm for checking Büchi
objectives of timed games. This new algorithm can be used to strengthen the in-
finite behavior of an interface, or to guarantee that the interface can indeed be
implemented. We illustrate the framework with an infrared sensor case study.