1 Introduction
Many computer applications, usually called reactive systems, involve time-critical aspects and often require a pro-grannner to specify timing constraints such as, for example, that an input is required within a bounded period of time. Reactive systems include real-time systems which are subject to hard timing constraints (e.g. process controllers and signal processing systems). Many different formalisms have been developed to specify, verify and program reactive systems, including (several) timed process algebras (see for example [1], [10]), temporal logic (and its executable versions) [12], [9] and the concurrent synchronous languages ESTEREL, LUSTRE, _ SIGNAL and Statecharts which have been already been used in many industrial applications.