Document Open Access Logo

Safety and Strong Completeness via Reducibility for Many-Valued Coalgebraic Dynamic Logics

Authors Helle Hvid Hansen , Wolfgang Poiger

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CALCO.2025.9.pdf
  • Filesize: 0.96 MB
  • 23 pages
HTML5 Logo HTML (experimental)
LIPIcs.CALCO.2025.9.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Program reasoning
Keywords
  • dynamic logic
  • many-valued coalgebraic logic
  • safety
  • strong completeness

Metrics

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

Abstract

We present a coalgebraic framework for studying generalisations of dynamic modal logics such as PDL and game logic in which both the propositions and the semantic structures can take values in an algebra 𝐀 of truth-degrees. More precisely, we work with coalgebraic modal logic via 𝐀-valued predicate liftings where 𝐀 is an FLew-algebra, and interpret actions (abstracting programs and games) as 𝖥-coalgebras where the functor 𝖥 represents some type of 𝐀-weighted system. We also allow combinations of crisp propositions with 𝐀-weighted systems and vice versa. We introduce coalgebra operations and tests, with a focus on operations which are reducible in the sense that modalities for composed actions can be reduced to compositions of modalities for the constituent actions. We prove that reducible operations are safe for bisimulation and behavioural equivalence, and prove a general strong completeness result, from which we obtain new strong completeness results for 𝟐-valued iteration-free PDL with 𝐀-valued accessibility relations when 𝐀 is a finite chain, and for many-valued iteration-free game logic with many-valued strategies based on finite Lukasiewicz logic.

Cite As Get BibTex

Helle Hvid Hansen and Wolfgang Poiger. Safety and Strong Completeness via Reducibility for Many-Valued Coalgebraic Dynamic Logics. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 9:1-9:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CALCO.2025.9

Author Details

Helle Hvid Hansen
  • Bernoulli Institute of Maths, CS and AI, University of Groningen, The Netherlands
Wolfgang Poiger
  • Institute of Computer Science of the Czech Academy of Sciences, Prague, Czech Republic

Funding

  • Poiger, Wolfgang: Received financial support from the European Union under the project no. CZ.02.01.01/00/23_025/0008724 via the Operational Programme Jan Amos Komenský, and from the University of Groningen.

