pith. sign in

arxiv: 2604.06879 · v1 · submitted 2026-04-08 · 💻 cs.PL · cs.DC· cs.SE

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) This is my paper

Pith reviewed 2026-05-10 18:04 UTC · model grok-4.3

classification 💻 cs.PL cs.DCcs.SE
keywords CCSconfluencecoherenceprioritiesclocksEstereldeterminacyprocess algebra
0
0 comments X

The pith

Extending CCS with priority-guarded actions and clocks enriches confluence into coherence for compositional encodings of Esterel.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper extends Milner's CCS with priority-guarded actions and clocks. This addition allows the definition of coherence, a property that strengthens determinacy and confluence beyond Milner's original theory. Coherence supports compositional encodings of synchronous languages like Esterel, addressing limitations in expressing causality and reaction to absence. A sympathetic reader would care because it bridges process algebra with practical deterministic concurrent programming.

Core claim

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.

What carries the argument

Coherence, defined using priority-guarded actions and clocks in the extended CCS, which enriches confluence to ensure determinacy and compositional encodings.

Load-bearing premise

The coherence property is preserved compositionally under the extended operators and that the encoding of Esterel-style reaction to absence remains faithful without introducing hidden non-determinism.

What would settle it

A concrete Esterel program whose encoding into the extended CCS exhibits observable non-determinism despite satisfying coherence would falsify the claim.

Figures

Figures reproduced from arXiv: 2604.06879 by Claude Stolze (University of Bamberg), Luigi Liquori (Centre Inria de l'Universit\'e C\^ote d'Azur), Michael Mendler (University of Bamberg).

Figure 1
Figure 1. Figure 1: Labelled Transition System (LTS) for CCSspt . • Each element (C,L) ∈ B is a blocking constraint from a thread participating in the transition α:B[ι], that only participates provided there cannot be a synchronisation on any of the actions L, within the clock horizon C. The horizon {σ} consists of all actions possibly taken before the clock σ is executed, i.e., it does not include any action happening after … view at source ↗
Figure 2
Figure 2. Figure 2: Store S , Readers Ri and Writers Wi , in CCSspt (left) and strategic transitions (right). lifts the blocking set L of the prefix to a blocking constraint in the scope of the thread’s clock. Note, by well-formedness, clock(α:L.P) = clock(P). • (Sum) The iterated application of the summation rule permits us to select any prefix αn:Ln.Pn of a thread M = P i αi :Li .Pi , generating a transition αn:B[ι] of M to… view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The manuscript extends CCS with priority-guarded actions and clocks, enriching Milner's confluence with a new coherence property that enables a compositional encoding of synchronous languages such as Esterel while preserving determinacy.

Significance. If the definitions and proofs establish that coherence is preserved under the extended operators and that the encoding of reaction to absence remains faithful, the result would bridge process-algebraic determinacy with synchronous programming semantics, addressing limitations in expressing causality and shared-memory constructs compositionally.

major comments (1)
  1. Abstract: the central claim that coherence permits a compositional encoding of Esterel-style reaction to absence is load-bearing, yet the abstract provides no definition of the priority-guarded actions, clocks, coherence, or the encoding function, preventing verification that coherence is preserved without introducing hidden non-determinism.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their thoughtful summary and for highlighting the importance of the abstract's clarity regarding our central claims. We address the single major comment below.

read point-by-point responses

  1. Referee: Abstract: the central claim that coherence permits a compositional encoding of Esterel-style reaction to absence is load-bearing, yet the abstract provides no definition of the priority-guarded actions, clocks, coherence, or the encoding function, preventing verification that coherence is preserved without introducing hidden non-determinism.

    Authors: We agree that the abstract is deliberately concise and omits formal definitions of priority-guarded actions, clocks, coherence, and the encoding function. These are introduced and formalized in the body of the paper: priority-guarded actions and clocks appear in the syntax and operational semantics (Section 2), coherence is defined as an extension of Milner's confluence in Section 3, and the compositional encoding of Esterel (including reaction to absence) together with the coherence-preservation theorems are given in Section 4. The proofs establish that the encoding introduces no hidden non-determinism. To make the load-bearing claim more immediately verifiable from the abstract alone, we will revise it to include brief informal characterizations of the key notions together with forward references to the relevant sections. revision: yes

Circularity Check

0 steps flagged

No significant circularity detected in derivation chain

full rationale

The paper extends Milner's CCS with priority-guarded actions and clocks as new operators, then defines coherence as an enrichment of confluence to support compositional encodings of Esterel-style synchronous programs. This is a standard definitional and theorem-proving contribution that builds on external prior results (Milner) without any quoted reduction of a central claim to a self-fit, self-citation chain, or input-by-construction. No self-definitional loops, fitted predictions renamed as results, or load-bearing uniqueness theorems from the authors themselves appear in the abstract or high-level argument. The derivation remains self-contained against the external benchmark of Milner's confluence theory.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract provides no explicit free parameters, axioms, or invented entities; all details are deferred to the full text.

pith-pipeline@v0.9.0 · 5487 in / 987 out tokens · 38016 ms · 2026-05-10T18:04:30.090266+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

