Equations, Contractions, and Unique Solutions

Davide Sangiorgi 1, 2
1 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : One of the most studied behavioural equivalences is bisimilarity. Its success is much due to the associated bisimulation proof method, which can be further enhanced by means of 'bisimulation up-to' techniques such as 'up-to context'. A different proof method is discussed, based on unique solution of special forms of inequations called contractions, and inspired by Milner's theorem on unique solution of equations. The method is as powerful as the bisimulation proof method and its 'up-to context' enhancements. The definition of contraction can be transferred onto other behavioural equivalences , possibly contextual and non-coinductive. This enables a coinduc-tive reasoning style on such equivalences, either by applying the method based on unique solution of contractions, or by injecting appropriate contraction preorders into the bisimulation game. The techniques are illustrated on CCS-like languages; an example dealing with higher-order languages is also shown.
Liste complète des métadonnées

Cited literature [41 references]  Display  Hide  Download

https://hal.inria.fr/hal-01647063
Contributor : Sangiorgi Davide <>
Submitted on : Sunday, November 26, 2017 - 12:18:04 PM
Last modification on : Thursday, February 7, 2019 - 5:00:36 PM
Document(s) archivé(s) le : Tuesday, February 27, 2018 - 12:13:31 PM

File

main.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Davide Sangiorgi. Equations, Contractions, and Unique Solutions. ACM Transactions on Computational Logic, Association for Computing Machinery, 2017, 18 (1), pp.1-36. ⟨10.1145/2971339⟩. ⟨hal-01647063⟩

Share

Metrics

Record views

84

Files downloads

150