Axiomatizing an Algebra of Step Reactions for Synchronous Languages Gerald Luettgen and Michael Mendler
This paper introduces a novel algebra for reasoning about step
reactions in synchronous languages, such as macro steps in Harel,
Pnueli and Shalev's Statecharts and instantaneous reactions in Berry's
Esterel. The algebra describes step reactions in terms of
configurations which can both be read in a standard operational as
well as in a model-theoretic fashion. The latter arises by viewing
configurations as propositional formulas, interpreted
intuitionistically over finite linear Kripke structures. Previous
work by the authors showed the adequacy of this approach by
establishing compositionality and full-abstraction results for
Statecharts and Esterel. The present paper generalizes this work in
an algebraic setting and, as its main result, provides a sound and
complete equational axiomatization of step reactions. This yields,
for the first time in the literature, a complete axiomatization of
Statecharts macro steps, which can also be applied, modulo encoding,
to Esterel reactions.
|
concur02@fi.muni.cz |