Expressive Quantale-Valued Logics for Coalgebras: An Adjunction-Based Approach

Beohar H, Gurke S, König B, Messing K, Forster J, Schröder L, Wild P (2024)

Publication Type: Conference contribution

Publication year: 2024

Journal

LIPIcs : Leibniz International Proceedings in Informatics Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik

Publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

Book Volume: 289

Conference Proceedings Title: Leibniz International Proceedings in Informatics, LIPIcs

Event location: Clermont-Ferrand, FRA

ISBN: 9783959773119

DOI: 10.4230/LIPIcs.STACS.2024.10

Abstract

We address the task of deriving fixpoint equations from modal logics characterizing behavioural equivalences and metrics (summarized under the term conformances). We rely on an earlier work that obtains Hennessy-Milner theorems as corollaries to a fixpoint preservation property along Galois connections between suitable lattices. We instantiate this to the setting of coalgebras, in which we spell out the compatibility property ensuring that we can derive a behaviour function whose greatest fixpoint coincides with the logical conformance. We then concentrate on the linear-time case, for which we study coalgebras based on the machine functor living in Eilenberg-Moore categories, a scenario for which we obtain a particularly simple logic and fixpoint equation. The theory is instantiated to concrete examples, both in the branching-time case (bisimilarity and behavioural metrics) and in the linear-time case (trace equivalences and trace distances).

Authors with CRIS profile

Jonas Forster Lehrstuhl für Informatik 8 (Theoretische Informatik) Lutz Schröder Lehrstuhl für Informatik 8 (Theoretische Informatik) Paul Wild Lehrstuhl für Informatik 8 (Theoretische Informatik)

Involved external institutions

University of Sheffield GB United Kingdom (GB) Universität Duisburg-Essen (UDE) DE Germany (DE)

How to cite

APA:

Beohar, H., Gurke, S., König, B., Messing, K., Forster, J., Schröder, L., & Wild, P. (2024). Expressive Quantale-Valued Logics for Coalgebras: An Adjunction-Based Approach. In Olaf Beyersdorff, Mamadou Moustapha Kante, Orna Kupferman, Daniel Lokshtanov (Eds.), Leibniz International Proceedings in Informatics, LIPIcs. Clermont-Ferrand, FRA: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.

MLA:

Beohar, Harsh, et al. "Expressive Quantale-Valued Logics for Coalgebras: An Adjunction-Based Approach." Proceedings of the 41st International Symposium on Theoretical Aspects of Computer Science, STACS 2024, Clermont-Ferrand, FRA Ed. Olaf Beyersdorff, Mamadou Moustapha Kante, Orna Kupferman, Daniel Lokshtanov, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2024.

BibTeX: Download