Expressivity of Quantitative Modal Logics: Categorical Foundations via Codensity and Approximation

TL;DR

This paper introduces a categorical framework using codensity lifting and approximating families to derive and unify quantitative expressivity results in modal logics for diverse systems.

Contribution

It presents the first categorical approach to quantitative expressivity, unifying existing results and deriving new ones through the notion of approximating families and codensity lifting.

Findings

Framework accommodates recent quantitative expressivity results

Derives a new result for bisimulation uniformity

Unifies diverse modal logic expressivity proofs

Abstract

A modal logic that is strong enough to fully characterize the behavior of a system is called expressive. Recently, with the growing diversity of systems to be reasoned about (probabilistic, cyber-physical, etc.), the focus shifted to quantitative settings which resulted in a number of expressivity results for quantitative logics and behavioral metrics. Each of these quantitative expressivity results uses a tailor-made argument; distilling the essence of these arguments is non-trivial, yet important to support the design of expressive modal logics for new quantitative settings. In this paper, we present the first categorical framework for deriving quantitative expressivity results, based on the new notion of approximating family. A key ingredient is the codensity lifting -- a uniform observation-centric construction of various bisimilarity-like notions such as bisimulation metrics. We show that several recent quantitative expressivity results (e.g. by K\"onig et al. and by Fijalkow et al.) are accommodated in our framework; a new expressivity result is derived, too, for what we call bisimulation uniformity.