Determinacy with Priorities up to Clocks

TL;DR

This paper extends CCS with priorities and clocks to incorporate a new notion of coherence, enabling the encoding of synchronous languages like Esterel within a compositional framework.

Contribution

It introduces an extension of CCS with priority-guarded actions and clocks, enriching Milner's confluence theory with a new concept of coherence for better expressiveness.

Findings

Enables encoding of synchronous languages such as Esterel within CCS.

Introduces the concept of coherence to extend confluence theory.

Provides a compositional approach to express causality and shared memory.

Abstract

In Milner's seminal book on communication and concurrency introducing CCS, a process algebra inherently non-deterministic, chapter 11 was completely devoted to introduce the notion of determinacy and confluence in order to identify a subcalculus of CCS in which all definable agents are confluent. At the same time, or shortly later, determinate semantics were given for programming languages that reconcile concurrency and determinacy, such as Esterel by Berry and Gonthier, or SL by Boussinot and de Simone. These dedicated semantics do not easily map to Milner's confluence theory for CCS, which is unable to express causality and shared memory multi-threading with reaction to absence in a compositional way. We present an extension of CCS with priority-guarded actions and clocks, and we exploit the added expressiveness to enrich Milner's original notion of confluence by the new concept of coherence which permits us to encode, in a compositional fashion, synchronous programming languages such as Esterel.