## The Algebra of Finite State Processes

**Peter Michael Sewell**
*Abstract:* This thesis is concerned with the algebraic
theory of finite state processes. The processes we focus on are
those given by a signature with prefix, summation and recursion,
considered modulo strong bisimulation. We investigate their
equational and implicational theories.

We first consider the existence of finite equational
axiomatisations. In order to express an interesting class of
equational axioms we embed the processes into a simply typed lambda
calculus, allowing equation schemes with metasubstitutions to be
expressed by pure equations. Two equivalences over the lambda terms
are defined, an extensional equality and a higher order
bisimulation. Under a restriction to first order variables these
are shown to coincide and an examination of the coincidence shows
that no finite equational axiomatisation of strong bisimulation can
exist. We then encode the processes of Basic Process Algebra with
iteration and zero (BPA_{delta}^{*}) into
this lambda calculus and show that it too is not finitely
equationally axiomatisable, in sharp contrast to the extant
positive result for the fragment without zero.

For the implicational theory, we show the existence of finite
computable complete sets of unifiers for finite sets of equations
between processes (with zero order variables). It follows that the
soundness of sequents over these is decidable.

Some applications to the theories of higher order process
calculi and non-well-founded sets are made explicit.

**ECS-LFCS-95-328**, October 1995.

This report is available in the following formats:

Previous |

Index |

Next