摘要：In this paper we prove completeness of four axiomatisations for finite-state behaviours with respect to behavioural equivalences at various Ï"-abstract levels: branching congruence, delay congruence, η-congruence, and weak congruence. Instead of merging guarded recursive equations, which was the approach originally used by Robin Milner and has since become the standard strategy for proving completeness results of this kind, in this work we take a new approach by solving guarded recursive equations with canonical solutions which are those with the fewest reachable states. The new strategy allows uniform treatment of the axiomatisations with respect to different behavioural equivalences.
关键词：Bisimulation; Congruence; Axiomatisation; Soundness and Completeness
