Document Open Access Logo

Expressive Logics for Coinductive Predicates

Authors Clemens Kupke, Jurriaan Rot

PDF
Thumbnail PDF

File

LIPIcs.CSL.2020.26.pdf
  • Filesize: 0.51 MB
  • 18 pages

Document Identifiers

Author Details

Clemens Kupke
  • Strathclyde University, United Kingdom
Jurriaan Rot
  • University College London, United Kingdom and Radboud University, The Netherlands

Funding

This work was partially supported by a Marie Curie Fellowship (grant code 795119).

Acknowledgements

We would like to thank Bart Jacobs for useful discussions and the anonymous referees for their very constructive and helpful feedback.

Cite AsGet BibTex

Clemens Kupke and Jurriaan Rot. Expressive Logics for Coinductive Predicates. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CSL.2020.26

Abstract

The classical Hennessy-Milner theorem says that two states of an image-finite transition system are bisimilar if and only if they satisfy the same formulas in a certain modal logic. In this paper we study this type of result in a general context, moving from transition systems to coalgebras and from bisimilarity to coinductive predicates. We formulate when a logic fully characterises a coinductive predicate on coalgebras, by providing suitable notions of adequacy and expressivity, and give sufficient conditions on the semantics. The approach is illustrated with logics characterising similarity, divergence and a behavioural metric on automata.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Categorical semantics
Keywords
  • Coalgebra
  • Fibration
  • Modal Logic

Metrics

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

