2026-07-26T03:31:44Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:12847 2024-03-06T10:50:50Z ddc:004 open_access

Canonical Solutions to Recursive Equations and Completeness of Equational Axiomatisations Liu, Xinxin Yu, TingTing Bisimulation Congruence Axiomatisation Soundness and Completeness 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Xinxin Liu and TingTing Yu 2020 Is Part Of LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2020.35 urn:nbn:de:0030-drops-128479 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.35 eng https://creativecommons.org/licenses/by/3.0/legalcode