Wild P, Schröder L (2021)
Publication Type: Conference contribution
Publication year: 2021
Pages Range: 551-571
Conference Proceedings Title: Foundations of Software Science and Computation Structures
ISBN: 9783030719944
DOI: 10.1007/978-3-030-71995-1_28
The classical van Benthem theorem characterizes modal logic as the bisimulation-invariant fragment of first-order logic; put differently, modal logic is as expressive as full first-order logic on bisimulation-invariant properties. This result has recently been extended to two flavours of quantitative modal logic, viz. fuzzy modal logic and probabilistic modal logic. In both cases, the quantitative van Benthem theorem states that every formula in the respective quantitative variant of first-order logic that is bisimulation-invariant, in the sense of being nonexpansive w.r.t. behavioural distance, can be approximated by quantitative modal formulae of bounded rank. In the present paper, we unify and generalize these results in three directions: We lift them to full coalgebraic generality, thus covering a wide range of system types including, besides fuzzy and probabilistic transition systems as in the existing examples, e.g. also metric transition systems; and we generalize from real-valued to quantale-valued behavioural distances, e.g. nondeterministic behavioural distances on metric transition systems; and we remove the symmetry assumption on behavioural distances, thus covering also quantitative notions of simulation.
APA:
Wild, P., & Schröder, L. (2021). A Quantified Coalgebraic van Benthem Theorem. In Stefan Kiefer; Christine Tasson (Eds.), Foundations of Software Science and Computation Structures (pp. 551-571).
MLA:
Wild, Paul, and Lutz Schröder. "A Quantified Coalgebraic van Benthem Theorem." Proceedings of the 24th International Conference, FOSSACS 2021 Ed. Stefan Kiefer; Christine Tasson, 2021. 551-571.
BibTeX: Download