Compilation of the ELECTRE reactive language into finite transition systems

Franck Cassez, Olivier Roux*

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

18 Citations (Scopus)


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.

Original languageEnglish
Pages (from-to)109-143
Number of pages35
JournalTheoretical Computer Science
Issue number1-2
Publication statusPublished - 24 Jul 1995
Externally publishedYes


Dive into the research topics of 'Compilation of the ELECTRE reactive language into finite transition systems'. Together they form a unique fingerprint.

Cite this