Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper extends CCS with priority-guarded actions and clocks to enable compositional encoding of synchronous programming languages like Esterel. It introduces a new concept of "coherence" to enrich Milner's original notion of confluence, addressing limitations in expressing causality and shared memory multi-threading with reaction to absence. The extended calculus allows for a more accurate and compositional representation of determinate concurrent systems.
Synchronous programming languages like Esterel can now be compositionally encoded within an extended CCS framework, bridging the gap between process algebra confluence theory and determinate concurrent semantics.
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.