Refusal testing. (English) Zbl 0626.68011

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.


68N25 Theory of operating systems
Full Text: DOI


[1] Abramsky, S., Observation equivalence as a testing equivalence, Theoret. comput. sci., 53, 3, (1987), to appear. · Zbl 0626.68016
[2] Baeten, J.C.M.; Bergstra, J.A.; Klop, J.W., Ready trace semantics for concrete process algebra with priority operator, () · Zbl 0627.68016
[3] Bergstra, J.A.; Klop, J.W., Process algebra for synchronous communication, Inform. and control, 60, 109-137, (1984) · Zbl 0597.68027
[4] Barwise, K.J., Admissible sets and structures, (1975), Springer Berlin
[5] Brookes, S.D.; Hoare, C.A.R.; Roscoe, A.W., A theory of communicating sequential processes, J. ACM, 31, 560-569, (1984) · Zbl 0628.68025
[6] De Nicola, R.; Hennessy, M.C.B.; De Nicola, R.; Hennessy, M.C.B., Testing equivalences for processes, (), 548-560 · Zbl 0515.68029
[7] Hennessy, M.C.B., An algebraic theory of processes (part 2), () · Zbl 0437.68002
[8] Hennessy, M.C.B.; Milner, R., On observing nondeterminism and concurrency, (), 299-309
[9] Hennessy, M.C.B.; Milner, R., Algebraic laws for nondeterminism and concurrency, J. ACM, 32, 137-161, (1985) · Zbl 0629.68021
[10] Hennessy, M.C.B.; Plotkin, G., A term model for CCS, (), 261-274 · Zbl 0479.68011
[11] Milner, R., A calculus of communicating systems, () · Zbl 0452.68027
[12] Milner, R., A modal characterisation of observable machine-behaviour, (), 25-34 · Zbl 0474.68074
[13] Phillips, I.C.C., Refusal testing, (), 304-313
[14] Pnueli, A., Linear and branching structures in the semantics and logics of reactive systems, (), 15-32
[15] Smyth, M.B., Power domains and predicate transformers: a topological view, (), 662-675 · Zbl 0533.68018
[16] Stirling, C., Modal logics for communicating systems, Theoret. comput. sci., 49, 2, 3, 311-347, (1987) · Zbl 0624.68019
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.