Modular specification of process algebras

  • van Glabbeek R
  • Vaandrager F
  • 4

    Readers

    Mendeley users who have this article in their library.
  • 11

    Citations

    Citations of this article.

Abstract

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. © 1993.

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document

Authors

  • Rob van Glabbeek

  • Frits Vaandrager

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free