Document Open Access Logo

Monads and Quantitative Equational Theories for Nondeterminism and Probability

Authors Matteo Mio, Valeria Vignudelli

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.28.pdf
  • Filesize: 0.64 MB
  • 18 pages

Document Identifiers

Author Details

Matteo Mio
  • Université Lyon, CNRS, ENS Lyon, UCB Lyon 1, LIP, France
Valeria Vignudelli
  • Université Lyon, CNRS, ENS Lyon, UCB Lyon 1, LIP, France

Funding

Both authors have been partially supported by the French project ANR-16-CE25-0011 REPAS. Vignudelli has been partially supported by the European Research Council (ERC) under the European Union’s Horizon 2020 programme (CoVeCe, grant agreement No 678157) and by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007) operated by the French National Research Agency (ANR).

Acknowledgements

The authors are grateful to the anonymous reviewers and to the authors of [Giorgio Bacci et al., 2018] for their useful comments and suggestions.

Cite AsGet BibTex

Matteo Mio and Valeria Vignudelli. Monads and Quantitative Equational Theories for Nondeterminism and Probability. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CONCUR.2020.28

Abstract

The monad of convex sets of probability distributions is a well-known tool for modelling the combination of nondeterministic and probabilistic computational effects. In this work we lift this monad from the category of sets to the category of extended metric spaces, by means of the Hausdorff and Kantorovich metric liftings. Our main result is the presentation of this lifted monad in terms of the quantitative equational theory of convex semilattices, using the framework of quantitative algebras recently introduced by Mardare, Panangaden and Plotkin.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Axiomatic semantics
  • Theory of computation → Categorical semantics
Keywords
  • Computational Effects
  • Monads
  • Metric Spaces
  • Quantitative Algebras

Metrics

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

