CCS WITH PRIORITY CHOICE

This paper investigates an extension of Milner's CCS with a priority choice operator called prisum: this operator is very similar to the PRIALT construct of Occam. The new binary prisum operator only allows execution of its second component in the case where the environment is not ready to allow the first component to proceed. This dependency on the set of actions the environment is ready to perform goes beyond that encountered in traditional CCS. Its expression leads to a novel 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 agents with priority 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 prisum. The laws are conservative over agents of traditional CCS. (C) 1995 Academic Press, Inc.