Aalborg Universitet New Results on Timed

Recently, we have proposed a new design theory for timed syst ems. This theory, building on Timed I/O Automata with game semant ics, includes classical operators like satisfaction, consistency, logical c omposition and structural composition. This paper presents a new efficient algorithm f or checking Büchi objectives of timed games. This new algorithm can be used to s trengthen the infinite behavior of an interface, or to guarantee that the inte rfac can indeed be implemented. We illustrate the framework with an infrared s nsor case study.