Hostname: page-component-74656f9884-54qdv Total loading time: 0 Render date: 2026-11-10T17:14:54.026Z Has data issue: false hasContentIssue false

A ground-complete axiomatisation of finite-state processes in a generic process algebra

Published online by Cambridge University Press:  01 December 2008

JOS C. M. BAETEN
Affiliation:
Division of Computer Science, Technische Universiteit Eindhoven, The Netherlands Email: josb@win.tue.nl
MARIO BRAVETTI
Affiliation:
Department of Computer Science, Università di Bologna, Italy Email: bravetti@cs.unibo.it
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

The three classical process algebras CCS, CSP and ACP present several differences in their respective technical machinery. This is due, not only to the difference in their operators, but also to the terminology and ‘way of thinking’ of the community that has been (and still is) working with them. In this paper we will first discuss these differences and try to clarify the different usage of terminology and concepts. Then, as a result of this discussion, we define a generic process algebra where each of the basic mechanisms of the three process algebras (including minimal fixpoint based unguarded recursion) is expressed by an operator, and which can be used as an underlying common language. We show an example of the advantages of adopting such a language instead of one of the three more specialised algebras: producing a complete axiomatisation for Milner's observational congruence in the presence of (unguarded) recursion and static operators. More precisely, we provide a syntactical characterisation (allowing as many terms as possible) for the equations involved in recursion operators, which guarantees that transition systems generated by the operational semantics are finite state. Conversely, we show that every process admits a specification in terms of such a restricted form of recursion. We then present an axiomatisation that is ground complete over such a restricted signature. Notably, we also show that the two standard axioms of Milner for weakly unguarded recursion can be expressed using a single axiom only.

Information

Type
Paper
Copyright
Copyright © Cambridge University Press 2008