Determinacy with Priorities up to Clocks
Luigi Liquori (Centre Inria de l'Universit\'e C\^ote d'Azur), Michael Mendler (University of Bamberg), Claude Stolze (University of Bamberg)

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
