CCS with Priority Guards

It has long been recognised that standard process algebra has difficulty
dealing with actions of different priority, such as for instance an
interrupt action of high priority. Various solutions have been proposed.
We introduce a new approach, involving the addition of "priority guards"
to Milner's process calculus CCS. In our approach, priority is
unstratified, meaning that actions are not assigned fixed levels, so
that the same action can have different priority depending where it
appears in a program. Unlike in other unstratified accounts of priority
in CCS (such as that of Camilleri and Winskel), we treat inputs and
outputs symmetrically. We introduce the new calculus, give examples,
develop its theory (including bisimulation and equational laws), and
compare it with existing approaches. We show that priority adds
expressiveness to both CCS and the pi-calculus.

Finally, we briefly discuss the implications for the addition of
priority to the pi-calculus.