Document Open Access Logo

Forward and Backward Steps in a Fibration

Authors Ruben Turkenburg , Harsh Beohar , Clemens Kupke , Jurriaan Rot

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2023.6.pdf
  • Filesize: 0.74 MB
  • 18 pages

Document Identifiers

Author Details

Ruben Turkenburg
  • Radboud University, Nijmegen, The Netherlands
Harsh Beohar
  • University of Sheffield, UK
Clemens Kupke
  • Strathclyde University, Glasgow, UK
Jurriaan Rot
  • Radboud University, Nijmegen, The Netherlands

Funding

Ruben Turkenburg, Jurriaan Rot: Partially supported by the NWO grant OCENW.M20.053.
  • Beohar, Harsh: Partially supported by the EPSRC grant EP/X019373/1.
  • Kupke, Clemens: Partially supported by Leverhulme Trust Research Project Grant RPG-2020-232.

Cite AsGet BibTex

Ruben Turkenburg, Harsh Beohar, Clemens Kupke, and Jurriaan Rot. Forward and Backward Steps in a Fibration. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CALCO.2023.6

Abstract

Distributive laws of various kinds occur widely in the theory of coalgebra, for instance to model automata constructions and trace semantics, and to interpret coalgebraic modal logic. We study steps, which are a general type of distributive law, that allow one to map coalgebras along an adjunction. In this paper, we address the question of what such mappings do to well known notions of equivalence, e.g., bisimilarity, behavioural equivalence, and logical equivalence. We do this using the characterisation of such notions of equivalence as (co)inductive predicates in a fibration. Our main contribution is the identification of conditions on the interaction between the steps and liftings, which guarantees preservation of fixed points by the mapping of coalgebras along the adjunction. We apply these conditions in the context of lax liftings proposed by Bonchi, Silva, Sokolova (2021), and generalise their result on preservation of bisimilarity in the construction of a belief state transformer. Further, we relate our results to properties of coalgebraic modal logics including expressivity and completeness.

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
Keywords
  • Coalgebra
  • Fibration
  • Bisimilarity

Metrics

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

