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.
Type de document :
Article dans une revue
ACM Transactions on Computational Logic, Association for Computing Machinery, 2017, 18 (1), pp.1-36. 〈10.1145/2971339〉
Liste complète des métadonnées

Littérature citée [41 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01647063
Contributeur : Sangiorgi Davide <>
Soumis le : dimanche 26 novembre 2017 - 12:18:04
Dernière modification le : mercredi 10 octobre 2018 - 10:10:35
Document(s) archivé(s) le : mardi 27 février 2018 - 12:13:31

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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〉

Partager

Métriques

Consultations de la notice

67

Téléchargements de fichiers

83