Skip to Main content Skip to Navigation
Journal articles

Unique solutions of contractions, CCS, and their HOL formalisation

Chun Tian 1 Davide Sangiorgi 2, 3
3 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : The unique solution of contractions is a proof technique for (weak) bisimilarity that overcomes certain syntactic limitations of Milner’s “unique solution of equations” theorem. This paper presents an overview of a comprehensive formalisation of Milner’s Calculus of Communicating Systems (CCS) in the HOL theorem prover (HOL4), with a focus towards the theory of unique solutions of equations and contractions. The formalisation consists of about 24,000 lines (1MB) of code in total. Some refinements of the “unique solution of contractions” theory itself are obtained. In particular we remove the constraints on summation, which must be guarded, by moving from contraction to rooted contraction. We prove the “unique solution of rooted contractions” theorem and show that rooted contraction is the coarsest precongruence contained in the contraction preorder.
Complete list of metadata
Contributor : Davide Sangiorgi Connect in order to contact the contributor
Submitted on : Monday, January 25, 2021 - 4:20:46 PM
Last modification on : Wednesday, November 3, 2021 - 4:00:04 AM
Long-term archiving on: : Monday, April 26, 2021 - 7:20:49 PM


Files produced by the author(s)




Chun Tian, Davide Sangiorgi. Unique solutions of contractions, CCS, and their HOL formalisation. Information and Computation, Elsevier, 2020, 275, pp.104606. ⟨10.1016/j.ic.2020.104606⟩. ⟨hal-03120563⟩



Les métriques sont temporairement indisponibles