Im Rahmen unseres Seminars SFB/TRR89 InvasIC hielt Prof. Mendler den Vortrag „Game-theoretic Semantics of Synchronous Reactions“
The synchronous model of programming, which emerged in the 1980ies and has led to the development of well-known languages such as Statecharts, Esterel, Signal, Lustre, has made the programming of concurrent systems with deterministic and bounded reaction a routine exercise. However, validity of this model is not for free. It depends on the Synchrony Hypothesis according to which a system is invariably faster than its environment. Yet, this raises a tangled compositionality problem. Since a node is in the environment of the every other node, it follows that each node must be faster than every other and hence faster than itself!
This talk presents a game-theoretic semantics of boolean logic defining the constructive interpretation of step responses for synchronous languages. This provides a coherent semantic framework encompassing both non-deterministic Statecharts (as per Pnueli & Shalev) and deterministic Esterel. The talk sketches a general theory for obtaining different notions of constructive responses in terms of winning conditions for finite and infinite games and their characterisation as maximal post-fixed points of functions in directed complete lattices of intensional truth-values.
Weitere Informationen finden Sie auf unserer InvasIC Weseite