Compositional semantics of non deterministic synchronous languages

Abstract:
A key feature of synchronous languages is that they conciliate concurrency with determinism. This is achieved by detecting so-called causality errors, which occur when the composition of deterministic processes is not deterministic. Although the existing synchronous languages only deal with deterministic programs, it is not a restriction of the approach. We show how a synchronous language can be extended with non deterministic processes, while still ensuring that process composition will never {\em introduce} non determinism. We give an operational semantics of the language, and show that the equivalence relation induced by this semantics is a congruence for all the language constructs.

Reference:

   @INPROCEEDINGS{oracle,
      AUTHOR={F. Maraninchi and N. Halbwachs},
      TITLE={Compositional semantics of non
            deterministic synchronous languages},
      BOOKTITLE={European Symposium on Programming,
      ESOP'96},
      ADDRESS={Linkoping},
      MONTH={April},
      YEAR= 1996
   }

Postscript file