References

  1. Zeinab Bakhtiari and Helle Hvid Hansen. Bisimulation for Weakly Expressive Coalgebraic Modal Logics. In Filippo Bonchi and Barbara König, editors, 7th Conference on Algebra and Coalgebra in Computer Science, CALCO 2017, June 12-16, 2017, Ljubljana, Slovenia, volume 72 of LIPIcs, pages 4:1-4:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CALCO.2017.4.
  2. Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Coalgebraic Behavioral Metrics. Logical Methods in Computer Science, 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:20)2018.
  3. Marta Bílková and Matej Dostál. Expressivity of Many-Valued Modal Logics, Coalgebraically. In Jouko A. Väänänen, Åsa Hirvonen, and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information, and Computation - 23rd International Workshop, WoLLIC 2016, Puebla, Mexico, August 16-19th, 2016. Proceedings, volume 9803 of Lecture Notes in Computer Science, pages 109-124. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-52921-8_8.
  4. Filippo Bonchi, Barbara König, and Daniela Petrisan. Up-To Techniques for Behavioural Metrics via Fibrations. In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, volume 118 of LIPIcs, pages 17:1-17:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.17.
  5. Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. A general account of coinduction up-to. Acta Inf., 54(2):127-190, 2017. URL: https://doi.org/10.1007/s00236-016-0271-4.
  6. Marcello M. Bonsangue and Alexander Kurz. Duality for Logics of Transition Systems. In Vladimiro Sassone, editor, Foundations of Software Science and Computational Structures, 8th International Conference, FOSSACS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, volume 3441 of LNCS, pages 455-469. Springer, 2005. URL: https://doi.org/10.1007/978-3-540-31982-5_29.
  7. Florence Clerc, Nathanaël Fijalkow, Bartek Klin, and Prakash Panangaden. Expressiveness of probabilistic modal logics: A gradual approach. Inf. Comput., 267:145-163, 2019. URL: https://doi.org/10.1016/j.ic.2019.04.002.
  8. Josee Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for Labelled Markov Processes. Inf. Comput., 179(2):163-193, 2002. URL: https://doi.org/10.1006/inco.2001.2962.
  9. Ulrich Dorsch, Stefan Milius, and Lutz Schröder. Graded Monads and Graded Logics for the Linear Time - Branching Time Spectrum. In Proceedings of CONCUR 2019, to appear, 2019. Google Scholar
  10. Sebastian Enqvist. Homomorphisms of Coalgebras from Predicate Liftings. In Reiko Heckel and Stefan Milius, editors, Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, Warsaw, Poland, September 3-6, 2013. Proceedings, volume 8089 of Lecture Notes in Computer Science, pages 126-140. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40206-7_11.
  11. Daniel Gorín and Lutz Schröder. Simulations and Bisimulations for Coalgebraic Modal Logics. In Reiko Heckel and Stefan Milius, editors, Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, Warsaw, Poland, September 3-6, 2013. Proceedings, volume 8089 of Lecture Notes in Computer Science, pages 253-266. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40206-7_19.
  12. Ichiro Hasuo, Toshiki Kataoka, and Kenta Cho. Coinductive predicates and final sequences in a fibration. Mathematical Structures in Computer Science, 28(4):562-611, 2018. URL: https://doi.org/10.1017/S0960129517000056.
  13. Matthew Hennessy and Robin Milner. Algebraic Laws for Nondeterminism and Concurrency. J. ACM, 32(1):137-161, 1985. URL: https://doi.org/10.1145/2455.2460.
  14. Claudio Hermida and Bart Jacobs. Structural Induction and Coinduction in a Fibrational Setting. Information and Computation, 145(2):107-152, 1998. URL: https://doi.org/10.1006/inco.1998.2725.
  15. Horst Herrlich. Topological functors. General Topology and its Applications, 4(2):125-142, 1974. URL: https://doi.org/10.1016/0016-660X(74)90016-6.
  16. Jesse Hughes and Bart Jacobs. Simulations in coalgebra. Theor. Comput. Sci., 327(1-2):71-108, 2004. URL: https://doi.org/10.1016/j.tcs.2004.07.022.
  17. Bart Jacobs. Categorical Logic and Type Theory. Elsevier, 1999. Google Scholar
  18. Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation, volume 59 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. URL: https://doi.org/10.1017/CBO9781316823187.
  19. Bart Jacobs and Ana Sokolova. Exemplaric Expressivity of Modal Logics. Journal of Logic and Computation, 20(5):1041-1068, 2009. Google Scholar
  20. Krzysztof Kapulkin, Alexander Kurz, and Jiri Velebil. Expressiveness of Positive Coalgebraic Logic. In Thomas Bolander, Torben Braüner, Silvio Ghilardi, and Lawrence S. Moss, editors, Advances in Modal Logic 9, papers from the ninth conference on "Advances in Modal Logic," held in Copenhagen, Denmark, 22-25 August 2012, pages 368-385. College Publications, 2012. URL: http://www.aiml.net/volumes/volume9/Kapulkin-Kurz-Velebil.pdf.
  21. Bartek Klin. The Least Fibred Lifting and the Expressivity of Coalgebraic Modal Logic. In José Luiz Fiadeiro, Neil Harman, Markus Roggenbach, and Jan J. M. M. Rutten, editors, Algebra and Coalgebra in Computer Science: First International Conference, CALCO 2005, Swansea, UK, September 3-6, 2005, Proceedings, volume 3629 of Lecture Notes in Computer Science, pages 247-262. Springer, 2005. URL: https://doi.org/10.1007/11548133_16.
  22. Bartek Klin. Coalgebraic Modal Logic Beyond Sets. Electr. Notes Theor. Comput. Sci., 173:177-201, 2007. URL: https://doi.org/10.1016/j.entcs.2007.02.034.
  23. Y. Komorida, S. Katsumata, N. Hu, B. Klin, and I. Hasuo. Codensity games for bisimilarity. In Proceedings of LICS 2019, to appear, 2019. Google Scholar
  24. Barbara König and Christina Mika-Michalski. (Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras. In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, volume 118 of LIPIcs, pages 37:1-37:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.37.
  25. Clemens Kupke, Alexander Kurz, and Dirk Pattinson. Algebraic Semantics for Coalgebraic Logics. Electr. Notes Theor. Comput. Sci., 106:219-241, 2004. URL: https://doi.org/10.1016/j.entcs.2004.02.037.
  26. Clemens Kupke and Dirk Pattinson. Coalgebraic semantics of modal logics: An overview. Theor. Comput. Sci., 412(38):5070-5094, 2011. URL: https://doi.org/10.1016/j.tcs.2011.04.023.
  27. Kim Guldstrand Larsen and Arne Skou. Bisimulation through Probabilistic Testing. Inf. Comput., 94(1):1-28, 1991. URL: https://doi.org/10.1016/0890-5401(91)90030-6.
  28. Johannes Marti and Yde Venema. Lax extensions of coalgebra functors and their logic. Journal of Computer and System Sciences, 81(5):880-900, 2015. CMCS 2012 (Selected Papers). URL: https://doi.org/10.1016/j.jcss.2014.12.006.
  29. Dirk Pattinson. Expressive Logics for Coalgebras via Terminal Sequence Induction. Notre Dame Journal of Formal Logic, 45(1):19-33, 2004. URL: https://doi.org/10.1305/ndjfl/1094155277.
  30. Dusko Pavlovic, Michael W. Mislove, and James Worrell. Testing Semantics: Connecting Processes and Process Logics. In Michael Johnson and Varmo Vene, editors, Algebraic Methodology and Software Technology, 11th International Conference, AMAST 2006, Proceedings, volume 4019 of LNCS, pages 308-322. Springer, 2006. URL: https://doi.org/10.1007/11784180_24.
  31. H. E. Porst and W. Tholen. Concrete Dualities. In H. E. Porst and W. Tholen, editors, Categories at Work, pages 111-136. Heldermann Verlag, 1991. Google Scholar
  32. Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):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. Theor. Comput. Sci., 390(2-3):230-247, 2008. URL: https://doi.org/10.1016/j.tcs.2007.09.023.
  34. David Sprunger, Shin-ya Katsumata, Jérémy Dubut, and Ichiro Hasuo. Fibrational Bisimulations and Quantitative Reasoning. In Corina Cîrstea, editor, Coalgebraic Methods in Computer Science - 14th IFIP WG 1.3 International Workshop, CMCS 2018, Colocated with ETAPS 2018, Thessaloniki, Greece, April 14-15, 2018, Revised Selected Papers, volume 11202 of Lecture Notes in Computer Science, pages 190-213. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-00389-0_11.
  35. Franck van Breugel and James Worrell. A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci., 331(1):115-142, 2005. URL: https://doi.org/10.1016/j.tcs.2004.09.035.
  36. Rob J. van Glabbeek. The Linear Time-Branching Time Spectrum (Extended Abstract). In Jos C. M. Baeten and Jan Willem Klop, editors, CONCUR '90, Theories of Concurrency: Unification and Extension, Amsterdam, The Netherlands, August 27-30, 1990, Proceedings, volume 458 of Lecture Notes in Computer Science, pages 278-297. Springer, 1990. URL: https://doi.org/10.1007/BFb0039066.
  37. 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, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 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