一句话：提出基于余密度提升与近似族的范畴框架，统一推导定量模态逻辑的表达力结果。
论文关注定量模态逻辑能否完整刻画系统行为这一问题。随着概率、信息物理等系统兴起，已有若干针对定量逻辑与行为度量的表达力结果，但证明多依赖定制论证。作者首次提出范畴论框架，以“近似族”为核心，并借助 codensity lifting 统一构造双模拟度量等行为等价概念。该框架可容纳 König 等人与 Fijalkow 等人的近期结果，并导出关于“bisimulation uniformity”的新表达力定理，为设计新定量场景下的表达力模态逻辑提供通用方法。
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önig 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.
@inproceedings{paperbot6189,
title = {Expressivity of Quantitative Modal Logics : Categorical Foundations via Codensity and Approximation},
author = {Yuichi Komorida and Shin-ya Katsumata and Clemens Kupke and Jurriaan Rot and Ichiro Hasuo},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470656}
}