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

Tools

Kormorida, Yuichi and Katsumata, Shin-ya and Kupke, Clemens and Rot, Jurriaan and Hasup, Ichiro; (2021) Expressivity of quantitative modal logics : categorical foundations via codensity and approximation. In: 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021. Proceedings - Symposium on Logic in Computer Science . IEEE, Piscataway, NJ. ISBN 9781665448956 (https://doi.org/10.1109/LICS52264.2021.9470656)

[thumbnail of Kormorida-etal-LICS2021-Expressivity-of-quantitative-modal-logics]
Preview
 Text. Filename: Kormorida_etal_LICS2021_Expressivity_of_quantitative_modal_logics.pdf
Accepted Author Manuscript
Download (1MB)| Preview

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.

  • Item type:Book Section
    ID code:77498
    Dates:
    Date
    Event
    7 July 2021
    Published
    2 July 2021
    Published Online
    31 March 2021
    Accepted
    Notes:© 2021 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
    Subjects:Science > Mathematics > Electronic computers. Computer science
    Department:Faculty of Science > Computer and Information Sciences
    Depositing user: Pure Administrator
    Date deposited:19 Aug 2021 15:01
    Last modified:11 Nov 2024 15:25
    Related URLs:
    URI:https://strathprints.strath.ac.uk/id/eprint/77498
CORE (COnnecting REpositories)