Adrien Durier ; Daniel Hirschkoff ; Davide Sangiorgi - Divergence and unique solution of equations

lmcs:4653 - Logical Methods in Computer Science, August 7, 2019, Volume 15, Issue 3 - https://doi.org/10.23638/LMCS-15(3:12)2019
Divergence and unique solution of equationsArticle

Authors: Adrien Durier ; Daniel Hirschkoff ; Davide Sangiorgi

    We study proof techniques for bisimilarity based on unique solution of equations. We draw inspiration from a result by Roscoe in the denotational setting of CSP and for failure semantics, essentially stating that an equation (or a system of equations) whose infinite unfolding never produces a divergence has the unique-solution property. We transport this result onto the operational setting of CCS and for bisimilarity. We then exploit the operational approach to: refine the theorem, distinguishing between different forms of divergence; derive an abstract formulation of the theorems, on generic LTSs; adapt the theorems to other equivalences such as trace equivalence, and to preorders such as trace inclusion. We compare the resulting techniques to enhancements of the bisimulation proof method (the `up-to techniques'). Finally, we study the theorems in name-passing calculi such as the asynchronous $\pi$-calculus, and use them to revisit the completeness part of the proof of full abstraction of Milner's encoding of the $\lambda$-calculus into the $\pi$-calculus for Lévy-Longo Trees.


    Volume: Volume 15, Issue 3
    Published on: August 7, 2019
    Accepted on: June 11, 2019
    Submitted on: July 2, 2018
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Community of mathematics and fundamental computer science in Lyon; Funder: French National Research Agency (ANR); Code: ANR-10-LABX-0070
    • Behavioural Application Program Interfaces; Funder: European Commission; Code: 778233
    • Coinduction for Verification and Certification; Funder: European Commission; Code: 678157
    • Reliable and Privacy-Aware Software Systems via Bisimulation Metrics; Funder: French National Research Agency (ANR); Code: ANR-16-CE25-0011

    1 Document citing this article

    Consultation statistics

    This page has been seen 1247 times.
    This article's PDF has been downloaded 610 times.