An enlarged definition and complete axiomatization of observational congruence of finite processes

  • Ph. Darondeau
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 137)


The paper is addressed to determine an adequate notion of observational equivalence of finite processes, and to give a complete axiomatization of the associated congruence. We begin with establishing the fact that recursive equivalence of processes as it has been defined in the work of Milner and his colleagues is not a fully observational equivalence, in that it is much more restrictive than it should be to agree in all cases with the judgement of an effective observer. Inspiring from CCS, an alternative syntax is proposed for processes, bringing forward n-ary guarding operators. Given p and q in that syntax, which allows invisible actions to be expressed, p and q are said equivalent iff after any common experiment, they both react by identical answers or absence of answer to any ambiguous communication offer that the observer may present. It is shown that this equivalence is also a congruence ; a finite set of equational axioms is given for the congruence, which we prove to be a complete proof system by argumenting over canonical forms of programs. In a second time, our language is enriched by adding it the necessary operators for expressing the parallel composition of processes and the renaming of their actions. The definition of the observational equivalence is extended accordingly, and it is shown that we still obtain a congruence, for which a complete proof system is finally given.


Proof System Axiomatic System Parallel Composition Denotational Semantic Identical Answer 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. (1).
    Milner R. (1978). Synthesis of Communicating Behaviour. Proc. 7th MFCS Conference. Zakopane Poland. Springer-Verlag LNCS Vol. 64,pp. 61–83.Google Scholar
  2. (2).
    Hennessy M. & Milner R. (1980). On observing nondeterminism and concurrency. ICALP'80. Noordwijkerhout. Springer-Verlag LNCS Vol. 74.Google Scholar
  3. (3).
    Hennessy M. & Plotkin G. (1980). A term model for CCS. Proc. 9th MFCS Conference. Rydzyna Poland. Springer-Verlag LNCS Vol. 88, pp. 261–274.Google Scholar
  4. (4).
    Milner R. (1980). A calculus of Communicating Systems. Springer-Verlag LNCS Vol. 92, (170 pp.)Google Scholar
  5. (5).
    Milner R. (1980). On relating synchrony and asynchrony. University of Edinburgh Report CSR 75–80, (December 1980).Google Scholar
  6. (6).
    Hoare C.A.R., Brookes S.D., Roscoe A.W. (1981). A theory of Communicating Sequential Processes. Programming Research Group — Oxford OX2 CPE.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1982

Authors and Affiliations

  • Ph. Darondeau
    • 1
  1. 1.IRISARennes CedexFrance

Personalised recommendations