Strong Priority and Determinacy in Timed CCS
Luigi Liquori Michael Mendler
Building on the classical theory of process algebra with priorities, we
identify a new scheduling mechanism, called "sequentially constructive
reduction" which is designed to capture the essence of synchronous programming.
The distinctive property of this evaluation strategy is to achieve
determinism-by-construction for multi-cast concurrent communication. In
particular, it permits us to model shared memory multi-threading with reaction
to absence as it lies at the core of the programming language Esterel. In the
technical setting of CCS extended by clocks and priorities, we prove for a
large class of processes, which we call "structurally coherent" the confluence
property for constructive reductions. We further show that under some syntactic
restrictions, called "pivotable" the operators of prefix, summation, parallel
composition, restriction and hiding preserve structural coherence. This covers
a strictly larger class of processes compared to those that are confluent in
Milner's classical theory of CCS without priorities.