New Results on Timed Specifications

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 structuralcomposition. This paper presents a new efficient algorithm for checking Büchiobjectives 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 beimplemented. We illustrate the framework with an infrared sensor case study.