A conditional operator for CCS

Abstract

This paper investigates an extension of Milner's CCS with a conditional operator called unless [Cam90]. The agent $\mathcal{K} \triangleright E$, pronounced E unless $\mathcal{K}$, behaves as E unless the environment is ready to perform any action in the set $\mathcal{K}$. This dependency on the set of actions the environment is ready to perform goes beyond that encountered in traditional CCS. Its expression is realised by an operational semantics in which transitions carry ready-sets (of the environment) as well as the normal action symbols from CCS. A notion of strong bisimulation is defined on conditional agents via this semantics. It is a congruence and satisfies new equational laws (including a new expansion law) which are shown to be complete for finite agents with the unless operator. The laws are conservative over agents of traditional CCS. The unless operator provides a rudimentary means of expressing bias (or priority) in the behaviour of agents; it is more expressive than the prisum operator presented in [CW91] and [Cam90].