A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic

TL;DR

This paper introduces an intuitionistic modal logic, $ ext{OM}$, to characterize open bisimilarity in process calculi, providing a constructive algorithm for distinguishing formulae and mechanising the proof in Abella.

Contribution

It develops a new intuitionistic modal logic for open bisimilarity, with mechanised soundness and completeness proofs, and an implemented algorithm for generating distinguishing formulae.

Findings

The logic $ ext{OM}$ is sound for open bisimilarity.

A constructive completeness proof yields an algorithm for distinguishing formulae.

The approach can characterize a spectrum of bisimilarity congruences.

Abstract

Open bisimilarity is defined for open process terms in which free variables may appear. The insight is, in order to characterise open bisimilarity, we move to the setting of intuitionistic modal logics. The intuitionistic modal logic introduced, called $\mathcal{OM}$, is such that modalities are closed under substitutions, which induces a property known as intuitionistic hereditary. Intuitionistic hereditary reflects in logic the lazy instantiation of free variables performed when checking open bisimilarity. The soundness proof for open bisimilarity with respect to our intuitionistic modal logic is mechanised in Abella. The constructive content of the completeness proof provides an algorithm for generating distinguishing formulae, which we have implemented. We draw attention to the fact that there is a spectrum of bisimilarity congruences that can be characterised by intuitionistic modal logics.