Bisimulation is not Finitely (First Order) Equationally
Axiomatisable
Abstract
This paper considers the existence of finite equational axiomatisations
of bisimulation over a calculus of finite state processes.
To express even simple properties such as \mu X E=\mu X E[E/X]
equationally it is necessary to use some notation for substitutions.
Accordingly the calculus is embedded in a simply typed lambda
calculus, allowing axioms such as the above to be written as equations
of higher type
rather than as equation schemes. Notions of higher order transition
system and bisimulation are then defined and using them the nonexistence
of finite axiomatisations containing at most first order variables is
shown.
The same technique is then applied to calculi of star expressions containing
a zero process --- in contrast to the positive result given in
[FZ93] for BPA*, which differs only in that it does not contain a zero.
Back to my home page.