Merge and termination in process algebra. (English) Zbl 0636.68024

Baeten, J. C. M.; van Glabbeek, R. J.

Foundations of software technology and theoretical computer science, Proc. 7th Conf., Pune/India 1987, Lect. Notes Comput. Sci. 287, 153-172 (1987).

[For the entire collection see Zbl 0625.00019.]
J. L. M. Vrancken [The algebra of communicating processes with empty process, report FVI 86-01, Dept. Comput. Sci., Univ. Amsterdam 1986], added the empty process \(\epsilon\) to the algebra of communicating processes of J. A. Bergstra and J. W. Klop [Inf. Control 60, 109-137 (1984; Zbl 0597.68027)]. Reconsidering the definition of the parallel composition operator merge, we found that it is preferable to explicitly state the termination option. This gives an extra summand in the defining equation of merge, using the auxiliary operator \(\sqrt{(tick)}\). We find that tick can be defined in terms of the encapsulation operator \(\partial_ H\). We give an operational and a denotational semantics for the resulting system ACP\(\sqrt{\quad}\), and prove that they are equal. We consider the limit rule, and prove that it holds in our models.

Reviewer: J.C.M.Baeten

MSC:

68N25	Theory of operating systems
68Q65	Abstract data types; algebraic specification
68Q55	Semantics in the theory of computing

Keywords:

concurrency; process algebra; empty process; termination; merge; tick