Expressive Logics for Coinductive Predicates

TL;DR

This paper generalizes the classical Hennessy-Milner theorem to coalgebras, establishing conditions under which modal logics fully characterize coinductive predicates like similarity and divergence.

Contribution

It introduces a framework for understanding when modal logics can fully characterize coinductive predicates on coalgebras, extending classical results to a broader setting.

Findings

Provided sufficient conditions for logic adequacy and expressivity on coalgebras

Illustrated the approach with logics for similarity, divergence, and behavioral metrics

Extended classical bisimilarity results to coinductive predicates in a coalgebraic context

Abstract

The classical Hennessy-Milner theorem says that two states of an image-finite transition system are bisimilar if and only if they satisfy the same formulas in a certain modal logic. In this paper we study this type of result in a general context, moving from transition systems to coalgebras and from bisimilarity to coinductive predicates. We formulate when a logic fully characterises a coinductive predicate on coalgebras, by providing suitable notions of adequacy and expressivity, and give sufficient conditions on the semantics. The approach is illustrated with logics characterising similarity, divergence and a behavioural metric on automata.