Further Formalization of the Process Algebra CCS in HOL4

TL;DR

This paper extends the formalization of the process algebra CCS in HOL4, incorporating weak bisimulation, observation congruence, and key lemmas with fully formal proofs, enhancing the theoretical foundation.

Contribution

It introduces comprehensive formal support for weak equivalences and proves significant lemmas without assumptions, advancing formal verification methods for CCS.

Findings

Formal definitions and theorems for weak bisimulation and observation congruence

Formal proofs of Deng Lemma, Hennessy Lemma, and coarsest congruence

Complete proof of the coarsest congruence theorem using ordinals

Abstract

In this project, we have extended previous work on the formalization of the process algebra CCS in HOL4. We have added full supports on weak bisimulation equivalence and observation congruence (rooted weak equivalence), with related definitions, theorems and algebraic laws. Some deep lemmas were also formally proved in this project, including Deng Lemma, Hennessy Lemma and several versions of the "Coarsest congruence contained in weak equivalence". For the last theorem, we have proved the full version (without any assumption) based on ordinals.