A Deterministic Logical Semantics for Esterel

Esterel is a synchronous design language for the specification of reactive systems. There exist two main semantics for Esterel. On the one hand, the logical behavioral semantics provides a simple and compact formalization of the behavior of programs using SOS rules. But it does not ensure deterministic executions for all programs and all inputs. As non-deterministic programs have to be rejected as incorrect, this means it defines behaviors for incorrect programs, which is not convenient. On the other hand, the constructive semantics is deterministic (amongst other properties) but at the expense of a much more complex formalism. In this work, we construct and thoroughly analyze a new deterministic semantics for Esterel that retains the simplicity of the logical behavioral semantics, from which it derives. In our view, it provides a much better framework for formal reasoning about Esterel programs.