Determinacy \(\to\) (observation equivalence \(=\) trace equivalence). (English) Zbl 0571.68018

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 [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 (Milner, loc. cit.) let \(\simeq_ f\) denote (the much weaker) failure equivalence, used for CSP [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\).


68N25 Theory of operating systems
Full Text: DOI


[1] Brookes, S.D., On the relationship of CCS and CSP, (), 83-96
[2] Brookes, S.D.; Rounds, W.C., Behaviourial equivalence of relations induced by programming logics, (), 97-108
[3] Hoare, C.A.R.; Brookes, S.D.; Roscoe, A.W.; Hoare, C.A.R.; Brookes, S.D.; Roscoe, A.W., A theory of communicating sequential processes, (), J. ACM, 31, 560-599, (1984), also · Zbl 0628.68025
[4] Milner, R., A calculus of communicating systems, () · Zbl 0452.68027
[5] Milner, R., Calculi for synchrony and asynchrony, Theoret. comput. sci., 25, 3, 267-310, (1983) · Zbl 0512.68026
[6] Tarski, A., A lattice-theoretical fixpoint theorem and its applications, Pacific J. math., 5, 285-309, (1955) · Zbl 0064.26004
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.