Merge and termination in process algebra

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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.

Original languageEnglish
Title of host publicationFoundations of Software Technology and Theoretical Computer Science: Seventh Conference, Pune, India, December 17-19, 1987. Proceedings
EditorsK.V. Nori
PublisherSpringer
Pages153-172
Number of pages20
Volume287
ISBN (Electronic)978-3-540-48033-4
ISBN (Print)978-3-540-18625-0
DOIs
Publication statusPublished - 25 Nov 1987
EventThe 7th Foundations of Software Technology and Theoretical Computer Science Conference, 1987
- Pune, India
Duration: 17 Dec 198719 Dec 1987
Conference number: 7

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume287
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceThe 7th Foundations of Software Technology and Theoretical Computer Science Conference, 1987
Abbreviated titleFSTTCS 1987
Country/TerritoryIndia
CityPune
Period17/12/8719/12/87

Fingerprint

Dive into the research topics of 'Merge and termination in process algebra'. Together they form a unique fingerprint.

Cite this