Refusal testing (Q580961)

When manipulating concurrent processes it is desirable to suppress their internal details and to consider two processes to be equivalent if their external behaviours are equivalent. Following Milner and De Nicola \& Hennessy we take this external equivalence to mean that an observer cannot tell the processes apart by testing their responses to the same stimuli. We introduce a form of testing (refusal testing) which is more powerful than that of De Nicola \& Hennessy in that the observer not only tests whether a process will perform an action but is also allowed under certain circumstances to discover in a finite amount of time that the process will not perform an action. The equivalence associated with refusal testing is compared with De Nicola \& Hennessy's testing equivalence and Milner's observation equivalence, and a sound and complete proof system is provided for refusal equivalence when applied to CCS processes.