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 B e r r y , 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 odel valuations. Esterel reactions are then characterized as speci c G odel 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 o ers interesting insights into the similarities of and the di erences between Esterel and Statecharts semantics.