References

  1. Harsh Beohar, Sebastian Gurke, Barbara König, and Karla Messing. Hennessy-Milner theorems via Galois connections. In CSL, volume 252 of LIPIcs, pages 12:1-12:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. Google Scholar
  2. Nick Bezhanishvili, Gaëlle Fontaine, and Yde Venema. Vietoris bisimulations. J. Log. Comput., 20(5):1017-1040, 2010. Google Scholar
  3. Filippo Bonchi, Barbara König, and Daniela Petrisan. Up-to techniques for behavioural metrics via fibrations. In CONCUR, volume 118 of LIPIcs, pages 17:1-17:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  4. Filippo Bonchi, Alexandra Silva, and Ana Sokolova. Distribution bisimilarity via the power of convex algebras. Log. Methods Comput. Sci., 17(3), 2021. Google Scholar
  5. Marcello M. Bonsangue and Alexander Kurz. Duality for logics of transition systems. In FoSSaCS, volume 3441 of Lecture Notes in Computer Science, pages 455-469. Springer, 2005. Google Scholar
  6. Marcello M. Bonsangue, Stefan Milius, and Alexandra Silva. Sound and complete axiomatizations of coalgebraic language equivalence. ACM Trans. Comput. Log., 14(1):7:1-7:52, 2013. Google Scholar
  7. Francis Borceux. Handbook of categorical algebra: volume 1, Basic category theory, volume 1. Cambridge University Press, 1994. Google Scholar
  8. Liang-Ting Chen and Achim Jung. On a categorical framework for coalgebraic modal logic. In MFPS, volume 308 of Electronic Notes in Theoretical Computer Science, pages 109-128. Elsevier, 2014. Google Scholar
  9. Brian A. Davey and Hilary A. Priestley. Introduction to Lattices and Order, Second Edition. Cambridge University Press, 2002. Google Scholar
  10. Richard Garner. The Vietoris monad and weak distributive laws. Appl. Categorical Struct., 28(2):339-354, 2020. Google Scholar
  11. Herman Geuvers. Apartness and distinguishing formulas in hennessy-milner logic. In A Journey from Process Algebra via Timed Automata to Model Learning, volume 13560 of Lecture Notes in Computer Science, pages 266-282. Springer, 2022. Google Scholar
  12. Herman Geuvers and Bart Jacobs. Relating apartness and bisimulation. Log. Methods Comput. Sci., 17(3), 2021. Google Scholar
  13. Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Log. Methods Comput. Sci., 3(4), 2007. Google Scholar
  14. Ichiro Hasuo, Toshiki Kataoka, and Kenta Cho. Coinductive predicates and final sequences in a fibration. Math. Struct. Comput. Sci., 28(4):562-611, 2018. Google Scholar
  15. Claudio Hermida. On fibred adjunctions and completeness for fibred categories. In COMPASS/ADT, volume 785 of Lecture Notes in Computer Science, pages 235-251. Springer, 1992. Google Scholar
  16. Claudio Hermida. Fibrations, logical predicates and indeterminates. PhD thesis, University of Edinburgh, UK, 1993. Google Scholar
  17. Claudio Hermida and Bart Jacobs. Structural induction and coinduction in a fibrational setting. Inf. Comput., 145(2):107-152, 1998. Google Scholar
  18. Jesse Hughes and Bart Jacobs. Simulations in coalgebra. Theor. Comput. Sci., 327(1-2):71-108, 2004. Google Scholar
  19. Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation, volume 59 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. Google Scholar
  20. Bart Jacobs, Alexandra Silva, and Ana Sokolova. Trace semantics via determinization. J. Comput. Syst. Sci., 81(5):859-879, 2015. Google Scholar
  21. Bart P. F. Jacobs. Categorical Logic and Type Theory, volume 141 of Studies in logic and the foundations of mathematics. North-Holland, 2001. Google Scholar
  22. Henning Kerstan, Barbara König, and Bram Westerbaan. Lifting adjunctions to coalgebras to (re)discover automata constructions. In CMCS, volume 8446 of Lecture Notes in Computer Science, pages 168-188. Springer, 2014. Google Scholar
  23. Bartek Klin. The least fibred lifting and the expressivity of coalgebraic modal logic. In CALCO, volume 3629 of Lecture Notes in Computer Science, pages 247-262. Springer, 2005. Google Scholar
  24. Bartek Klin. Coalgebraic modal logic beyond sets. In MFPS, volume 173 of Electronic Notes in Theoretical Computer Science, pages 177-201. Elsevier, 2007. Google Scholar
  25. Yuichi Komorida, Shin-ya Katsumata, Nick Hu, Bartek Klin, and Ichiro Hasuo. Codensity games for bisimilarity. In LICS, pages 1-13. IEEE, 2019. Google Scholar
  26. Yuichi Komorida, Shin-ya Katsumata, Clemens Kupke, Jurriaan Rot, and Ichiro Hasuo. Expressivity of quantitative modal logics : Categorical foundations via codensity and approximation. In LICS, pages 1-14. IEEE, 2021. Google Scholar
  27. Clemens Kupke, Alexander Kurz, and Dirk Pattinson. Algebraic semantics for coalgebraic logics. In CMCS, volume 106 of Electronic Notes in Theoretical Computer Science, pages 219-241. Elsevier, 2004. Google Scholar
  28. Clemens Kupke, Alexander Kurz, and Dirk Pattinson. Ultrafilter extensions for coalgebras. In CALCO, volume 3629 of Lecture Notes in Computer Science, pages 263-277. Springer, 2005. Google Scholar
  29. Clemens Kupke and Jurriaan Rot. Expressive logics for coinductive predicates. Log. Methods Comput. Sci., 17(4), 2021. Google Scholar
  30. Lawrence S. Moss. Coalgebraic logic. Ann. Pure Appl. Log., 96(1-3):277-317, 1999. Google Scholar
  31. Dusko Pavlovic, Michael W. Mislove, and James Worrell. Testing semantics: Connecting processes and process logics. In AMAST, volume 4019 of Lecture Notes in Computer Science, pages 308-322. Springer, 2006. Google Scholar
  32. Jurriaan Rot, Bart Jacobs, and Paul Blain Levy. Steps and traces. J. Log. Comput., 31(6):1482-1525, 2021. Google Scholar
  33. Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Generalizing determinization from automata to coalgebras. Log. Methods Comput. Sci., 9(1), 2013. Google Scholar
  34. David Sprunger, Shin-ya Katsumata, Jérémy Dubut, and Ichiro Hasuo. Fibrational bisimulations and quantitative reasoning. In CMCS, volume 11202 of Lecture Notes in Computer Science, pages 190-213. Springer, 2018. Google Scholar
  35. Ruben Turkenburg, Clemens Kupke, Jurriaan Rot, and Ezra Schoen. Preservation and reflection of bisimilarity via invertible steps. In FoSSaCS, volume 13992 of Lecture Notes in Computer Science, pages 328-348. Springer, 2023. Google Scholar
  36. Glynn Winskel. A compositional proof system on a category of labelled transition systems. Inf. Comput., 87(1/2):2-57, 1990. Google Scholar
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