We consider the language of CSP extended with a construct that allows processes to test whether a particular event is available (w ithout actually performing the event). We present an operational semantics for this language, together with two congruent denotational semantic models. We also show how this extended language can be simulated using standard CSP, so as to be able to analyse systems using the model checker FDR.
['Gavin Lowe']
Extending CSP with tests for availability