CCS with priority choice

An extension of Milner´s CCS with a priority choice operator called prisum is investigated. This operator is very similar to the PRIALT construct of Occam. The binary prisum operator only allows execution of its second component in the case in which 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 read-sets (of the environment) as well as the normal action symbols from CCS. A notion of strong bisimulation is defined on agents with priority by means of 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