LIPIcs.CONCUR.2020.35.pdf
- Filesize: 0.49 MB
- 17 pages
Document
Canonical Solutions to Recursive Equations and Completeness of Equational Axiomatisations
Authors
-
Part of:
Volume:
31st International Conference on Concurrency Theory (CONCUR 2020)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Concurrency Theory (CONCUR) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2020-08-26
File
Document Identifiers
Acknowledgements
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)
https://doi.org/10.4230/LIPIcs.CONCUR.2020.35
https://doi.org/10.4230/LIPIcs.CONCUR.2020.35
Abstract
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
Keywords
- Bisimulation
- Congruence
- Axiomatisation
- Soundness and Completeness
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- 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: https://doi.org/10.1006/inco.1996.0047.
-
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.
- M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the Association for Computing Machinery, 32(1):137-161, 1985. URL: https://doi.org/10.1145/2455.2460.
- M. Lohrey, P.R. D'Argenio, and H. Hermanns. Axiomatising divergence. Information and computation, 203:115-144, 2005. URL: https://doi.org/10.1016/j.ic.2005.05.007.
- R. Milner. A complete inference system for a class of regular behaviours. Journal of computer and system sciences, 28:439-466, 1984. URL: https://doi.org/10.1016/0022-0000(84)90023-0.
-
R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
- R. Milner. A complete axiomatisation system for observational congruence of finite-state behaviours. information and computation, 81:227-247, 1989. URL: https://doi.org/10.1016/0890-5401(89)90070-9.
- 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: https://doi.org/10.1007/3-540-57182-5_39.
- 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: https://doi.org/10.1145/233551.233556.
- D. Walker. Bisimulation and divergence. Information and computation, 85:220-241, 1990. URL: https://doi.org/10.1016/0890-5401(90)90048-M.