• Media type: Text; Electronic Conference Proceeding; E-Article
  • Title: Canonical Solutions to Recursive Equations and Completeness of Equational Axiomatisations
  • Contributor: Liu, Xinxin [Author]; Yu, TingTing [Author]
  • imprint: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020
  • Language: English
  • DOI: https://doi.org/10.4230/LIPIcs.CONCUR.2020.35
  • Keywords: Axiomatisation ; Bisimulation ; Soundness and Completeness ; Congruence
  • Origination:
  • Footnote: Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
  • Description: 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.
  • Access State: Open Access