Towards a Model Theory for Esterel
Gerald Lüttgen, Michael Mendler · Electronic Notes in Theoretical Computer Science · 2002
Esterel is a synchronous language for reactive-systems design and builds the core of the commercial tool Esterel Studio. This paper shows how the constructive semantics of a combinational fragment of Esterel, as presented by Berry, can be derived in a model-theoretic fashion, thus complementing the existing behavioral, operational, and circuit-based approaches to Esterel semantics. Technically, Esterel programs are read as formulas in propositional intuitionistic logic, which are interpreted over simple linear Kripke structures, referred to as Gödel valuations. Esterel reactions are then characterized as specific Gödel valuations, called response models, and it is shown that the approach is compositional in the structure of Esterel programs. The obtained results are an important step towards explaining the logic behind Esterel semantics. In addition, the intuitionistic setting advocated in this paper nicely links to Pnueli and Shalev's semantics of Harel's Statecharts, another synchronous language for reactive-systems design. This offers interesting insights into the similarities of and the differences between Esterel and Statecharts semantics.