Modal Logic and the Approximation Induction Principle

TL;DR

This paper establishes a compactness theorem for Hennessy-Milner logic and explores conditions under which the Approximation Induction Principle is sound in process algebra, linking modal logic with process equivalences.

Contribution

It introduces a compactness theorem for Hennessy-Milner logic and identifies necessary and sufficient conditions for the soundness of the Approximation Induction Principle.

Findings

A new compactness theorem for Hennessy-Milner logic.

A sufficient condition for the soundness of the Approximation Induction Principle.

The condition is shown to be necessary for compositional equivalences.

Abstract

We prove a compactness theorem in the context of Hennessy-Milner logic. It is used to derive a sufficient condition on modal characterizations for the Approximation Induction Principle to be sound modulo the corresponding process equivalence. We show that this condition is necessary when the equivalence in question is compositional with respect to the projection operators.