### The Algebra of Finite State Processes

#### 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.

Back to my home page.