The TTM/RTTL framework was first presented in [111], and in detail in [102]. It includes the following elements: (a) a semantic model of time, (b) a generic computational model (Timed Transition Models4) for modelling plants and controllers, (c) an abstract specification language (Real-Time Temporal Logic), (d) verification methodologies including model-checking for finite state systems, and a deductive proof system for infinite state systems, and (e) heuristics for constructing proofs and controller synthesis methods [104,105,110,107,109,108]. The first four elements represent an extension of untimed Manna-Pnueli temporal logic [82] to timed systems. Each of these elements is discussed below.