References

  1. Suzana Andova. Process algebra with probabilistic choice. In Formal Methods for Real-Time and Probabilistic Systems, 5th International AMAST Workshop, ARTS'99, Bamberg, Germany, May 26-28, 1999. Proceedings, pages 111-129, 1999. URL: https://doi.org/10.1007/3-540-48778-6_7.
  2. Suzana Andova and Sonja Georgievska. On compositionality, efficiency, and applicability of abstraction in probabilistic systems. In Mogens Nielsen, Antonín Kucera, Peter Bro Miltersen, Catuscia Palamidessi, Petr Tuma, and Frank D. Valencia, editors, SOFSEM 2009: Theory and Practice of Computer Science, 35th Conference on Current Trends in Theory and Practice of Computer Science, Spindleruv Mlýn, Czech Republic, January 24-30, 2009. Proceedings, volume 5404 of Lecture Notes in Computer Science, pages 67-78. Springer, 2009. URL: https://doi.org/10.1007/978-3-540-95891-8_10.
  3. Steve Awodey. Category Theory. Oxord University Press, 2010. Google Scholar
  4. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. Complete axiomatization for the total variation distance of Markov chains. In Sam Staton, editor, Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2018, Dalhousie University, Halifax, Canada, June 6-9, 2018, volume 341 of Electronic Notes in Theoretical Computer Science, pages 27-39. Elsevier, 2018. URL: https://doi.org/10.1016/j.entcs.2018.03.014.
  5. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. A complete quantitative deduction system for the bisimilarity distance on Markov chains. Logical Methods in Computer Science, 14(4), 2018. URL: https://doi.org/10.23638/LMCS-14(4:15)2018.
  6. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare, Qiyi Tang, and Franck van Breugel. Computing probabilistic bisimilarity distances for probabilistic automata. In 30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands, pages 9:1-9:17, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.9.
  7. Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. An algebraic theory of Markov Processes. 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 679-688. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209177.
  8. 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.
  9. E. Bandini and R. Segala. Axiomatizations for probabilistic bisimulation. In Proc. of the 28th Int. Coll. on Automata, Languages and Programming (ICALP 2001), volume 2076 of LNCS, pages 370-381. Springer, 2001. Google Scholar
  10. Filippo Bonchi, Barbara König, and Daniela Petrisan. Up-to techniques for behavioural metrics via fibrations. In 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, pages 17:1-17:17, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.17.
  11. 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.
  12. Filippo Bonchi, Alexandra Silva, and Ana Sokolova. The Power of Convex Algebras. In CONCUR 2017, volume 85, pages 23:1-23:18. LIPIcs, 2017. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.23.
  13. Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. The theory of traces for systems with nondeterminism and probability. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-14, 2019. URL: https://doi.org/10.1109/LICS.2019.8785673.
  14. Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. Presenting convex sets of probability distributions by convex semilattices and unique bases, 2020. URL: http://arxiv.org/abs/2005.01670.
  15. Franck van Breugel. The metric monad for probabilistic nondeterminism. http://www.cse.yorku.ca/~franck/research/drafts/monad.pdf, 2005.
  16. Franck van Breugel and James Worrell. Towards quantitative verification of probabilistic transition systems. In Fernando Orejas, Paul G. Spirakis, and Jan van Leeuwen, editors, Automata, Languages and Programming, 28th International Colloquium, ICALP 2001, Crete, Greece, July 8-12, 2001, Proceedings, volume 2076 of Lecture Notes in Computer Science, pages 421-432. Springer, 2001. URL: https://doi.org/10.1007/3-540-48224-5_35.
  17. Stanley Burris and H. P. Sankappanavar. A Course in Universal Algebra. Springer-Verlag Graduate Texts in Mathematics, 1981. Google Scholar
  18. Valentina Castiglioni. Trace and testing metrics on nondeterministic probabilistic processes. In Proc. Express/SOS 2018., pages 19-36, 2018. URL: https://doi.org/10.4204/EPTCS.276.4.
  19. Konstantinos Chatzikokolakis, Catuscia Palamidessi, and Valeria Vignudelli. Up-to techniques for generalized bisimulation metrics. In 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada, pages 35:1-35:14, 2016. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2016.35.
  20. Pedro R. D'Argenio, Daniel Gebler, and Matias David Lee. Axiomatizing bisimulation equivalences and metrics from probabilistic SOS rules. In Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, pages 289-303, 2014. URL: https://doi.org/10.1007/978-3-642-54830-7_19.
  21. Y. Deng and C. Palamidessi. Axiomatizations for probabilistic finite-state behaviors. Theoretical Computer Science, 373:92-114, 2007. Google Scholar
  22. Yuxin Deng, Tom Chothia, Catuscia Palamidessi, and Jun Pang. Metrics for action-labelled quantitative transition systems. Electron. Notes Theor. Comput. Sci., 153(2):79-96, 2006. URL: https://doi.org/10.1016/j.entcs.2005.10.033.
  23. Josee Desharnais, Radha Jagadeesan, Vineet Gupta, and Prakash Panangaden. The metric analogue of weak bisimulation for probabilistic processes. In Proc. LICS'02, pages 413-422. IEEE Computer Society, 2002. URL: https://doi.org/10.1109/LICS.2002.1029849.
  24. E. Doberkat. Eilenberg-moore algebras for stochastic relations. Information and Computation, 204(12):1756-1781, 2006. Erratum and Addendum: Eilenberg-Moore algebras for stochastic relations. Information and Computation, Volume 206, Issue 12, December 2008, Pages 1476-1484. Google Scholar
  25. Daniel Gebler, Kim G. Larsen, and Simone Tini. Compositional bisimulation metric reasoning with probabilistic process calculi. Logical Methods in Computer Science, 12(4), 2016. URL: https://doi.org/10.2168/LMCS-12(4:12)2016.
  26. Daniel Gebler and Simone Tini. SOS specifications for uniformly continuous operators. J. Comput. Syst. Sci., 92:113-151, 2018. URL: https://doi.org/10.1016/j.jcss.2017.09.011.
  27. A. Giacalone, C.-C. Jou, and S.A. Smolka. Algebraic reasoning for probabilistic concurrent systems. In Proc. PROCOMET'90), pages 443-458. North-Holland, 1990. Google Scholar
  28. Jean Goubault-Larrecq. Continuous previsions. In Jacques Duparc and Thomas A. Henzinger, editors, Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings, volume 4646 of Lecture Notes in Computer Science, pages 542-557. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74915-8_40.
  29. Jean Goubault-Larrecq. Prevision domains and convex powercones. In Roberto M. Amadio, editor, Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29 - April 6, 2008. Proceedings, volume 4962 of Lecture Notes in Computer Science, pages 318-333. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78499-9_23.
  30. Alexandre Goy and Daniela Petrisan. Combining probabilistic and non-deterministic choice via weak distributive laws. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 454-464. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394795.
  31. Felix Hausdorff. Grundzuge der mengenlehre. German. Veit und Co. (cit. page 5), 1914. Google Scholar
  32. B. Jacobs. Convexity, duality and effects. In Theoretical computer science, volume 323 of IFIP Adv. Inf. Commun. Technol., pages 1-19. Springer, Berlin, 2010. URL: https://doi.org/10.1007/978-3-642-15240-5_1.
  33. Bart Jacobs. Coalgebraic trace semantics for combined possibilitistic and probabilistic systems. Electr. Notes Theor. Comput. Sci., 203(5):131-152, 2008. Google Scholar
  34. Alexander Kechris. Classical Descriptive Set Theory. Springer-Verlag, 1995. Google Scholar
  35. Bartek Klin. Bialgebras for structural operational semantics: An introduction. Theor. Comput. Sci., 412(38):5043-5069, 2011. URL: https://doi.org/10.1016/j.tcs.2011.03.023.
  36. Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. Quantitative algebraic reasoning. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 700-709. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934518.
  37. Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. On the axiomatizability of quantitative algebras. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005102.
  38. Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. Free complete Wasserstein algebras. Logical Methods in Computer Science, 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:19)2018.
  39. Matteo Mio. Upper-expectation bisimilarity and łukasiewicz μ-calculus. In Anca Muscholl, editor, Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8412 of Lecture Notes in Computer Science, pages 335-350. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54830-7_22.
  40. M. Mislove, J. Ouaknine, and J. Worrell. Axioms for probability and nondeterminism. In Proc. of the 10th Int. Workshop on Expressiveness in Concurrency (EXPRESS 2003), volume 96 of ENTCS, pages 7-28. Elsevier, 2003. Google Scholar
  41. Michael W. Mislove. Nondeterminism and probabilistic choice: Obeying the laws. In CONCUR 2000, pages 350-364. LNCS 1877, 2000. URL: https://doi.org/10.1007/3-540-44618-4_26.
  42. Michael W. Mislove. On combining probability and nondeterminism. Electron. Notes Theor. Comput. Sci., 162:261-265, 2006. URL: https://doi.org/10.1016/j.entcs.2005.12.113.
  43. Eugenio Moggi. Computational lambda-calculus and monads. In Fourth Annual IEEE Symposium on Logic in Computer Science, pages 14-23, 1989. Google Scholar
  44. Eugenio Moggi. Notions of computation and monads. Information and Computation, 93(1):55-92, 1991. Google Scholar
  45. Prakash Panangaden. Labelled Markov Processes. Imperial College Press, 2009. Google Scholar
  46. R. Segala. Modeling and verification of randomized distributed real-time systems. PhD thesis, MIT, 1995. Google Scholar
  47. M.H. Stone. Postulates for the barycentric calculus. Ann. Mat. Pura Appl. (4), 29:25-30, 1949. URL: https://doi.org/10.1007/BF02413910.
  48. T. Świrszcz. Monadic functors and convexity. Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys., 22:39-42, 1974. Google Scholar
  49. Qiyi Tang and Franck van Breugel. Deciding probabilistic bisimilarity distance one for probabilistic automata. In 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, pages 9:1-9:17, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.9.
  50. Regina Tix, Klaus Keimel, and Gordon D. Plotkin. Semantic domains for combining probability and non-determinism. Electron. Notes Theor. Comput. Sci., 222:3-99, 2009. URL: https://doi.org/10.1016/j.entcs.2009.01.002.
  51. Daniele Turi and Gordon D. Plotkin. Towards a mathematical operational semantics. In Proc. LICS 1997, pages 280-291, 1997. URL: https://doi.org/10.1109/LICS.1997.614955.
  52. D. Varacca and G. Winskel. Distributing probability over non-determinism. Mathematical Structures in Computer Science, 16:87-113, 2006. 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