Synchronous languages such as Esterel or Statecharts with their underlying cycle-based computation principle (synchrony hypothesis, maximal progress, run-to-completion) are very popular among engineers and widely used in the programming of reactive and embedded systems. Traditionally, the development platforms for such languages were built mainly with simulation and code-generation in mind. Only recently increasing efforts are being made on the integration of semantic validation techniques (model-checking, theorem-proving, test sequence generation, etc). These efforts depend crucially on modular semantics of the standard two-level micro-macro step model which are notoriously hard to come by.
In this project aims to show how the Synchronoy Hypothesis and some of the recent successful proposals for solving the compositionality problem for Statecharts and Esterel can be understood in a game-theoretic way. Technically, synchronous programs are mapped into finite two-player games in such a way that the analysis of signal statuses is reflected in the computation of winning strategies. This game-theoretic approach offers a new semantical foundation for synchronous languages.