Compilation of the ELECTRE reactive language into finite transition systems

We present in this paper an operational semantics for the ELECTRE reactive language (Roux et al., 1992). This language is based on an asynchronous approach to real-time systems. First basic concepts and intuitive semantics are introduced. Then we give rules to model dynamic semantics of ELECTRE programs: this constitutes an operational semantics for the ELECTRE language. This operational semantics is used to define a model of execution for ELECTRE programs: transition system. In addition, we prove, using structural induction on the operational semantics, that this transition system is afinite state transition system. Eventually, we extend the previous transition system so as to handle multiple-storage events: it is important since the asynchronous ELECTRE language deals with multiple memorized occurrences of the events. This result gives a means of compiling the ELECTRE language into a finite-state machine.