Semantic games for synchrony
Joaquin AGUADO
The Otto Friedrich University
Informatics Theory Group (GdI) Fac. of Information Systems and Applied Computer Science (WIAI), D-96045 Bamberg, GERMANY
joaquin.aguado@wiai.uni-bamberg.de

Abstract:
In this talk, we want to illustrate how the co-contravariant fixed point problem in synchronous languages can be handled by means of a game theoretical approach. For this, we consider a particular subset of Esterel (kernel) for instantaneous reactions. Since configurations can be reducible to parallel composition of transitions, the choice of priorities can be represented using negations and stimulus (environment) can be accounted for as part of the configuration, the kernel consists of the following; nothing, emit s, present s then C, present s else C, C || C and C ; C. This extends our previous work by including composite conditions (Boolean triggers) and sequencing (C ; C).

For the considered fragment, we show that the Must/Cannot analysis of combinational Esterel corresponds to the computation of winning strategies of a particular game (the maze), where sequencing is modelled by a notion of stratified plays.

Slides: