Tags:axiomatisation, bisimulation, congruence, guarded expression and soundness and completeness
Abstract:
In this paper we propose a new strategy for proving completeness of equational axiomatisations for finite-state behaviours, and present completeness proofs for equational axiomatisations of four bisimulation based tau-abstract behavioural congruences: branching congruence, delay congruence, eta-congruence, and observational congruence. Unlike the standard strategy for proving completeness of this kind by joining guarded equations, originally proposed by Milner, in this work we do it by constructing canonical expressions which can be used to bridge the gap between the two expressions of which the equality is to be established.
Canonical Expressions of Finite-State Behaviours and Completeness of Equational Axiomatisations