Determinacy \(\to\) (observation equivalence \(=\) trace equivalence) (Q1061481)

If an experiment s is conducted on a parallel process p, then, in general, different processes may result from the experiment, due to the nondeterministic behaviour of p (in the notation of Milner [\textit{R. Milner}, A calculus of communicating systems (1980; Zbl 0452.68027)]:p\(\Rightarrow^{s}p'\) for different p'). Process p is called determinate if the resulting processes are all equivalent (i.e., if \(p\Rightarrow^{s}p'\) and \(p\Rightarrow^{s}p''\), then p' and p'' are equivalent). This means that, although p behaves nondeterministically, this cannot be detected by an observer of p. Let \(\simeq\) denote observation equivalence, used in CCS (\textit{Milner}, loc. cit.) let \(\simeq_ f\) denote (the much weaker) failure equivalence, used for CSP [\textit{S. D. Brookes}, Lect. Notes Comput. Sci. 154, 83-96 (1983; Zbl 0516.68024)], and let \(\simeq_ t\) denote (the still weaker) trace equivalence. We show that the three corresponding notions of determinacy are the same, and that for determinate processes \(\simeq\), \(\simeq_ f\), and \(\simeq_ t\) are the same. Determinacy is preserved under \(\simeq\) and \(\simeq_ f\), but not under \(\simeq_ t\).