{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:43:03Z","timestamp":1762324983840,"version":"3.40.3"},"publisher-location":"Cham","reference-count":58,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030719944"},{"type":"electronic","value":"9783030719951"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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.<\/jats:p>","DOI":"10.1007\/978-3-030-71995-1_28","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T17:03:39Z","timestamp":1616432619000},"page":"551-571","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["A Quantified Coalgebraic van Benthem Theorem"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9796-9675","authenticated-orcid":false,"given":"Paul","family":"Wild","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3146-5906","authenticated-orcid":false,"given":"Lutz","family":"Schr\u00f6der","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"28_CR1","doi-asserted-by":"crossref","unstructured":"Abriola, S., Descotte, M., Figueira, S.: Model theory of XPath on data trees. Part II: Binary bisimulation and definability. Inf. Comput. (2017), in press","DOI":"10.1016\/j.ic.2017.01.002"},{"key":"28_CR2","unstructured":"Ad\u00e1mek, J., Herrlich, H., Strecker, G.: Abstract and Concrete Categories. Wiley Interscience (1990), available as Reprints Theory Appl. Cat. 17 (2006), pp. 1-507"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"de\u00a0Alfaro, L., Faella, M., Stoelinga, M.: Linear and branching system metrics. IEEE Trans. Software Eng. 35(2), 258\u2013273 (2009)","DOI":"10.1109\/TSE.2008.106"},{"key":"28_CR4","unstructured":"Baldan, P., Bonchi, F., Kerstan, H., K\u00f6nig, B.: Coalgebraic behavioral metrics. Log. Methods Comput. Sci. 14(3) (2018)"},{"key":"28_CR5","unstructured":"Barr, M.: Terminal coalgebras in well-founded set theory. Theoret. Comput. Sci. 114, 299\u2013315 (1993)"},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"van Benthem, J.: Correspondence theory. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol.\u00a03, pp. 325\u2013408. Springer (2001)","DOI":"10.1007\/978-94-017-0454-0_4"},{"key":"28_CR7","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.2168\/LMCS-9(4:8)2013"},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"Borceux, F.: Handbook of Categorical Algebra: Volume 3, Sheaf Theory. Cambridge University Press (1994)","DOI":"10.1017\/CBO9780511525872"},{"key":"28_CR9","doi-asserted-by":"crossref","unstructured":"van Breugel, F.: A behavioural pseudometric for metric labelled transition systems. In: Abadi, M., de\u00a0Alfaro, L. (eds.) Concurrency Theory, CONCUR 2005. LNCS, vol.\u00a03653, pp. 141\u2013155. Springer (2005)","DOI":"10.1007\/11539452_14"},{"key":"28_CR10","unstructured":"van Breugel, F., Worrell, J.: A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci. 331, 115\u2013142 (2005)"},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"Carreiro, F.: PDL is the bisimulation-invariant fragment of weak chain logic. In: Logic in Computer Science, LICS 2015. pp. 341\u2013352. IEEE (2015)","DOI":"10.1109\/LICS.2015.40"},{"key":"28_CR12","doi-asserted-by":"crossref","unstructured":"ten Cate, B., Fontaine, G., Litak, T.: Some modal aspects of XPath. J. Appl. Non-Classical Log. 20, 139\u2013171 (2010)","DOI":"10.3166\/jancl.20.139-171"},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"Chatzikokolakis, K., Gebler, D., Palamidessi, C., Xu, L.: Generalized bisimulation metrics. In: Concurrency Theory, CONCUR 2014. LNCS, vol.\u00a08704, pp. 32\u201346. Springer (2014)","DOI":"10.1007\/978-3-662-44584-6_4"},{"key":"28_CR14","unstructured":"Dawar, A., Otto, M.: Modal characterisation theorems over special classes of frames. In: Logic in Computer Science, LICS 05. pp. 21\u201330. IEEE Computer Society (2005)"},{"key":"28_CR15","unstructured":"Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theor. Comput. Sci. 318, 323\u2013354 (2004)"},{"key":"28_CR16","unstructured":"Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled markov processes. Inf. Comput. 179(2), 163\u2013193 (2002)"},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"Doberkat, E.: Stochastic Coalgebraic Logic. Monographs in Theoretical Computer Science. An EATCS Series, Springer (2009)","DOI":"10.1007\/978-3-642-02995-0"},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"Eleftheriou, P., Koutras, C., Nomikos, C.: Notions of bisimulation for Heyting-valued modal languages. J. Logic Comput. 22(2), 213\u2013235 (2012)","DOI":"10.1093\/logcom\/exq005"},{"key":"28_CR19","doi-asserted-by":"crossref","unstructured":"Enqvist, S., Seifan, F., Venema, Y.: Monadic second-order logic and bisimulation invariance for coalgebras. In: Logic in Computer Science, LICS 2015. IEEE (2015)","DOI":"10.1109\/LICS.2015.41"},{"key":"28_CR20","unstructured":"Fahrenberg, U., Legay, A., Thrane, C.: The quantitative linear-time\u2013branching-time spectrum. In: Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2011. LIPIcs, vol.\u00a013, pp. 103\u2013114. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2011)"},{"key":"28_CR21","doi-asserted-by":"crossref","unstructured":"Fan, T.: Fuzzy bisimulation for G\u00f6del modal logic. IEEE Trans. Fuzzy Sys. 23, 2387\u20132396 (Dec 2015)","DOI":"10.1109\/TFUZZ.2015.2426724"},{"key":"28_CR22","unstructured":"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\u2013314 (2015)"},{"key":"28_CR23","doi-asserted-by":"crossref","unstructured":"Flagg, B., Kopperman, R.: Continuity spaces: Reconciling domains and metric spaces. Theoretical Computer Science 177(1), 111 \u2013 138 (1997)","DOI":"10.1016\/S0304-3975(97)00236-3"},{"key":"28_CR24","doi-asserted-by":"crossref","unstructured":"Flagg, R.: Quantales and continuity spaces. Algebra Univ. 37(3), 257\u2013276 (1997)","DOI":"10.1007\/s000120050018"},{"key":"28_CR25","doi-asserted-by":"crossref","unstructured":"Gavazzo, F.: Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances. In: Logic in Computer Science, LICS 2018. pp. 452\u2013461. ACM (2018)","DOI":"10.1145\/3209108.3209149"},{"key":"28_CR26","unstructured":"Giacalone, A., Jou, C., Smolka, S.: Algebraic reasoning for probabilistic concurrent systems. In: Programming concepts and methods, PCM 1990. pp. 443\u2013458. North-Holland (1990)"},{"key":"28_CR27","unstructured":"Halpern, J.Y.: An analysis of first-order logics of probability. Artif. Intell 46, 311\u2013350 (1990)"},{"key":"28_CR28","doi-asserted-by":"crossref","unstructured":"Hansen, H., Kupke, C., Pacuit, E.: Neighbourhood structures: Bisimilarity and basic model theory. Log. Meth. Comput. Sci. 5(2) (2009)","DOI":"10.2168\/LMCS-5(2:2)2009"},{"key":"28_CR29","unstructured":"Hennessy, M., Milner, R.: Algebraic laws for non-determinism and concurrency. J. ACM 32, 137\u2013161 (1985)"},{"key":"28_CR30","unstructured":"Henriksen, M., Kopperman, R.: A general theory of structure spaces with applications to spaces of prime ideals. Alg. Univ. 28(3), 349\u2013376 (1991)"},{"key":"28_CR31","unstructured":"Hofmann, D.: Topological theories and closed objects. Adv. Math. 215(2), 789 \u2013 824 (2007)"},{"key":"28_CR32","doi-asserted-by":"crossref","unstructured":"Hofmann, D., Reis, C.: Probabilistic metric spaces as enriched categories. Fuzzy Sets Sys. 210, 1\u201321 (2013)","DOI":"10.1016\/j.fss.2012.05.005"},{"key":"28_CR33","unstructured":"Hofmann, D., Waszkiewicz, P.: Approximation in quantale-enriched categories. Topol. Appl. 158(8), 963\u2013977 (2011)"},{"key":"28_CR34","unstructured":"Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: Logic in Computer Science, LICS 1997. pp. 111\u2013122. IEEE (1997)"},{"key":"28_CR35","doi-asserted-by":"crossref","unstructured":"Janin, D., Walukiewicz, I.: Automata for the modal $$\\mu $$-calculus and related results. In: Mathematical Foundations of Computer Science, MFCS 1995. LNCS, vol.\u00a0969, pp. 552\u2013562. Springer (1995)","DOI":"10.1007\/3-540-60246-1_160"},{"key":"28_CR36","unstructured":"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.\u00a042, pp. 18\u201340. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2015)"},{"key":"28_CR37","unstructured":"K\u00f6nig, 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.\u00a0118, pp. 37:1\u201337:17. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2018)"},{"key":"28_CR38","unstructured":"Kontinen, J., M\u00fcller, J., Schnoor, H., Vollmer, H.: A van Benthem theorem for modal team semantics. In: Computer Science Logic, CSL 2015. LIPIcs, vol.\u00a041, pp. 277\u2013291. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2015)"},{"key":"28_CR39","unstructured":"Larsen, K., Skou, A.: Bisimulation through probabilistic testing. Inform. Comput. 94, 1\u201328 (1991)"},{"key":"28_CR40","doi-asserted-by":"crossref","unstructured":"Litak, T., Pattinson, D., Sano, K., Schr\u00f6der, L.: Coalgebraic predicate logic. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) Automata, Languages, and Programming, ICALP 2012. LNCS, vol.\u00a07392, pp. 299\u2013311. Springer (2012)","DOI":"10.1007\/978-3-642-31585-5_29"},{"key":"28_CR41","doi-asserted-by":"crossref","unstructured":"Lukasiewicz, T., Straccia, U.: Managing uncertainty and vagueness in description logics for the semantic web. J. Web Sem. 6(4), 291\u2013308 (2008)","DOI":"10.1016\/j.websem.2008.04.001"},{"key":"28_CR42","unstructured":"Morgan, C., McIver, A.: A probabilistic temporal calculus based on expectations. In: Groves, L., Reeves, S. (eds.) Formal Methods Pacific, FMP 1997. Springer (1997)"},{"key":"28_CR43","unstructured":"Nov\u00e1k, V.: First-order fuzzy logic. Stud. Log. 46, 87\u2013109 (1987)"},{"key":"28_CR44","unstructured":"Otto, M.: Elementary proof of the van Benthem-Rosen characterisation theorem. Tech. Rep.\u00a02342, Department of Mathematics, Technische Universit\u00e4t Darmstadt (2004)"},{"key":"28_CR45","unstructured":"Pattinson, D.: Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Log. 45, 19\u201333 (2004)"},{"key":"28_CR46","doi-asserted-by":"crossref","unstructured":"Raney, G.: Completely distributive complete lattices. Proc. AMS 3(5), 677\u2013680 (1952)","DOI":"10.1090\/S0002-9939-1952-0052392-3"},{"key":"28_CR47","doi-asserted-by":"crossref","unstructured":"Raney, G.: A subdirect-union representation for completely distributive complete lattices. Proc. AMS 4(4), 518\u2013522 (1953)","DOI":"10.1090\/S0002-9939-1953-0058568-4"},{"key":"28_CR48","doi-asserted-by":"crossref","unstructured":"Rosen, E.: Modal logic over finite structures. J. Logic, Language and Information 6(4), 427\u2013439 (1997)","DOI":"10.1023\/A:1008275906015"},{"key":"28_CR49","unstructured":"Rutten, J.: Universal coalgebra: A theory of systems. Theoret. Comput. Sci. 249, 3\u201380 (2000)"},{"key":"28_CR50","unstructured":"Schr\u00f6der, L.: Expressivity of coalgebraic modal logic: The limits and beyond. Theoret. Comput. Sci. 390, 230\u2013247 (2008)"},{"key":"28_CR51","unstructured":"Schr\u00f6der, L., Pattinson, D.: Description logics and fuzzy probability. In: Walsh, T. (ed.) Int. Joint Conf. Artificial Intelligence, IJCAI 2011. pp. 1075\u20131081. AAAI (2011)"},{"key":"28_CR52","unstructured":"Schr\u00f6der, L., Pattinson, D., Litak, T.: A van Benthem\/Rosen theorem for coalgebraic predicate logic. J. Log. Comput. 27(3), 749\u2013773 (2017)"},{"key":"28_CR53","unstructured":"Straccia, U.: A fuzzy description logic. In: Artificial Intelligence, AAAI 1998. pp. 594\u2013599. AAAI Press \/ MIT Press (1998)"},{"key":"28_CR54","doi-asserted-by":"crossref","unstructured":"Sturm, H., Wolter, F.: First-order expressivity for S5-models: Modal vs. two-sorted languages. J. Philos. Logic 30, 571\u2013591 (2001)","DOI":"10.1023\/A:1013360121031"},{"key":"28_CR55","doi-asserted-by":"crossref","unstructured":"Wild, P., Schr\u00f6der, L.: A characterization theorem for a modal description logic. In: Int. Joint Conf. Artificial Intelligence, IJCAI 2017. pp. 1304\u20131310. ijcai.org (2017)","DOI":"10.24963\/ijcai.2017\/181"},{"key":"28_CR56","unstructured":"Wild, P., Schr\u00f6der, L.: Characteristic logics for behavioural metrics via fuzzy lax extensions. In: Concurrency Theory, CONCUR 2020. LIPIcs, vol.\u00a0171, pp. 27:1\u201327:23. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2020)"},{"key":"28_CR57","doi-asserted-by":"crossref","unstructured":"Wild, P., Schr\u00f6der, L., Pattinson, D., K\u00f6nig, B.: A van Benthem theorem for fuzzy modal logic. In: Logic in Computer Science, LICS 2018. pp. 909\u2013918. ACM (2018)","DOI":"10.1145\/3209108.3209180"},{"key":"28_CR58","doi-asserted-by":"crossref","unstructured":"Wild, P., Schr\u00f6der, L., Pattinson, D., K\u00f6nig, 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\u20131906. ijcai.org (2019)","DOI":"10.24963\/ijcai.2019\/263"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-71995-1_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T17:12:33Z","timestamp":1616433153000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-71995-1_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030719944","9783030719951"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-71995-1_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FOSSACS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"88","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3,2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}