Nonaxiomatisability of equivalences over finite state processes Original Research Article

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 View the MathML source 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.