Abstract
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.
Work of both authors forms part of the DFG project Probabilistic description logics as a fragment of probabilistic first-order logic (SCHR 1118/6-2)
Chapter PDF
Similar content being viewed by others
References
Abriola, S., Descotte, M., Figueira, S.: Model theory of XPath on data trees. Part II: Binary bisimulation and definability. Inf. Comput. (2017), in press
Adámek, J., Herrlich, H., Strecker, G.: Abstract and Concrete Categories. Wiley Interscience (1990), available as Reprints Theory Appl. Cat. 17 (2006), pp. 1-507
de Alfaro, L., Faella, M., Stoelinga, M.: Linear and branching system metrics. IEEE Trans. Software Eng. 35(2), 258–273 (2009)
Baldan, P., Bonchi, F., Kerstan, H., König, B.: Coalgebraic behavioral metrics. Log. Methods Comput. Sci. 14(3) (2018)
Barr, M.: Terminal coalgebras in well-founded set theory. Theoret. Comput. Sci. 114, 299–315 (1993)
van Benthem, J.: Correspondence theory. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 3, pp. 325–408. Springer (2001)
Bilkova, M., Kurz, A., Petrisan, D., Velebil, J.: Relation lifting, with an application to the many-valued cover modality. Logical Methods in Computer Science Volume 9, Issue 4 (Oct 2013)
Borceux, F.: Handbook of Categorical Algebra: Volume 3, Sheaf Theory. Cambridge University Press (1994)
van Breugel, F.: A behavioural pseudometric for metric labelled transition systems. In: Abadi, M., de Alfaro, L. (eds.) Concurrency Theory, CONCUR 2005. LNCS, vol. 3653, pp. 141–155. Springer (2005)
van Breugel, F., Worrell, J.: A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci. 331, 115–142 (2005)
Carreiro, F.: PDL is the bisimulation-invariant fragment of weak chain logic. In: Logic in Computer Science, LICS 2015. pp. 341–352. IEEE (2015)
ten Cate, B., Fontaine, G., Litak, T.: Some modal aspects of XPath. J. Appl. Non-Classical Log. 20, 139–171 (2010)
Chatzikokolakis, K., Gebler, D., Palamidessi, C., Xu, L.: Generalized bisimulation metrics. In: Concurrency Theory, CONCUR 2014. LNCS, vol. 8704, pp. 32–46. Springer (2014)
Dawar, A., Otto, M.: Modal characterisation theorems over special classes of frames. In: Logic in Computer Science, LICS 05. pp. 21–30. IEEE Computer Society (2005)
Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theor. Comput. Sci. 318, 323–354 (2004)
Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled markov processes. Inf. Comput. 179(2), 163–193 (2002)
Doberkat, E.: Stochastic Coalgebraic Logic. Monographs in Theoretical Computer Science. An EATCS Series, Springer (2009)
Eleftheriou, P., Koutras, C., Nomikos, C.: Notions of bisimulation for Heyting-valued modal languages. J. Logic Comput. 22(2), 213–235 (2012)
Enqvist, S., Seifan, F., Venema, Y.: Monadic second-order logic and bisimulation invariance for coalgebras. In: Logic in Computer Science, LICS 2015. IEEE (2015)
Fahrenberg, U., Legay, A., Thrane, C.: The quantitative linear-time–branching-time spectrum. In: Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2011. LIPIcs, vol. 13, pp. 103–114. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Fan, T.: Fuzzy bisimulation for Gödel modal logic. IEEE Trans. Fuzzy Sys. 23, 2387–2396 (Dec 2015)
Figueira, D., Figueira, S., Areces, C.: Model theory of XPath on data trees. Part I: Bisimulation and characterization. J. Artif. Intell. Res. (JAIR) 53, 271–314 (2015)
Flagg, B., Kopperman, R.: Continuity spaces: Reconciling domains and metric spaces. Theoretical Computer Science 177(1), 111 – 138 (1997)
Flagg, R.: Quantales and continuity spaces. Algebra Univ. 37(3), 257–276 (1997)
Gavazzo, F.: Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances. In: Logic in Computer Science, LICS 2018. pp. 452–461. ACM (2018)
Giacalone, A., Jou, C., Smolka, S.: Algebraic reasoning for probabilistic concurrent systems. In: Programming concepts and methods, PCM 1990. pp. 443–458. North-Holland (1990)
Halpern, J.Y.: An analysis of first-order logics of probability. Artif. Intell 46, 311–350 (1990)
Hansen, H., Kupke, C., Pacuit, E.: Neighbourhood structures: Bisimilarity and basic model theory. Log. Meth. Comput. Sci. 5(2) (2009)
Hennessy, M., Milner, R.: Algebraic laws for non-determinism and concurrency. J. ACM 32, 137–161 (1985)
Henriksen, M., Kopperman, R.: A general theory of structure spaces with applications to spaces of prime ideals. Alg. Univ. 28(3), 349–376 (1991)
Hofmann, D.: Topological theories and closed objects. Adv. Math. 215(2), 789 – 824 (2007)
Hofmann, D., Reis, C.: Probabilistic metric spaces as enriched categories. Fuzzy Sets Sys. 210, 1–21 (2013)
Hofmann, D., Waszkiewicz, P.: Approximation in quantale-enriched categories. Topol. Appl. 158(8), 963–977 (2011)
Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: Logic in Computer Science, LICS 1997. pp. 111–122. IEEE (1997)
Janin, D., Walukiewicz, I.: Automata for the modal \(\mu \)-calculus and related results. In: Mathematical Foundations of Computer Science, MFCS 1995. LNCS, vol. 969, pp. 552–562. Springer (1995)
Khakpour, N., Mousavi, M.R.: Notions of conformance testing for cyber-physical systems: Overview and roadmap (invited paper). In: Concurrency Theory, CONCUR 2015. LIPIcs, vol. 42, pp. 18–40. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
König, B., Mika-Michalski, C.: (Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras. In: Schewe, S., Zhang, L. (eds.) Concurrency Theory, CONCUR 2018. LIPIcs, vol. 118, pp. 37:1–37:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Kontinen, J., Müller, J., Schnoor, H., Vollmer, H.: A van Benthem theorem for modal team semantics. In: Computer Science Logic, CSL 2015. LIPIcs, vol. 41, pp. 277–291. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)
Larsen, K., Skou, A.: Bisimulation through probabilistic testing. Inform. Comput. 94, 1–28 (1991)
Litak, T., Pattinson, D., Sano, K., Schröder, L.: Coalgebraic predicate logic. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) Automata, Languages, and Programming, ICALP 2012. LNCS, vol. 7392, pp. 299–311. Springer (2012)
Lukasiewicz, T., Straccia, U.: Managing uncertainty and vagueness in description logics for the semantic web. J. Web Sem. 6(4), 291–308 (2008)
Morgan, C., McIver, A.: A probabilistic temporal calculus based on expectations. In: Groves, L., Reeves, S. (eds.) Formal Methods Pacific, FMP 1997. Springer (1997)
Novák, V.: First-order fuzzy logic. Stud. Log. 46, 87–109 (1987)
Otto, M.: Elementary proof of the van Benthem-Rosen characterisation theorem. Tech. Rep. 2342, Department of Mathematics, Technische Universität Darmstadt (2004)
Pattinson, D.: Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Log. 45, 19–33 (2004)
Raney, G.: Completely distributive complete lattices. Proc. AMS 3(5), 677–680 (1952)
Raney, G.: A subdirect-union representation for completely distributive complete lattices. Proc. AMS 4(4), 518–522 (1953)
Rosen, E.: Modal logic over finite structures. J. Logic, Language and Information 6(4), 427–439 (1997)
Rutten, J.: Universal coalgebra: A theory of systems. Theoret. Comput. Sci. 249, 3–80 (2000)
Schröder, L.: Expressivity of coalgebraic modal logic: The limits and beyond. Theoret. Comput. Sci. 390, 230–247 (2008)
Schröder, L., Pattinson, D.: Description logics and fuzzy probability. In: Walsh, T. (ed.) Int. Joint Conf. Artificial Intelligence, IJCAI 2011. pp. 1075–1081. AAAI (2011)
Schröder, L., Pattinson, D., Litak, T.: A van Benthem/Rosen theorem for coalgebraic predicate logic. J. Log. Comput. 27(3), 749–773 (2017)
Straccia, U.: A fuzzy description logic. In: Artificial Intelligence, AAAI 1998. pp. 594–599. AAAI Press / MIT Press (1998)
Sturm, H., Wolter, F.: First-order expressivity for S5-models: Modal vs. two-sorted languages. J. Philos. Logic 30, 571–591 (2001)
Wild, P., Schröder, L.: A characterization theorem for a modal description logic. In: Int. Joint Conf. Artificial Intelligence, IJCAI 2017. pp. 1304–1310. ijcai.org (2017)
Wild, P., Schröder, L.: Characteristic logics for behavioural metrics via fuzzy lax extensions. In: Concurrency Theory, CONCUR 2020. LIPIcs, vol. 171, pp. 27:1–27:23. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Wild, P., Schröder, L., Pattinson, D., König, B.: A van Benthem theorem for fuzzy modal logic. In: Logic in Computer Science, LICS 2018. pp. 909–918. ACM (2018)
Wild, P., Schröder, L., Pattinson, D., König, B.: A modal characterization theorem for a probabilistic fuzzy description logic. In: Kraus, S. (ed.) International Joint Conference on Artificial Intelligence, IJCAI 2019. pp. 1900–1906. ijcai.org (2019)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Wild, P., Schröder, L. (2021). A Quantified Coalgebraic van Benthem Theorem. In: Kiefer, S., Tasson, C. (eds) Foundations of Software Science and Computation Structures. FOSSACS 2021. Lecture Notes in Computer Science(), vol 12650. Springer, Cham. https://doi.org/10.1007/978-3-030-71995-1_28
Download citation
DOI: https://doi.org/10.1007/978-3-030-71995-1_28
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-71994-4
Online ISBN: 978-3-030-71995-1
eBook Packages: Computer ScienceComputer Science (R0)