Skip to Main content Skip to Navigation
Journal articles

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.
Complete list of metadata

Cited literature [41 references]  Display  Hide  Download
Contributor : Davide Sangiorgi Connect in order to contact the contributor
Submitted on : Sunday, November 26, 2017 - 12:18:04 PM
Last modification on : Friday, July 8, 2022 - 10:06:43 AM
Long-term archiving on: : Tuesday, February 27, 2018 - 12:13:31 PM


Files produced by the author(s)




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⟩



Record views


Files downloads