Document Open Access Logo

(Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras

Authors Barbara König, Christina Mika-Michalski

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2018.37.pdf
  • Filesize: 0.51 MB
  • 17 pages

Document Identifiers

Author Details

Barbara König
  • Universität Duisburg-Essen, Germany
Christina Mika-Michalski
  • Universität Duisburg-Essen, Germany

Funding

Research partially supported by DFG Project BEMEGA.

Cite AsGet BibTex

Barbara König and Christina Mika-Michalski. (Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 37:1-37:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CONCUR.2018.37

Abstract

Behavioural equivalences can be characterized via bisimulations, modal logics and spoiler-defender games. In this paper we review these three perspectives in a coalgebraic setting, which allows us to generalize from the particular branching type of a transition system. We are interested in qualitative notions (classical bisimulation) as well as quantitative notions (bisimulation metrics). Our first contribution is to introduce a spoiler-defender bisimulation game for coalgebras in the classical case. Second, we introduce such games for the metric case and furthermore define a real-valued modal coalgebraic logic, from which we can derive the strategy of the spoiler. For this logic we show a quantitative version of the Hennessy-Milner theorem.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Logic and verification
Keywords
  • coalgebra
  • bisimulation games
  • spoiler-defender games
  • behavioural metrics
  • modal logic

Metrics

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

Related Versions

References

  1. J. Adámek, H.P. Gumm, and V. Trnková. Presentation of Set functors: A coalgebraic perspective. Journal of Logic and Computation, 20(5), 2010. Google Scholar
  2. J. Adámek and J. Rosický. Locally Presentable and Accessible Categories, volume 189 of London Mathematical Society Lecture Note Series. Cambridge University Press, 1994. Google Scholar
  3. R.B. Ash. Real Analysis and Probability. Academic Press, 1972. Google Scholar
  4. A. Balan and A. Kurz. Finitary functors: From Set to Preord and Poset. In Proc. of CALCO '11, pages 85-99. Springer, 2011. LNCS 6859. Google Scholar
  5. P. Baldan, F. Bonchi, H. Kerstan, and B. König. Behavioral metrics via functor lifting. In Proc. of FSTTCS '14, volume 29 of LIPIcs, 2014. Google Scholar
  6. P. Baldan, F. Bonchi, H. Kerstan, and B. König. Coalgebraic behavioral metrics. Logical Methods in Computer Science, to appear. Selected Papers of the 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Google Scholar
  7. A. Baltag. Truth-as-simulation: Towards a coalgebraic perspective on logic and games. Technical Report SEN-R9923, Centrum voor Wiskunde en Informatica (CWI), November 1999. Google Scholar
  8. V. Castiglioni, D. Gebler, and S. Tini. Logical characterization of bisimulation metrics. In Proc. of QAPL '16, 2016. EPTCS 227. Google Scholar
  9. K. Chatzikokolakis, D. Gebler, C. Palamidessi, and L. Xu. Generalized bisimulation metrics. In Proc. of CONCUR '14. Springer, 2014. LNCS/ARCoSS 8704. Google Scholar
  10. D. Chen, F. van Breugel, and J. Worrell. On the complexity of computing probabilistic bisimilarity. In Proc. of FOSSACS '12, pages 437-451. Springer, 2012. LNCS/ARCoSS 7213. Google Scholar
  11. X. Chen and Y. Deng. Game characterizations of process equivalences. In Proc. of APLAS '08, pages 107-121. Springer, 2008. LNCS 5356. Google Scholar
  12. L. de Alfaro, M. Faella, and M. Stoelinga. Linear and branching system metrics. IEEE Trans. Softw. Eng., 35(2):258-273, 2009. Google Scholar
  13. J. Desharnais. Labelled Markov processes. PhD thesis, McGill University, Montreal, November 1999. Google Scholar
  14. J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. Metrics for labelled Markov processes. Theoretical Computer Science, 318:323-354, 2004. Google Scholar
  15. J. Desharnais, F. Laviolette, and M. Tracol. Approximate analysis of probabilistic processes: Logic, simulation and games. In Proc. of QEST '08, pages 264-273. IEEE, 2008. Google Scholar
  16. U. Fahrenberg, A. Legay, and C. Thrane. The quantitative linear-time-branching-time spectrum. In Proc. of FSTTCS '11, volume 13 of LIPIcs, pages 103-114, 2011. Google Scholar
  17. N. Fijalkow, B. Klin, and P. Panangaden. Expressiveness of probabilistic modal logics. In Proc. of ICALP '17, volume 80 of LIPIcs, pages 105:1-12. Schloss Dagstuhl - Leibniz Center for Informatics, 2017. Google Scholar
  18. G. Fontaine, R.A. Leal, and Y. Venema. Automata for coalgebras: An approach using predicate liftings. In Proc. of ICALP '10, pages 381-392. Springer, 2010. LNCS 6198. Google Scholar
  19. D. Gorín and L. Schröder. Simulations and bisimulations for coalgebraic modal logics. In Proc. of CALCO '13, pages 253-266. Springer, 2013. LNCS 8089. Google Scholar
  20. H. Peter Gumm. Universal coalgebras and their logics. AJSE-Mathematics, 34(1D):105-130, 2009. Google Scholar
  21. M. Hennessy and R. Milner. On observing nondeterminism and concurrency. In Proc. of ICALP '80, pages 299-309. Springer, 1980. LNCS 85. Google Scholar
  22. N. Khakpour and M.R. Mousavi. Notions of conformance testing for cyber-physical systems: Overview and roadmap (invited paper). In Proc. of CONCUR '15, volume 42. LIPIcs, 2015. Google Scholar
  23. B. König and C. Mika-Michalski. (Metric) bisimulation games and real-valued modal logics for coalgebras, 2018. arXiv:1705.10165. URL: http://arxiv.org/abs/1705.10165.
  24. C. Kupke. Terminal sequence induction via games (international tbilisi symposium on language, logic and computation). In Prof. of TbiLLC '07, pages 257-271. Springer, 2009. LNAI 5422. Google Scholar
  25. L.S. Moss. Coalgebraic logic. Annals of Pure and Applied Logic, 96(1-3):277-317, 1999. Google Scholar
  26. M. Otto. Elementary proof of the van Benthem-Rosen characterisation theorem. Technical Report 2342, Department of Mathematics, Technische Universität Darmstadt, 2004. Google Scholar
  27. D. Pattinson. Coalgebraic modal logic: soundness, completeness and decidability of local consequence. Theoretical Computer Science, 309(1):177-193, 2003. Google Scholar
  28. J.J.M.M. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249:3-80, 2000. Google Scholar
  29. L. Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theoretical Computer Science, 390(2):230-247, 2008. Google Scholar
  30. L. Schröder and D. Pattinson. Description logics and fuzzy probability. In Proc. of IJCAI '11, volume 2, pages 1075-1080. AAAI Press, 2011. Google Scholar
  31. S. Staton. Relating coalgebraic notions of bisimulation. In Proc. of CALCO '09, pages 191-205. Springer, 2009. LNCS 5728. Google Scholar
  32. C. Stirling. Bisimulation, modal logic and model checking games. Logic Journal of the IGPL, 7(1):103-124, 1999. Google Scholar
  33. D. Turi and J. Rutten. On the foundations of final coalgebra semantics: non-well-founded sets, partial orders, metric spaces. Mathematical Structures in Computer Science, 8:481-540, 1998. Google Scholar
  34. F. van Breugel and J. Worrell. Approximating and computing behavioural distances in probabilistic transition systems. Theoretical Computer Science, 360:373-385, 2005. Google Scholar
  35. F. van Breugel and J. Worrell. A behavioural pseudometric for probabilistic transition systems. Theoretical Computer Science, 331(1):115-142, 2005. Google Scholar
  36. C. Villani. Optimal Transport - Old and New, volume 338 of A Series of Comprehensive Studies in Mathematics. Springer, 2009. Google Scholar
  37. P. Wild, L. Schröder, D. Pattinson, and B. König. A van Benthem theorem for fuzzy modal logic. In Proc. of LICS '18, 2018. to appear. URL: http://arxiv.org/abs/1802.00478.
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