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.

翻译：一种足以充分描述系统行为特征的模型逻辑被称为“表达式”。最近,随着各种系统日益多样化,需要说明(概率、网络物理等),重点转向了定量环境,导致定量逻辑和行为计量的多项表达性结果。每种定量表达性结果都使用定制的论据;这些论点的精髓是非三重性的,但对于支持为新的定量设置设计表达式模式逻辑十分重要。在本文中,我们根据近似家庭的新概念,提出了第一个得出定量表达性结果的绝对框架。一个关键要素是代码性提升 -- -- 一种以观察为中心的不同不同概念的统一结构,如刺激性指标。我们表明,我们的框架中包含了最近的若干定量表达性结果(例如K\ " onig等人 " 和Fijalkow等人 " ),而Fijalkow等人也提出了新的表达性结果,我们称之为“双向统一性”。