Document Open Access Logo

Bisimulation for Weakly Expressive Coalgebraic Modal Logics

Authors Zeinab Bakhtiari, Helle Hvid Hansen

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2017.4.pdf
  • Filesize: 0.49 MB
  • 16 pages

Document Identifiers

Author Details

Zeinab Bakhtiari
Helle Hvid Hansen

Cite AsGet BibTex

Zeinab Bakhtiari and Helle Hvid Hansen. Bisimulation for Weakly Expressive Coalgebraic Modal Logics. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 4:1-4:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CALCO.2017.4

Abstract

Research on the expressiveness of coalgebraic modal logics with respect to semantic equivalence notions has so far focused mainly on finding logics that are able to distinguish states that are not behaviourally equivalent (such logics are said to be expressive). In other words, the notion of behavioural equivalence is taken as the starting point, and the expressiveness of the logic is evaluated against it. However, for some applications, modal logics that are not expressive are of independent interest. Such an example is given by contingency logic. We can now turn the question of expressiveness around and ask, given a modal logic, what is a suitable notion of semantic equivalence? In this paper, we propose a notion of \Lambda-bisimulation which is parametric in a collection \Lambda of predicate liftings. We study the basic properties of \Lambda-bisimilarity, and prove as our main result a Hennessy-Milner style theorem, which shows that (for finitary functors) \Lambda-bisimilarity exactly matches the expressiveness of the coalgebraic modal logic arising from \Lambda.
Keywords
  • Coalgebraic modal logic
  • bisimulation
  • expressiveness
  • Hennessy-Milner theorem

Metrics

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

References

  1. J. Adámek and H. Porst. From varieties of algebras to covarieties of coalgebras. In CMCS 2000, volume 44 of Electr. Notes in Theor. Comp. Sci., pages 27-46. Elsevier, 2001. Google Scholar
  2. Z. Bakhtiari, H. van Ditmarsch, and H.H. Hansen. Neighbourhood contingency bisimulation. In ICLA 2017, volume 10119 of LNCS, pages 48-63. Springer, 2017. Google Scholar
  3. M. Bílková and M. Dostál. Expressivity of many-valued modal logics, coalgebraically. In WoLLIC 2016, volume 9803 of LNCS, pages 109-124. Springer, 2016. Google Scholar
  4. S. Enqvist. Homomorphisms of coalgebras from predicate liftings. In CALCO 2013, volume 8089 of LNCS, pages 126-140. Springer, 2013. Google Scholar
  5. J. Fan and H. van Ditmarsch. Neighborhood contingency logic. In ICLA 2015, volume 8923 of LNCS, pages 88-99. Springer, 2015. Google Scholar
  6. J. Fan, Y. Wang, and H. van Ditmarsch. Almost necessary. In AiML 2014, pages 178-196. College Publications, 2014. Google Scholar
  7. D. Gorín and L. Schröder. Simulations and bisimulations for coalgebraic modal logics. In CALCO 2013, volume 8089 of LNCS, pages 253-266. Springer, 2013. Google Scholar
  8. H.H. Hansen, C. Kupke, and E. Pacuit. Neighbourhood structures: Bisimilarity and basic model theory. Logical Methods in Computer Science, 5(2:2), 2009. Google Scholar
  9. M. Hennessy and R. Milner. Algebraic laws for non-determinism and concurrency. Journal of the ACM, 32:137-161, 1985. Google Scholar
  10. B. Jacobs and A. Sokolova. Exemplaric expressivity of modal logics. Journal of logic and computation, 20(5):1041-1068, 2010. Google Scholar
  11. B. Klin. Coalgebraic modal logic beyond sets. Electronic Notes in Theoretical Computer Science, 173:177-201, 2007. Google Scholar
  12. C. Kupke and R.A. Leal. Characterising behavioural equivalence: Three sides of one coin. In CALCO 2009, volume 5728 of LNCS, pages 97-112. Springer, 2009. Google Scholar
  13. C. Kupke and D. Pattinson. Coalgebraic semantics of modal logics: an overview. Theoretical Computer Science, 412(38):5070-5094, 2011. Google Scholar
  14. A. Kurz. Logics for coalgebras and applications to computer science. PhD thesis, Ludwig-Maximilians-Universität München, 2000. Google Scholar
  15. P.B. Levy. Similarity quotients as final coalgebras. In FoSSaCS 2011, volume 6604 of LNCS, pages 27-41. Springer, 2011. Google Scholar
  16. T. Litak, D. Pattinson, K. Sano, and L. Schröder. Coalgebraic predicate logic. In ICALP 2012, volume 7392 of LNCS, pages 299-311. Springer, 2012. Google Scholar
  17. S. Mac Lane. Categories for the working mathematician, volume 5. Springer Science &Business Media, 2013. Google Scholar
  18. J. Marti and Y. Venema. Lax extensions of coalgebra functors and their logic. Journal of Computer and System Sciences, 81(5):880-900, 2015. Google Scholar
  19. H. Montgomery and R. Routley. Contingency and non-contingency bases for normal modal logics. Logique et Analyse, 9:318-328, 1966. Google Scholar
  20. L. Moss and I. Viglizzo. Harsanyi type spaces and final coalgebras constructed from satisfied theories. In CMCS 2004, volume 106 of Electr. Notes in Theor. Comp. Sci., pages 279-295. Elsevier, 2004. Google Scholar
  21. D. Pattinson. Coalgebraic modal logic: Soundness, completeness and decidability of local consequence. Theoretical Computer Science, 309(1-3):177-193, 2003. Google Scholar
  22. D. Pattinson et al. Expressive logics for coalgebras via terminal sequence induction. Notre Dame Journal of Formal Logic, 45(1):19-33, 2004. Google Scholar
  23. J.J.M.M. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249(1):3-80, 2000. Google Scholar
  24. L. Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theoretical Computer Science, 390:230-247, 2008. Google Scholar
  25. J. van Benthem, N. Bezhanishvili, S. Enqvist, and J. Yu. Instantial neighbourhood logic. Review of Symbolic Logic, 10(1):116-144, 2017. 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