Divergence and unique solution of equations
| Autor: | Durier, Adrien, Hirschkoff, Daniel, Sangiorgi, Davide |
|---|---|
| Rok vydání: | 2018 |
| Předmět: | |
| Zdroj: | Logical Methods in Computer Science, Volume 15, Issue 3 (August 7, 2019) lmcs:4653 |
| Druh dokumentu: | Working Paper |
| DOI: | 10.23638/LMCS-15(3:12)2019 |
| Popis: | 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\'evy-Longo Trees. Comment: This is an extended version of the paper with the same title published in the proceedings of CONCUR'17 |
| Databáze: | arXiv |
| Externí odkaz: |
|