Abstract
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.
Preview
Unable to display preview. Download preview PDF.
References
Milner R. (1978). Synthesis of Communicating Behaviour. Proc. 7th MFCS Conference. Zakopane Poland. Springer-Verlag LNCS Vol. 64,pp. 61–83.
Hennessy M. & Milner R. (1980). On observing nondeterminism and concurrency. ICALP'80. Noordwijkerhout. Springer-Verlag LNCS Vol. 74.
Hennessy M. & Plotkin G. (1980). A term model for CCS. Proc. 9th MFCS Conference. Rydzyna Poland. Springer-Verlag LNCS Vol. 88, pp. 261–274.
Milner R. (1980). A calculus of Communicating Systems. Springer-Verlag LNCS Vol. 92, (170 pp.)
Milner R. (1980). On relating synchrony and asynchrony. University of Edinburgh Report CSR 75–80, (December 1980).
Hoare C.A.R., Brookes S.D., Roscoe A.W. (1981). A theory of Communicating Sequential Processes. Programming Research Group — Oxford OX2 CPE.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1982 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Darondeau, P. (1982). An enlarged definition and complete axiomatization of observational congruence of finite processes. In: Dezani-Ciancaglini, M., Montanari, U. (eds) International Symposium on Programming. Programming 1982. Lecture Notes in Computer Science, vol 137. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-11494-7_5
Download citation
DOI: https://doi.org/10.1007/3-540-11494-7_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-11494-9
Online ISBN: 978-3-540-39184-5
eBook Packages: Springer Book Archive