Nonaxiomatisability of
equivalences over finite state processes
Abstract
This paper considers the existence of finite equational
axiomatisations of behavioural equivalences over a calculus of finite
state processes. To express even simple properties such as \mu x E
= \mu x E[E/x] some notation for substitutions is required.
Accordingly the calculus is embedded in a simply typed lambda
calculus, allowing such schemas to be expressed as equations between
terms containing first order variables. A notion of first order trace congruence
over such terms is introduced and used to show that no finite set of
such equations is sound and complete for any reasonable equivalence
finer than trace equivalence. The intermediate results are then
applied to give two nonaxiomatisability results over calculi of
regular expressions.
Back to my home page.