Abstract:
We study testing preorders for an asynchronous
version of CCS called TACCS, where message
emission is non blocking.
We first give a labelled transition system semantics for
this language, which includes both external and internal choice
operators. By applying the standard definitions of may and must testing to this
semantics we obtain two behavioural preorders based on
asynchronous observations.
We present alternative behavioural characterisations of these preorders,
which are subsequently used to obtain equational
theories for the finite fragment of the language.