21 extracted references · 21 canonical work pages

  1. [1]

    R. M. Amadio (2007): A Synchronous π-Calculus. Information and Computation 9(205), pp. 1470–1490, doi:10.1016/j.ic.2007.02.002

    work page doi:10.1016/j.ic.2007.02.002 2007

  2. [2]

    H. R. Andersen & M. Mendler (1994): An asynchronous process algebra with multiple clocks. In: Proc. ESOP, pp. 58–73, doi:10.1007/3-540-57880-3_4

    work page doi:10.1007/3-540-57880-3_4 1994

  3. [3]

    Berry (1999): The Constructive Semantics of Pure Esterel

    G. Berry (1999): The Constructive Semantics of Pure Esterel. Draft Book

    work page 1999

  4. [4]

    Bliudze & J

    S. Bliudze & J. Sifakis (2007): The algebra of connectors: structuring interaction in BIP. In: Proc. of EM- SOFT, ACM, pp. 11–20, doi:10.1145/1289927.1289935

    work page doi:10.1145/1289927.1289935 2007

  5. [5]

    R. Bol & J. F. Groote (1996): The Meaning of Negative Premises in Transitions System Specifications. JACM 43(5), pp. 863–914, doi:10.1145/234752.234756

    work page doi:10.1145/234752.234756 1996

  6. [6]

    Boussinot & R

    F. Boussinot & R. de Simone (1996): The SL synchronous language. IEEE Transactions on Software Engi- neering 22(4), pp. 256–266, doi:10.1109/32.491649

    work page doi:10.1109/32.491649 1996

  7. [7]

    Camilleri & G

    J. Camilleri & G. Winskel (1995): CCS with priority choice. Information and Computation 116(1), pp. 26– 37, doi:10.1006/INCO.1995.1003

    work page doi:10.1006/inco.1995.1003 1995

  8. [8]

    Cleaveland, G

    R. Cleaveland, G. Lüttgen & M. Mendler (1997): An Algebraic Theory of Multiple Clocks. In: Proc. of CONCUR, LNCS 1243, pp. 166–180, doi:10.1007/3-540-63141-0_12

    work page doi:10.1007/3-540-63141-0_12 1997

  9. [9]

    Cleaveland, G

    R. Cleaveland, G. Lüttgen & V . Natarajan (1998): A Process Algebra with Distributed Priorities. Theor. Comput. Sci. 195(2), pp. 227–258, doi:10.1016/S0304-3975(97)00221-1

    work page doi:10.1016/s0304-3975(97)00221-1 1998

  10. [10]

    Dokter, S.-S

    K. Dokter, S.-S. Jongmans, F. Arbab & S. Bliudze (2017): Combine and Conquer: Relating BIP and Reo. Journal of Logical and Algebraic Methods in Programming 86, pp. 134–156, doi:10.1016/j.jlamp.2016.09.008

    work page doi:10.1016/j.jlamp.2016.09.008 2017

  11. [11]

    Maximal sound predictive race detection with control flow abstraction

    R. von Hanxleden, B. Duderstadt, C. Motika, S. Smyth, M. Mendler, J. Aguado, S. Mercer & O. O’Brien (2014): SCCharts: Sequentially Constructive Statecharts for Safety-Critical Applications. In: Proc. of PLDI, ACM, pp. 372–383, doi:10.1145/2594291.2594310

    work page doi:10.1145/2594291.2594310 2014

  12. [12]

    Hennessy & T

    M. Hennessy & T. Regan (1995): A process algebra for timed system. Information and Computation 117, pp. 221–239, doi:10.1006/INCO.1995.1041

    work page doi:10.1006/inco.1995.1041 1995

  13. [13]

    Hoare (1985): Communicating Sequential Processes

    C.A.R. Hoare (1985): Communicating Sequential Processes. Prentice-Hall. 256 pages

    work page 1985

  14. [14]

    Liquori, M

    L. Liquori, M. Mendler & C. Stolze (2026): A process calculus with clocks and priorities. https://inria. hal.science/hal-05497982

    work page 2026

  15. [15]

    Lüttgen, M

    G. Lüttgen, M. von der Beeck & R. Cleaveland (1999): Statecharts Via Process Algebra. In: Proc. of CON- CUR, LNCS 1664, Springer, pp. 399–414, doi:10.1007/3-540-48320-9_28

    work page doi:10.1007/3-540-48320-9_28 1999

  16. [16]

    Milner (1983): Calculi for Synchrony and Asynchrony

    R. Milner (1983): Calculi for Synchrony and Asynchrony. Theor. Comput. Sci. 25, pp. 267–310, doi:10.1016/0304-3975(83)90114-7

    work page doi:10.1016/0304-3975(83)90114-7 1983

  17. [17]

    Milner (1989): Communication and Concurrency

    R. Milner (1989): Communication and Concurrency. Prentice Hall

    work page 1989

  18. [18]

    Nicollin & J

    X. Nicollin & J. Sifakis (1994): The Algebra of Timed Processes, ATP: Theory and Application. Inf. Com- put. 114(1), pp. 131–178, doi:10.1006/INCO.1994.1083

    work page doi:10.1006/inco.1994.1083 1994

  19. [19]

    Phillips (2008): CCS with priority guards

    I. Phillips (2008): CCS with priority guards. The Journal of Logic and Algebraic Programming 75(1), pp. 139–165, doi:10.1016/J.JLAP.2007.06.005

    work page doi:10.1016/j.jlap.2007.06.005 2008

  20. [20]

    Lüttgen R

    G. Lüttgen R. Cleaveland & V . Natarajan (2001): Priority in Process Algebra. In: Handbook of Process Algebra, North-Holland / Elsevier, pp. 711–765, doi:10.1016/B978-044482830-9/50030-8

    work page doi:10.1016/b978-044482830-9/50030-8 2001

  21. [21]

    Versari, M

    C. Versari, M. Busi & R. Gorrieri (2009): An expressiveness study of priority in process calculi. Mathemat- ical Structures in Computer Science 6(19), pp. 1161—-1189, doi:10.1017 /S0960129509990168

    work page 2009