License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2020.35
URN: urn:nbn:de:0030-drops-128479
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12847/
Go to the corresponding LIPIcs Volume Portal

Liu, Xinxin ; Yu, TingTing

Canonical Solutions to Recursive Equations and Completeness of Equational Axiomatisations

pdf-format:
LIPIcs-CONCUR-2020-35.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{liu_et_al:LIPIcs:2020:12847,
  author =	{Xinxin Liu and TingTing Yu},
  title =	{{Canonical Solutions to Recursive Equations and Completeness of Equational Axiomatisations}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{35:1--35:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Igor Konnov and Laura Kov{\'a}cs},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12847},
  URN =		{urn:nbn:de:0030-drops-128479},
  doi =		{10.4230/LIPIcs.CONCUR.2020.35},
  annote =	{Keywords: Bisimulation, Congruence, Axiomatisation, Soundness and Completeness}
}

Keywords: Bisimulation, Congruence, Axiomatisation, Soundness and Completeness
Collection: 31st International Conference on Concurrency Theory (CONCUR 2020)
Issue Date: 2020
Date of publication: 26.08.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI