Document Open Access Logo

Characteristic Logics for Behavioural Metrics via Fuzzy Lax Extensions

Authors Paul Wild, Lutz Schröder

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.27.pdf
  • Filesize: 0.56 MB
  • 23 pages

Document Identifiers

Author Details

Paul Wild
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Lutz Schröder
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Funding

Work forms part of the DFG project Probabilistic description logics as a fragment of probabilistic first-order logic (SCHR 1118/6-2).

Cite AsGet BibTex

Paul Wild and Lutz Schröder. Characteristic Logics for Behavioural Metrics via Fuzzy Lax Extensions. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 27:1-27:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CONCUR.2020.27

Abstract

Behavioural distances provide a fine-grained measure of equivalence in systems involving quantitative data, such as probabilistic, fuzzy, or metric systems. Like in the classical setting of crisp bisimulation-type equivalences, the wide variation found in system types creates a need for generic methods that apply to many system types at once. Approaches of this kind are emerging within the paradigm of universal coalgebra, based either on lifting pseudometrics along set functors or on lifting general real-valued (fuzzy) relations along functors by means of fuzzy lax extensions. An immediate benefit of the latter is that they allow bounding behavioural distance by means of fuzzy bisimulations that need not themselves be (pseudo-)metrics, in analogy to classical bisimulations (which need not be equivalence relations). The known instances of generic pseudometric liftings, specifically the generic Kantorovich and Wasserstein liftings, both can be extended to yield fuzzy lax extensions, using the fact that both are effectively given by a choice of quantitative modalities. Our central result then shows that in fact all fuzzy lax extensions are Kantorovich extensions for a suitable set of quantitative modalities, the so-called Moss modalities. For non-expansive fuzzy lax extensions, this allows for the extraction of quantitative modal logics that characterize behavioural distance, i.e. satisfy a quantitative version of the Hennessy-Milner theorem; equivalently, we obtain expressiveness of a quantitative version of Moss' coalgebraic logic.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • Modal logic
  • behavioural distance
  • coalgebra
  • bisimulation
  • lax extension

Metrics

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

Related Versions

References

  1. Jiří Adámek, Horst Herrlich, and George Strecker. Abstract and Concrete Categories. Wiley Interscience, 1990. Available as Reprints Theory Appl. Cat. 17 (2006), pp. 1-507. Google Scholar
  2. Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Coalgebraic Behavioral Metrics. Logical Methods in Computer Science, Volume 14, Issue 3, September 2018. URL: https://doi.org/10.23638/LMCS-14(3:20)2018.
  3. Borja Balle, Pascale Gourdeau, and Prakash Panangaden. Bisimulation metrics for weighted automata. In International Colloquium on Automata, Languages, and Programming, ICALP 2017, volume 80 of LIPIcs, pages 103:1-103:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.103.
  4. Michael Barr. Relational algebras. In Proc. Midwest Category Seminar, volume 137 of LNM. Springer, 1970. Google Scholar
  5. Michael Barr. Terminal coalgebras in well-founded set theory. Theoret. Comput. Sci., 114:299-315, 1993. Google Scholar
  6. Filippo Bonchi, Alexandra Silva, and Ana Sokolova. The power of convex algebras. In Concurrency Theory, CONCUR 2017, volume 85 of LIPIcs, pages 23:1-23:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.23.
  7. Yongzhi Cao, Sherry Sun, Huaiqing Wang, and Guoqing Chen. A behavioral distance for fuzzy-transition systems. IEEE Trans. Fuzzy Systems, 21(4):735-747, 2013. URL: https://doi.org/10.1109/TFUZZ.2012.2230177.
  8. Valentina Castiglioni, Daniel Gebler, and Simone Tini. Logical characterization of bisimulation metrics. In Quantitative Aspects of Programming Languages and Systems, QAPL 2016, volume 227 of EPTCS, pages 44-62, 2016. URL: https://doi.org/10.4204/EPTCS.227.
  9. Konstantinos Chatzikokolakis, Daniel Gebler, Catuscia Palamidessi, and Lili Xu. Generalized bisimulation metrics. In Concurrency Theory, CONCUR 2014, volume 8704 of LNCS, pages 32-46. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44584-6.
  10. Petr Cintula, Carles Noguera, and Jonas Rogger. From Kripke to neighborhood semantics for modal fuzzy logics. In Information Processing and Management of Uncertainty in Knowledge-Based Systems, IPMU 2016, volume 611 of CCIS, pages 95-107. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-40581-0_9.
  11. Corina Cîrstea, Alexander Kurz, Dirk Pattinson, Lutz Schröder, and Yde Venema. Modal logics are coalgebraic. Comput. J., 54:31-41, 2011. URL: https://doi.org/10.1093/comjnl/bxp004.
  12. Luca de Alfaro, Marco Faella, and Mariëlle Stoelinga. Linear and branching system metrics. IEEE Trans. Software Eng., 35(2):258-273, 2009. URL: https://doi.org/10.1109/TSE.2008.106.
  13. Yuxin Deng, Tom Chothia, Catuscia Palamidessi, and Jun Pang. Metrics for action-labelled quantitative transition systems. In Quantitative Aspects of Programming Languages, QAPL 2005, volume 153 of ENTCS, pages 79-96. Elsevier, 2006. URL: https://doi.org/10.1016/j.entcs.2005.10.033.
  14. Josée Desharnais. Labelled Markov processes. PhD thesis, McGill University, Montreal, November 1999. Google Scholar
  15. Josee Desharnais, Abbas Edalat, and Prakash Panangaden. A logical characterization of bisimulation for labeled Markov processes. In Logic in Computer Science, LICS 1998, pages 478-487. IEEE Computer Society, 1998. Google Scholar
  16. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled Markov processes. Theor. Comput. Sci., 318:323-354, 2004. Google Scholar
  17. Wenjie Du, Yuxin Deng, and Daniel Gebler. Behavioural pseudometrics for nondeterministic probabilistic systems. In Dependable Software Engineering: Theories, Tools, and Applications, SETTA 2016, volume 9984 of LNCS, pages 67-84. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-47677-3.
  18. Pantelis Eleftheriou, Costas Koutras, and Christos Nomikos. Notions of bisimulation for Heyting-valued modal languages. J. Log. Comput., 22(2):213-235, 2012. Google Scholar
  19. Uli Fahrenberg and Axel Legay. The quantitative linear-time-branching-time spectrum. Theor. Comput. Sci., 538:54-69, 2014. URL: https://doi.org/10.1016/j.tcs.2013.07.030.
  20. Uli Fahrenberg, Axel Legay, and Claus Thrane. The quantitative linear-time-branching-time spectrum. In Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2011, volume 13 of LIPIcs, pages 103-114. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2011.103.
  21. T. Fan. Fuzzy bisimulation for Gödel modal logic. IEEE Trans. Fuzzy Sys., 23:2387-2396, December 2015. URL: https://doi.org/10.1109/TFUZZ.2015.2426724.
  22. Norm Ferns, Prakash Panangaden, and Doina Precup. Metrics for finite Markov decision processes. In Uncertainty in Artificial Intelligence, UAI 2004, pages 162-169. AUAI Press, 2004. Google Scholar
  23. Melvin Fitting. Many-valued modal logics. Fundam. Inform., 15:235-254, 1991. Google Scholar
  24. Francesco Gavazzo. Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances. In Logic in Computer Science, LICS 2018, pages 452-461. ACM, 2018. URL: https://doi.org/10.1145/3209108.
  25. Alessandro Giacalone, Chi-Chang Jou, and Scott Smolka. Algebraic reasoning for probabilistic concurrent systems. In Programming concepts and methods, PCM 1990, pages 443-458. North-Holland, 1990. Google Scholar
  26. Dirk Hofmann. Topological theories and closed objects. Adv. Math., 215(2):789-824, 2007. URL: https://doi.org/10.1016/j.aim.2007.04.013.
  27. Dirk Hofmann, Gavin Seal, and Walter Tholen, editors. Monoidal Topology: A Categorical Approach to Order, Metric, and Topology. Cambridge University Press, 2014. Google Scholar
  28. 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.
  29. Michael Huth and Marta Kwiatkowska. Quantitative analysis and model checking. In Logic in Computer Science, LICS 1997, pages 111-122. IEEE, 1997. Google Scholar
  30. Narges Khakpour and Mohammad Mousavi. Notions of conformance testing for cyber-physical systems: Overview and roadmap (invited paper). In Concurrency Theory, CONCUR 2015, volume 42 of LIPIcs, pages 18-40. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2015.18.
  31. Barbara König and Christina Mika-Michalski. (Metric) bisimulation games and real-valued modal logics for coalgebras. In Sven Schewe and Lijun Zhang, editors, Concurrency Theory, CONCUR 2018, volume 118 of LIPIcs, pages 37:1-37:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.37.
  32. Alexander Kurz and Raul Leal. Equational coalgebraic logic. In Mathematical Foundations of Programming Semantics, MFPS 2009, volume 249 of ENTCS, pages 333-356. Elsevier, 2009. Google Scholar
  33. Paul Levy. Similarity quotients as final coalgebras. In Foundations of Software Science and Computational Structures, FOSSACS 2011, volume 6604 of LNCS, pages 27-41. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-19805-2.
  34. Thomas Lukasiewicz and Umberto Straccia. Managing uncertainty and vagueness in description logics for the semantic web. J. Web Sem., 6(4):291-308, 2008. URL: https://doi.org/10.1016/j.websem.2008.04.001.
  35. Johannes Marti and Yde Venema. Lax extensions of coalgebra functors and their logic. J. Comput. Syst. Sci., 81(5):880-900, 2015. Google Scholar
  36. Stefan Milius, Dirk Pattinson, and Lutz Schröder. Generic trace semantics and graded monads. In Algebra and Coalgebra in Computer Science, CALCO 2015, Leibniz International Proceedings in Informatics, 2015. Google Scholar
  37. Robin Milner. Communication and Concurrency. Prentice Hall, 1989. Google Scholar
  38. Matteo Mio and Alex Simpson. Łukasiewicz μ-calculus. Fund. Inf., 150(3-4):317-346, 2017. Google Scholar
  39. Matteo Mio and Valeria Vignudelli. Monads and quantitative equational theories for nondeterminism and probability, 2020. This volume; full version available as arXiv e-print https://arxiv.org/abs/2005.07509. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.28.
  40. Carroll Morgan and Annabelle McIver. A probabilistic temporal calculus based on expectations. In Lindsay Groves and Steve Reeves, editors, Formal Methods Pacific, FMP 1997. Springer, 1997. Google Scholar
  41. Charles Morgan. Local and global operators and many-valued modal logics. Notre Dame J. Formal Log., 20:401-411, 1979. Google Scholar
  42. Lawrence Moss. Coalgebraic logic. Ann. Pure Appl. Logic, 96:277-317, 1999. Google Scholar
  43. David Park. Concurrency and automata on infinite sequences. In Theoretical Computer Science, 5th GI-Conference, volume 104 of LNCS, pages 167-183. Springer, 1981. URL: https://doi.org/10.1007/BFb0017288.
  44. Dirk Pattinson. Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Log., 45:19-33, 2004. Google Scholar
  45. Ricardo Rodriguez and Lluis Godo. Modal uncertainty logics with fuzzy neighborhood semantics. In Weighted Logics for Artiticial Intelligence, WL4AI 2013 (Workshop at IJCAI 2013), pages 79-86, 2013. Google Scholar
  46. Jan Rutten. Universal coalgebra: A theory of systems. Theoret. Comput. Sci., 249:3-80, 2000. Google Scholar
  47. Lutz Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theoret. Comput. Sci., 390:230-247, 2008. Google Scholar
  48. Lutz Schröder and Dirk Pattinson. Description logics and fuzzy probability. In Toby Walsh, editor, Int. Joint Conf. Artificial Intelligence, IJCAI 2011, pages 1075-1081. AAAI, 2011. Google Scholar
  49. Umberto Straccia. A fuzzy description logic. In Artificial Intelligence, AAAI 1998, pages 594-599. AAAI Press / MIT Press, 1998. Google Scholar
  50. Albert Thijs. Simulation and fixpoint semantics. PhD thesis, University of Groningen, 1996. Google Scholar
  51. Věra Trnková. General theory of relational automata. Fund. Inform., 3:189-234, 1980. Google Scholar
  52. Franck van Breugel, Claudio Hermida, Michael Makkai, and James Worrell. Recursively defined metric spaces without contraction. Theor. Comput. Sci., 380(1-2):143-163, 2007. URL: https://doi.org/10.1016/j.tcs.2007.02.059.
  53. Franck van Breugel and James Worrell. A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci., 331:115-142, 2005. Google Scholar
  54. Cédric Villani. Optimal Transport: Old and New. Springer, 2008. Google Scholar
  55. Igor Walukiewicz. Completeness of Kozen’s axiomatisation of the propositional μ-calculus. In Logic in Computer Science, LICS 1995, pages 14-24. IEEE Computer Society, 1995. URL: https://doi.org/10.1109/LICS.1995.523240.
  56. Paul Wild and Lutz Schröder. Characteristic logics for behavioural metrics via fuzzy lax extensions, 2020. arXiv e-print. URL: http://arxiv.org/abs/2007.01033.
  57. Paul Wild, Lutz Schröder, Dirk Pattinson, and Barbara König. A van Benthem theorem for fuzzy modal logic. In Logic in Computer Science, LICS 2018, pages 909-918. ACM, 2018. 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