Some unexpected facts about priority and fairness in CSP

We have recently implemented the operator prioritise(P,As), where As is a list of disjoint subsets of Events (=Σ). These sets are given successively lower priority, with the first (which may be empty) having equal priority with tau. There is no need for the union of As to be the whole of Events: other events are neither of higher nor lower priority than any other. This encompasses and substantially generalises the the tau-priority model previously implemented for timed systems.

I will describe the compositionality properties of this operator, which prove to be different from what had been expected.

I will also show that it is possible, in many circumstances, to use priority to capture properties of a process's unstable failures: the combination of its stable failures and failures (s,X) where the process can perform the trace s and diverge, even when offered the set X under the assumption of acceptance fairness: if a process could normally pass through infinitely many states in a tau-chain in which externally offered events are possible, then one of these events occurs so divergence does not.