Expressivity of quantitative modal logics: categorical foundations via codensity and approximation

Yuichi Kormorida, Shin-ya Katsumata, Clemens Kupke, Jurriaan Rot, Ichiro Hasup

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

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ö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.
Original languageEnglish
Title of host publication2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021
Place of PublicationPiscataway, NJ
PublisherIEEE
Number of pages14
ISBN (Electronic)9781665448956
ISBN (Print)9781665448963
DOIs
Publication statusPublished - 7 Jul 2021

Publication series

NameProceedings - Symposium on Logic in Computer Science
Volume2021-June
ISSN (Print)1043-6871

Keywords

  • modal logic
  • expressivity
  • codensity lifting

Cite this