References

  1. 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 Olaf Beyersdorff, Mamadou M. Kanté, Orna Kupferman, and Daniel Lokshtanov, editors, 41st International Symposium on Theoretical Aspects of Computer Science (STACS'24), volume 289 of Leibniz International Proceedings in Informatics, pages 10:1-10:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.STACS.2024.10.
  2. Marta Bílková and Matěj Dostál. Many-valued relation lifting and Moss' coalgebraic logic. In Reiko Heckel and Stefan Milius, editors, Algebra and Coalgebra in Computer Science (CALCO'13), pages 66-79. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40206-7_7.
  3. Marta Bílková and Matěj Dostál. Expressivity of many-valued modal logics, coalgebraically. In Jouko Väänänen, Åsa Hirvonen, and Ruy de Queiroz, editors, Logic, Language, Information, and Computation (WoLLIC'16), pages 109-124. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-52921-8_8.
  4. Félix Bou, Francesc Esteva, Lluís Godo, and Ricardo O. Rodríguez. On the minimum many-valued modal logic over a finite residuated lattice. Journal of Logic and Computation, 21(5):739-790, 2011. URL: https://doi.org/10.1093/logcom/exp062.
  5. Xavier Caicedo and Ricardo O. Rodríguez. Standard Gödel modal logics. Studia Logica, 94(2):189-214, 2010. URL: https://doi.org/10.1007/s11225-010-9230-1.
  6. Roberto L. O. Cignoli, Itala M. L. D’Ottaviano, and Daniele Mundici. Algebraic Foundations of Many-Valued Reasoning, volume 7 of Trends in Logic. Springer, 2000. Google Scholar
  7. Petr Cintula and Carles Noguera. Neighborhood semantics for modal many-valued logics. Fuzzy Sets and Systems, 345:99-112, 2018. URL: https://doi.org/10.1016/j.fss.2017.10.009.
  8. Fredrik Dahlqvist and Alexander Kurz. The positivication of coalgebraic logics. In Filippo Bonchi and Barbara König, editors, Algebra and Coalgebra in Computer Science (CALCO'17), volume 72 of Leibniz International Proceedings in Informatics, pages 9:1-9:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CALCO.2017.9.
  9. Ernst-Erich Doberkat. Towards a probabilistic interpretation of game logic. In Wolfram Kahl, Michael Winter, and José Oliveira, editors, Relational and Algebraic Methods in Computer Science (RAMiCS'15), pages 43-47. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24704-5_3.
  10. Michael J. Fischer and Richard E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18(2):194-211, 1979. URL: https://doi.org/10.1016/0022-0000(79)90046-1.
  11. Melvin C. Fitting. Many-valued modal logics. Fundamenta Informaticae, 15(3-4):235-254, 1991. URL: https://doi.org/10.3233/FI-1991-153-404.
  12. Melvin C. Fitting. Many-valued modal logics II. Fundamenta Informaticae, 17(1-2):55-73, 1992. URL: https://doi.org/10.3233/FI-1992-171-205.
  13. Nikolaos Galatos, Peter Jipsen, Tomasz Kowalski, and Hiroakira Ono. Residuated Lattices: An algebraic glimpse at substructural logics, volume 151 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2007. Google Scholar
  14. Petr Hájek. Metamathematics of Fuzzy Logic, volume 4 of Trends in Logic. Springer, 1998. URL: https://doi.org/10.1007/978-94-011-5300-3.
  15. Petr Hájek, Lluís Godo, and Francesc Esteva. A complete many-valued logic with product-conjunction. Archive for Mathematical Logic, 35(3):191-208, 1996. URL: https://doi.org/10.1007/BF01268618.
  16. Helle H. Hansen and Clemens Kupke. Weak Completeness of Coalgebraic Dynamic Logics. In Ralph Matthes and Matteo Mio, editors, Tenth International Workshop on Fixed Points in Computer Science (FICS'15), volume 191 of EPTCS, pages 90-104, 2015. URL: https://doi.org/10.4204/EPTCS.191.9.
  17. Helle H. Hansen, Clemens Kupke, and Raul A. Leal. Strong completeness for iteration-free coalgebraic dynamic logics. In Josep Díaz, Ivan Lanese, and Davide Sangiorgi, editors, 8th International Conference on Theoretical Computer Science (TCS'14), pages 281-295. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44602-7_22.
  18. Georges Hansoul and Bruno Teheux. Extending Łukasiewicz logics with a modality: Algebraic approach to relational semantics. Studia Logica, 101(3):505-545, 2013. URL: https://doi.org/10.1007/s11225-012-9396-9.
  19. David Harel, Dexter Kozen, and Jerzy Tiuryn. Dynamic Logic. MIT Press, 2000. Google Scholar
  20. Bartek Klin and Julian Salamanca. Iterated covariant powerset is not a monad. Electronic Notes in Theoretical Computer Science, 341:261-276, 2018. URL: https://doi.org/10.1016/j.entcs.2018.11.013.
  21. Dexter Kozen. A probabilistic PDL. Journal of Computer and System Sciences, 30(2):162-178, 1985. URL: https://doi.org/10.1016/0022-0000(85)90012-1.
  22. Clemens Kupke and Dirk Pattinson. Coalgebraic semantics of modal logics: An overview. Theoretical Computer Science, 412(38):5070-5094, 2011. URL: https://doi.org/10.1016/j.tcs.2011.04.023.
  23. Alexander Kurz and Wolfgang Poiger. Many-Valued Coalgebraic Logic: From Boolean Algebras to Primal Varieties. In Paolo Baldan and Valeria de Paiva, editors, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO'23), volume 270 of Leibniz International Proceedings in Informatics, pages 17:1-17:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.CALCO.2023.17.
  24. Alexander Kurz, Wolfgang Poiger, and Bruno Teheux. Many-valued coalgebraic logic over semi-primal varieties. Logical Methods in Computer Science, 20(3), 2024. URL: https://doi.org/10.46298/lmcs-20(3:6)2024.
  25. Alexander Kurz, Wolfgang Poiger, and Bruno Teheux. New perspectives on semi-primal varieties. Journal of Pure and Applied Algebra, 228(4):article no. 107525, 2024. URL: https://doi.org/10.1016/j.jpaa.2023.107525.
  26. Saunders Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer, second edition, 1997. URL: https://doi.org/10.1007/978-1-4757-4721-8.
  27. Chun-Yu Lin and Churn-Jung Liau. Many-valued coalgebraic modal logic: One-step completeness and finite model property. Fuzzy Sets and Systems, 467:article no. 108564, 2023. URL: https://doi.org/10.1016/j.fss.2023.108564.
  28. Minghui Ma and Shanxia Wang. Finite-chain graded modal logic. In Shier Ju, Hu Liu, and Hiroakira Ono, editors, Modality, Semantics and Interpretations: The Second Asian Workshop on Philosophical Logic, pages 71-85. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47197-5_4.
  29. Eric Pacuit. Neighborhood Semantics for Modal Logic. Short Textbooks in Logic. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-67149-9.
  30. Rohit Parikh. Propositional game logic. In 24th Annual Symposium on Foundations of Computer Science, pages 195-200. IEEE Computer Society, 1983. URL: https://doi.org/10.1109/SFCS.1983.47.
  31. Dirk Pattinson. Coalgebraic modal logic: Soundness, completeness and decidability of local consequence. Theoretical Computer Science, 309(1):177-193, 2003. URL: https://doi.org/10.1016/S0304-3975(03)00201-9.
  32. Dirk Pattinson. An introduction to the theory of coalgebras. Lecture notes for NASSLLI'03. Available online at https://ncatlab.org/nlab/files/Pattinson-Coalgebras.pdf (Accessed: Feb 26, 2025), 2003.
  33. Marc Pauly. From programs to games: Invariance and safety for bisimulation. In Peter G. Clote and Helmut Schwichtenberg, editors, Computer Science Logic, volume 1862 of Lecture Notes in Computer Science, pages 485-496. Springer, 2000. URL: https://doi.org/10.1007/3-540-44622-2_33.
  34. Marc Pauly and Rohit Parikh. Game logic - An overview. Studia Logica, 75(2):165-182, 2003. URL: https://doi.org/10.1023/A:1027354826364.
  35. André Platzer. Differential game logic. ACM Trans. Comput. Log., 17(1):1-51, 2015. URL: https://doi.org/10.1145/2817824.
  36. Norbert Preining. Gödel logics - A survey. In Christian G. Fermüller and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'10), pages 30-51. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-16242-8_4.
  37. Ricardo O. Rodríguez and Amanda Vidal. Axiomatization of crisp Gödel modal logic. Studia Logica, 109(2):367-395, 2021. URL: https://doi.org/10.1007/s11225-020-09910-5.
  38. J.J.M.M. Rutten. Universal coalgebra: A theory of systems. Theoretical Computer Science, 249(1):3-80, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00056-6.
  39. Lutz Schröder and Dirk Pattinson. Strong completeness of coalgebraic modal logics. In Susanne Albers and Jean-Yves Marion, editors, 26th International Symposium on Theoretical Aspects of Computer Science (STACS'09), volume 3 of Leibniz International Proceedings in Informatics, pages 673-684, 2009. URL: https://doi.org/10.4230/LIPICS.STACS.2009.1855.
  40. Lutz Schröder and Dirk Pattinson. Coalgebraic correspondence theory. In Luke Ong, editor, Foundations of Software Science and Computational Structures (FoSSaCS'10), pages 328-342. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12032-9_23.
  41. Lutz Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theoretical Computer Science, 390(2):230-247, 2008. URL: https://doi.org/10.1016/j.tcs.2007.09.023.
  42. Lutz Schröder and Dirk Pattinson. Description logics and fuzzy probability. In Toby Walsh, editor, 22nd International Joint Conference on Artificial Intelligence. International Joint Conference on Artificial Intelligence (IJCAI'11). AAAI Press, 2011. Google Scholar
  43. Igor Sedlàr. Propositional dynamic logic with Belnapian truth values. In Stéphane Demri Lev Beklemishev and András Máté', editors, Advances in Modal Logic (AiML'16), volume 11, pages 503-519. College Publications, 2016. URL: http://www.aiml.net/volumes/volume11/Sedlar.pdf.
  44. Igor Sedlàr. Finitely-valued Propositional Dynamic Logic. In Nicola Olivetti, Rineke Verbrugge, Sara Negri, and Gabriel Sandu, editors, Advances in Modal Logic (AiML'20), volume 13, pages 561-579. College Publications, 2020. URL: http://www.aiml.net/volumes/volume13/Sedlar.pdf.
  45. Bruno Teheux. Propositional dynamic logic for searching games with errors. Journal of Applied Logic, 12(4):377-394, 2014. URL: https://doi.org/10.1016/j.jal.2014.04.001.
  46. Samuel Teuber, Stefan Mitsch, and André Platzer. Provably safe neural network controllers via differential dynamic logic. In Amir Globersons, Lester Mackey, Danielle Belgrave, Angela Fan, Ulrich Paquet, Jakub M. Tomczak, and Cheng Zhang, editors, Advances in Neural Information Processing Systems 38 (NeurIPS'24), 2024. Google Scholar
  47. Johan van Benthem. Program constructions that are safe for bisimulation. Studia Logica, 60:311-330, 1998. URL: https://doi.org/10.1023/A:1005072201319.
  48. Johan van Benthem, Nick Bezhanishvili, and Sebastian Enqvist. A propositional dynamic logic for instantial neighborhood semantics. Studia Logica, 107(4):719-751, 2019. URL: https://doi.org/10.1007/s11225-018-9825-5.
  49. Johan van Benthem, Nick Bezhanishvili, Sebastian Enqvist, and Junhua Yu. Instantial neighbourhood logic. The Review of Symbolic Logic, 10(1):116-144, 2017. URL: https://doi.org/10.1017/S1755020316000447.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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