Abstract
intuitively, processes can be seen as objects which cannot do anything, but communicate (either internally or externally). Hence, they can be entirely specified, using only communication relations. Similarly, process equivalence relations, usually rely on communication relations exclusively. That is, the unique way for defining their equivalence, turns out to be the only means processes have in order to influence their environment. Therefore, it seems quite natural to insist that process equivalence relations be congruence relations. Moreover, such relations must characterize machine behaviours in such a way that they correspond to the intuitive meaning they usually have. Unfortunately this is not so general. In this paper we introduce an equivalence relation for processes. This equivalence is based exclusively on communication relations and on the notion of process interface. It is called safe implementation equivalence. It relates two processes if they both accept the same language and are equally deterministic. Actually this relation is generated by various preorders relying on relations which allow to evaluate formally the nondeterminism of processes. We apply it to various process languages. And, in each case, we show it to be a congruence, which we algebraically axiomatize.
Key-words
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
AUSTRY D., BOUDOL G. — Algèbre de processus et synchronisation TCS 30,1 —1984 —
ARNOLD A., NIVAT M. — Comportement de processus Colloque AFCET: les mathematiques de l'informatique — 1982 —
BERGSTRA J.A, KLOP J.W. —Algebra of communicating processes Report CS-R8421 Centrum voor Wiskunde en informatica —1984—
BROOKES S. D. — A model for communicating sequential processes Phd thesis Oxford' University —1983 —
DARONDEAU Ph. — An enlarged definition and complete axiomatization of observational congruence of finite processes LNCS 137 —1982—
DARONDEAU Ph., KOTT L. — On the observational semantics of fair asynchrony Proc ICALP 83, LNCS 154 —1983 —
GAMATIE B. —Systèmes de processus communicants et interprétation parallèle de languages fonctionnels IR no 320 INRIA —1984—
GAMATIE B. — Towards specification and proof af asynchronous systems IR no 466 INRIA —1985— & STACS 86: LNCS 210
GAMATIE B. — Safe implementation equivalence for asynchronous nondeterministic processes. IR. IRISA —1986—
HOARE C.A.R. —Communicating sequential processes CACM 21, vol 8—1978—
HOARE C.A.R., BROOKES S.D., ROSCOE A.W. — A theory of communicating processes — PRG-16 Oxford University —1981—
HENNESSY M., MILNER R. — Algebraic laws for nondeterminism and concurrency — JACM 32,1 —1985—
HENNESSY M., DE NICOLA R. — Testing equivalence for processes Proc ICALP 83, LNCS 154 —1983—
MILNER R. — A calculus of communicating systems LNCS 92 —1980—
PLOTKIN G. — A structural approach to operational semantics DAIMI FN —19 Comp. Sc. Dept. Aarhus University —1981—
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gamatie, B. (1986). Safe implementation equivalence for asynchronous nondeterministic processes. In: Gruska, J., Rovan, B., Wiedermann, J. (eds) Mathematical Foundations of Computer Science 1986. MFCS 1986. Lecture Notes in Computer Science, vol 233. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0016260
Download citation
DOI: https://doi.org/10.1007/BFb0016260
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16783-9
Online ISBN: 978-3-540-39909-4
eBook Packages: Springer Book Archive