Modular Specification of Process Algebras

R.J. van Glabbeek, F.W. Vaandrager

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

This paper proposes a modular approach to the algebraic specification of process algebras. This is done by means of the notion of a module. The simplest modules are building blocks of operators and axioms, each block describing a feature of concurrency in a certain semantical setting. These modules can then be combined by means of a union operator +, an export operator □, allowing to forget some operators in a module, an operator H, changing semantics by taking homomorphic images, and an operator S which takes subalgebras. These operators enable us to combine modules in a subtle way, when the direct combination would be inconsistent.

We give a presentation of equational logic, infinitary conditional equational logic — of which we also prove the completeness — and first-order logic and show how the notion of a formal proof of a formula from a theory can be generalized to that of a proof of a formula from a module. This module logic is then applied in process algebra. We show how auxiliary process algebra operators can be hidden when this is needed. Moreover, we demonstrate how new process combinators can be defined in terms of more elementary ones in a clean way. As an illutration of our approach, we specify some FIFO-queues and verify several of their properties.

Original languageEnglish
Pages (from-to)293-348
Number of pages56
JournalTheoretical Computer Science
Volume113
Issue number2
DOIs
Publication statusPublished - 7 Jun 1993

Fingerprint

Dive into the research topics of 'Modular Specification of Process Algebras'. Together they form a unique fingerprint.

Cite this