Canonical Solutions to Recursive Equations and Completeness of Equational Axiomatisations

Authors Xinxin Liu, TingTing Yu

Thumbnail PDF


  • Filesize: 0.49 MB
  • 17 pages

Document Identifiers

Author Details

Xinxin Liu
  • State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, China
  • University of Chinese Academy of Sciences, China
TingTing Yu
  • Beijing Sunwise Information Technology Ltd, China
  • Beijing Institute of Control Engneering, China


We thank the reviewers' suggestions which greatly improved the presentation.

Cite AsGet BibTex

Xinxin Liu and TingTing Yu. Canonical Solutions to Recursive Equations and Completeness of Equational Axiomatisations. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 35:1-35:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Process calculi
  • Bisimulation
  • Congruence
  • Axiomatisation
  • Soundness and Completeness


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. L. Aceto, R. van Glabbeek, W. Fokkink, and A. Ingĺfsdóttir. Axiomatizing prefix itteration with silent steps. Information and computation, 127(1):26-40, 1996. URL:
  2. Y. Deng. A simple completeness proof for the axiomatisations of weak behavioural equivalences. Bulletin of the European Association for Theoretical Computer Science, 172:359-397, 2007. Google Scholar
  3. M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the Association for Computing Machinery, 32(1):137-161, 1985. URL:
  4. M. Lohrey, P.R. D'Argenio, and H. Hermanns. Axiomatising divergence. Information and computation, 203:115-144, 2005. URL:
  5. R. Milner. A complete inference system for a class of regular behaviours. Journal of computer and system sciences, 28:439-466, 1984. URL:
  6. R. Milner. Communication and Concurrency. Prentice-Hall, 1989. Google Scholar
  7. R. Milner. A complete axiomatisation system for observational congruence of finite-state behaviours. information and computation, 81:227-247, 1989. URL:
  8. R. J. van Glabbeek. A complete axiomatisation for branching bisimulation congruence of finite-state behaviours. In A.M Borzyszkowski & S. Sokolowski, editors: Proceedings 18th International Symposium on Mathematical Foundations of Computer Science, MFCS'93, Gdansk, Opland, August/September 1993, LNCS 711, Springer, pages 473-484, 1993. URL:
  9. R. J. van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics. Journal of the Association for Computing Machinery, 43(3):555-600, 1996. URL:
  10. D. Walker. Bisimulation and divergence. Information and computation, 85:220-241, 1990. URL: