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: