In VRANCKEN [14], the empty process ɛ was added to the Algebra of Communicating Processes of BERGSTRA & KLOP [3, 4]. 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 √ (tick). We find that tick can be defined in terms of the encapsulation operator ∂H. We give an operational and a denotational semantics for the resulting system ACP√, and prove that they are equal. We consider the Limit Rule, and prove it holds in our models.
CITATION STYLE
Baeten, J. C. M., & van Glabbeek, R. J. (1987). Merge and termination in process algebra. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 287 LNCS, pp. 153–172). Springer Verlag. https://doi.org/10.1007/3-540-18625-5_49
Mendeley helps you to discover research relevant for your work.