During the last few years the area of real time systems has received a lot of attention from the research community. In particular, a variety of specification formalisms has emerged allowing real time properties to be expressed explicitly. These specification formalisms may roughly be divided into two groups, namely: real time logics (eg [AH89, HNSY92]) and real time process algebras (eg [Yi90, NRJV90]).

Central to the ongoing research has been the construction of model-checking algorithms; ie algorithms for deciding whether a given real time system satisfies a given specification. A number of model-checking algorithms exists for real timed logical specifications [ACD90] and more recently algorithms for modelchecking 3 timed process algebraic specifications have been given [Cer92, LY93]. In this work, we deal with the more ambitious goal of model-construction: ie given a real time specification (logical or process algebraic) we want to automatically synthesize a real time system satisfying the specification (if such a system exists). Moreover, we consider the model-construction problem in the setting of implicit specifications, ie: