Document Open Access Logo

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

Authors Harsh Beohar , Sebastian Gurke , Barbara König , Karla Messing , Jonas Forster , Lutz Schröder , Paul Wild

PDF
Thumbnail PDF

File

LIPIcs.STACS.2024.10.pdf
  • Filesize: 0.93 MB
  • 19 pages

Document Identifiers

Author Details

Harsh Beohar
  • University of Sheffield, UK
Sebastian Gurke
  • Universität Duisburg-Essen, Germany
Barbara König
  • Universität Duisburg-Essen, Germany
Karla Messing
  • Universität Duisburg-Essen, Germany
Jonas Forster
  • Friedrich-Alexander-Universität Erlangen-, Nürnberg, Germany
Lutz Schröder
  • Friedrich-Alexander-Universität Erlangen-, Nürnberg, Germany
Paul Wild
  • Friedrich-Alexander-Universität Erlangen-, Nürnberg, Germany

Funding

The first author was supported by the EPSRC NIA Grant EP/X019373/1, while the remaining authors were supported by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - project number 434050016 (SpeQt).

Cite AsGet BibTex

Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing, Jonas Forster, Lutz Schröder, and Paul Wild. Expressive Quantale-Valued Logics for Coalgebras: An Adjunction-Based Approach. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/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).

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • modal logics
  • coalgebras
  • behavioural equivalences
  • behavioural metrics
  • linear-time semantics
  • Eilenberg-Moore categories

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Jiří Adámek, Horst Herrlich, and George E. Strecker. Abstract and concrete categories: The joy of cats. Wiley, 1990. Republished in: Reprints in Theory and Applications of Categories, No. 17 (2006) pp. 1-507. URL: http://tac.mta.ca/tac/reprints/articles/17/tr17abs.html.
  2. Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Coalgebraic behavioral metrics. Logical Methods in Computer Science, 14(3), 2018. Selected Papers of the 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Google Scholar
  3. Paolo Baldan, Barbara König, and Tommaso Padoan. Abstraction, up-to techniques and games for systems of fixpoint equations. In Proc. of CONCUR '20, volume 171 of LIPIcs, pages 25:1-25:20. Schloss Dagstuhl - Leibniz Center for Informatics, 2020. Google Scholar
  4. Harsh Beohar, Sebastian Gurke, Barbara König, and Karla Messing. Hennessy-Milner theorems via Galois connections. In Proc. of CSL '23, volume 252 of LIPIcs, pages 12:1-12:18. Schloss Dagstuhl - Leibniz Center for Informatics, 2023. Google Scholar
  5. Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing, Jonas Forster, Lutz Schröder, and Paul Wild. Expressive quantale-valued logics for coalgebras: an adjunction-based approach, 2023. arXiv:2310.05711. URL: https://arxiv.org/abs/2310.05711.
  6. Filippo Bonchi, Alexandra Silva, and Ana Sokolova. The Power of Convex Algebras. In Proc. of CONCUR '17, volume 85 of LIPIcs, pages 23:1-23:18. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017. Google Scholar
  7. Corina Cîrstea. From branching to linear time, coalgebraically. Fundamenta Informaticae, 150(3-4):379-406, 2017. Google Scholar
  8. Patrick Cousot and Radhia Cousot. Systematic design of program analysis frameworks. In Proc. of POPL '79, pages 269-282. ACM Press, 1979. Google Scholar
  9. Patrick Cousot and Radhia Cousot. Temporal abstract interpretation. In Mark N. Wegman and Thomas W. Reps, editors, Proc. of POPL '00, pages 12-25. ACM, 2000. Google Scholar
  10. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled Markov processes. Theoretical Computer Science, 318:323-354, 2004. Google Scholar
  11. Ulrich Dorsch, Stefan Milius, and Lutz Schröder. Graded monads and graded logics for the linear time - branching time spectrum. In Wan J. Fokkink and Rob van Glabbeek, editors, Concurrency Theory, CONCUR 2019, volume 140 of LIPIcs, pages 36:1-36:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.36.
  12. Jonas Forster, Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. Quantitative Hennessy-Milner Theorems via Notions of Density. In Proc. of CSL '23, volume 252 of LIPIcs, pages 22:1-22:20, 2023. Google Scholar
  13. Jonas Forster, Lutz Schröder, Paul Wild, Harsh Beohar, Sebastian Gurke, Barbara König, and Karla Messing. Graded semantics and graded logics for Eilenberg-Moore coalgebras, 2023. arXiv:2307.14826. URL: https://arxiv.org/abs/2307.14826.
  14. Alessandro Giacalone, Chi-Chang Jou, and Scott A. Smolka. Algebraic reasoning for probabilistic concurrent systems. In Manfred Broy and Cliff B. Jones, editors, Programming concepts and methods, pages 443-458. North-Holland, 1990. Google Scholar
  15. Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Logical Methods in Computer Science, 3(4:11):1-36, 2007. Google Scholar
  16. Dirk Hofmann, Gavin J. Seal, and Walter Tholen, editors. Lax algebras, pages 145-283. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2014. URL: https://doi.org/10.1017/CBO9781107517288.005.
  17. Bart Jacobs. Categorical Logic and Type Theory, volume 141 of Studies in Logic and the Foundations of Mathematics. Elsevier, 1st edition, January 1999. Google Scholar
  18. Bart Jacobs. Predicate logic for functors and monads. Available from author’s website, 2010. URL: http://www.cs.ru.nl/~bart/PAPERS/predlift-indcat.pdf.
  19. Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. URL: https://doi.org/10.1017/CBO9781316823187.
  20. Bart Jacobs, Alexandra Silva, and Ana Sokolova. Trace semantics via determinization. In Proc. of CMCS '12, pages 109-129. Springer, 2012. LNCS 7399. Google Scholar
  21. Bartek Klin. Coalgebraic modal logic beyond sets. In Proc. of MFPS '07, volume 173 of ENTCS, pages 177-201, 2007. Google Scholar
  22. Yuichi Komorida, Shin-ya Katsumata, Nick Hu, Bartek Klin, and Ichiro Hasuo. Codensity games for bisimilarity. In Proc. of LICS '19, pages 1-13, 2019. URL: https://doi.org/10.1109/LICS.2019.8785691.
  23. Yuichi Komorida, Shin-ya Katsumata, Clemens Kupke, Jurriaan Rot, and Ichiro Hasuo. Expressivity of quantitative modal logics: Categorical foundations via codensity and approximation. In Proc. LICS '21, pages 1-14. IEEE, 2021. Google Scholar
  24. Clemens Kupke and Dirk Pattinson. Coalgebraic semantics of modal logics: An overview. Theoretical Computer Science, 412:5070-5094, 2011. Google Scholar
  25. Clemens Kupke and Jurriaan Rot. Expressive logics for coinductive predicates. In Proc. of CSL '20, volume 152 of LIPIcs, pages 26:1-26:18. Schloss Dagstuhl - Leibniz Center for Informatics, 2020. Google Scholar
  26. F. William Lawvere. Metric spaces, generalized logic, and closed categories. Rendiconti del Seminario Matemàtico e Fisico di Milano, 43(1):135-166, 1973. Republished in Reprints in Theory and Applications of Categories 1 (2002), 1-37. URL: https://doi.org/10.1007/bf02924844.
  27. Stefan Milius, Dirk Pattinson, and Lutz Schröder. Generic trace semantics and graded monads. In Proc. of CALCO '15, volume 35 of LIPIcs, pages 253-269. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  28. Dusko Pavlovic, Michael Mislove, and James Worrell. Testing semantics: Connecting processes and process logics. In Proc. of AMAST '06, pages 308-322. Springer, 2006. LNCS 4019. Google Scholar
  29. Francis Jeffry Pelletier and Norman M. Martin. Post’s functional completeness theorem. Notre Dame Journal of Formal Logic, 31(2), 1990. Google Scholar
  30. Damien Pous. Complete lattices and up-to techniques. In Proc. of APLAS '07, pages 351-366. Springer, 2007. LNCS 4807. Google Scholar
  31. Michael O. Rabin. Probabilistic automata. Information and Control, 6(3):230-245, 1963. Google Scholar
  32. Jan Rutten. Universal coalgebra: A theory of systems. Theoretical Computer Science, 249:3-80, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00056-6.
  33. Lutz Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theoretical Computer Science, 390(2):230-247, 2008. Foundations of Software Science and Computational Structures. URL: https://doi.org/10.1016/j.tcs.2007.09.023.
  34. Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Generalizing the powerset construction, coalgebraically. In Proc. of FSTTCS '10, volume 8, pages 272-283. Schloss Dagstuhl - Leibniz Center for Informatics, 2010. LIPIcs. Google Scholar
  35. Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Generalizing determinization from automata to coalgebras. Logical Methods in Computer Science, 9(1:09), 2013. Google Scholar
  36. Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285-309, 1955. Google Scholar
  37. Ruben Turkenburg, Harsh Beohar, Clemens Kupke, and Jurriaan Rot. Forward and Backward Steps in a Fibration. In Paolo Baldan and Valeria de Paiva, editors, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023), volume 270 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1-6:18, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CALCO.2023.6.
  38. Franck van Breugel and James Worrell. A behavioural pseudometric for probabilistic transition systems. Theoretical Computer Science, 331:115-142, 2005. Google Scholar
  39. Rob van Glabbeek. The linear time - branching time spectrum I. In J.A. Bergstra, A. Ponse, and S.A. Smolka, editors, Handbook of Process Algebra, chapter 1, pages 3-99. Elsevier, 2001. Google Scholar
  40. Cédric Villani. Optimal Transport - Old and New, volume 338 of A Series of Comprehensive Studies in Mathematics. Springer, 2009. Google Scholar
  41. Paul Wild and Lutz Schröder. A quantified coalgebraic van Benthem theorem. In Proc. of FOSSACS '21, volume 12650 of LNCS, pages 551-571. Springer, 2021. Google Scholar
  42. Paul Wild and Lutz Schröder. Characteristic logics for behavioural hemimetrics via fuzzy lax extensions. Logical Methods in Computer Science, 18(2), 2022. URL: https://doi.org/10.46298/lmcs-18(2:19)2022.
  43. Paul Wild, Lutz Schröder, Dirk Pattinson, and Barbara König. A van Benthem theorem for fuzzy modal logic. In Anuj Dawar and Erich Grädel, editors, Logic in Computer Science, LICS 2018, pages 909-918. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209180.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact