CoChat
Sign Up
Cited by 13Logic, programming, and type systemsFormal Methods in VerificationAdvanced Algebra and Logic

Combining Nondeterminism, Probability, and Termination: Equational and Metric Reasoning

Open access
Mio, Matteo, Sarkis, Ralph, Vignudelli, Valeria·2021·2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
DOI 10.1109/lics52264.2021.9470717
Open this paper in CoChat — free accountOpen PDF

Abstract

We study monads resulting from the combination of nondeterministic and probabilistic behaviour with the possibility of termination, which is essential in program semantics. Our main contributions are presentation results for the monads, providing equational reasoning tools for establishing equivalences and distances of programs.

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

Crossref · 10.1109/lics52264.2021.9470717

Cites

Statistics

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • Interpretability can be maintained if human behaviour is modelled using nondeterminism.

    “However, note that interpretability can be maintained if human behaviour is modelled using nondeterminism.”

    From Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems (2024) · cites this paper as Mio et al., 2021

    The paper’s introduction (p. 1) describes equational reasoning about program behaviour, and its Examples of Applications (p. 10) model nondeterministic choices in process algebra. A search for interpretability and human behaviour found no passage connecting nondeterministic modelling of humans to maintained interpretability. (LLM, conf=0.76)

    Experimental — accuracy not yet measured

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Cites

No references could be resolved yet.

Research works printed but not linked: 44

  1. [1][1] S. Awodey, Category Theory . Oxord University Press, 2010. -
  2. [2][2] G. Bacci, G. Bacci, K. G. Larsen, and R. Mardare, 'Complete axiomatization for the total variation distance of Markov chains,' in Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2018, Dalhousie University, Halifax, Canada, June 6-9, 2018 , ser. Electronic Notes in Theoretical Computer Science, S. Staton, Ed., vol. 341. Elsevier, 2018, pp. 27-39. [Online]. Available: https://doi.org/10.1016/j.entcs.2018.03.014 - · DOI
  3. [3][3] --, 'A complete quantitative deduction system for the bisimilarity distance on Markov chains,' Logical Methods in Computer Science , vol. 14, no. 4, 2018. [Online]. Available: https://doi.org/10.23638/LMCS-14(4:15)2018 - · DOI
  4. [4][4] G. Bacci, R. Mardare, P. Panangaden, and G. D. Plotkin, 'An algebraic theory of Markov Processes,' in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018 , A. Dawar and E. Gr¨ adel, Eds. ACM, 2018, pp. 679-688. [Online]. Available: https://doi.org/10.1145/3209108.3209177 - · DOI
  5. [5][5] P. Baldan, F. Bonchi, H. Kerstan, and B. K¨ onig, 'Behavioral metrics via functor lifting,' in 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, December 15-17, 2014, New Delhi, India , ser. LIPIcs, V. Raman and S. P. Suresh, Eds., vol. 29. Schloss Dagstuhl -LeibnizZentrum f¨ ur Informatik, 2014, pp. 403-415. [Online]. Available: https://doi.org/10.4230/LIPIcs.FSTTCS.2014.403 - · DOI
  6. [6][6] --, 'Coalgebraic behavioral metrics,' Logical Methods in Computer Science , vol. 14, no. 3, 2018. [Online]. Available: https://doi.org/10.23638/LMCS-14(3:20)2018 - · DOI
  7. [7][7] E. Bandini and R. Segala, 'Axiomatizations for probabilistic bisimulation,' in Proc. of the 28th Int. Coll. on Automata, Languages and Programming (ICALP 2001) , ser. LNCS, vol. 2076. Springer, 2001, pp. 370-381. -
  8. [9][9] F. Bartels, 'GSOS for probabilistic transition systems,' in Proc. CMCS '02 , ser. ENTCS, vol. 65, no. 1. Elsevier, 2002, pp. 29-53. -
  9. [10][10] F. Bartels, A. Sokolova, and E. d. Vink, 'A hierarchy of probabilistic system types,' Theoretical Computer Science , vol. 327, pp. 3-22, 2004. -
  10. [11][11] F. Bonchi, B. K¨ onig, and D. Petrisan, 'Up-to techniques for behavioural metrics via fibrations,' in 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China , 2018, pp. 17:1-17:17. [Online]. Available: https://doi.org/10.4230/LIPIcs.CONCUR.2018.17 - · DOI
  11. [12][12] F. Bonchi, D. Petrisan, D. Pous, and J. Rot, 'A general account of coinduction up-to,' Acta Inf. , vol. 54, no. 2, pp. 127-190, 2017. [Online]. Available: https://doi.org/10.1007/s00236-016-0271-4 - · DOI
  12. [13][13] F. Bonchi and A. Santamaria, 'Combining semilattices and semimodules,' 2020, to appear in Proc. FoSSaCs 2021 . [Online]. Available: https://arxiv.org/abs/2012.14778 - · arXiv
  13. [14][14] F. Bonchi, A. Silva, and A. Sokolova, 'The Power of Convex Algebras,' in CONCUR 2017 , vol. 85. LIPIcs, 2017, pp. 23:1-23:18. -
  14. [15][15] F. Bonchi, A. Sokolova, and V. 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 , 2019, pp. 1-14. [Online]. Available: https://doi.org/10.1109/LICS.2019.8785673 - · DOI
  15. [16][16] --, 'Presenting convex sets of probability distributions by convex semilattices and unique bases,' 2020, https://arxiv.org/abs/2005.01670. - · arXiv
  16. [18][18] S. Burris and H. P. Sankappanavar, A Course in Universal Algebra . Springer-Verlag Graduate Texts in Mathematics, 1981. -
  17. [19][19] P. R. D'Argenio, D. Gebler, and M. D. 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 , 2014, pp. 289-303. [Online]. Available: https://doi.org/10.1007/978-3-642-54830-7 19 - · DOI
  18. [20][20] R. De Nicola and M. Hennessy, 'Testing equivalences for processes,' Theoretical Computer Science , vol. 34, pp. 83-133, 1984. -
  19. [21][21] J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden, 'Approximating labelled Markov processes,' Information and Computation , vol. 184, pp. 160-200, 2003. -
  20. [22][22] E. Doberkat, 'Eilenberg-moore algebras for stochastic relations,' Information and Computation , vol. 204, no. 12, pp. 1756-1781, 2006, erratum and Addendum: Eilenberg-Moore algebras for stochastic relations. Information and Computation , Volume 206, Issue 12, December 2008, Pages 1476-1484. -
  21. [23][23] D. Gebler, K. G. Larsen, and S. Tini, 'Compositional bisimulation metric reasoning with probabilistic process calculi,' Logical Methods in Computer Science , vol. 12, no. 4, 2016. [Online]. Available: https://doi.org/10.2168/LMCS-12(4:12)2016 - · DOI
  22. [24][24] J. Goubault-Larrecq, 'Continuous previsions,' in Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings , ser. Lecture Notes in Computer Science, J. Duparc and T. A. Henzinger, Eds., vol. 4646. Springer, 2007, pp. 542-557. [Online]. Available: https://doi.org/10.1007/978-3-540-74915-8 40 - · DOI
  23. [25][25] --, 'Prevision domains and convex powercones,' in 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 , ser. Lecture Notes in Computer Science, R. M. Amadio, Ed., vol. 4962. Springer, 2008, pp. 318-333. [Online]. Available: https://doi.org/10.1007/978-3-540-78499-9 23 - · DOI
  24. [26][26] A. Goy and D. Petrisan, 'Combining probabilistic and non-deterministic choice via weak distributive laws,' in LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbr¨ ucken, Germany, July 8-11, 2020 , H. Hermanns, L. Zhang, N. Kobayashi, and D. Miller, Eds. ACM, 2020, pp. 454-464. [Online]. Available: https://doi.org/10.1145/3373718.3394795 - · DOI
  25. [27][27] B. Jacobs, 'Convexity, duality and effects,' in Theoretical computer science , ser. IFIP Adv. Inf. Commun. Technol. Springer, Berlin, 2010, vol. 323, pp. 1-19. [Online]. Available: http://dx.doi.org/10.1007/978-3-642-15240-5 1 - · DOI
  26. [28][28] --, 'Coalgebraic trace semantics for combined possibilitistic and probabilistic systems,' Electr. Notes Theor. Comput. Sci. , vol. 203, no. 5, pp. 131-152, 2008. -
  27. [29][29] R. Mardare, P. Panangaden, and G. D. Plotkin, 'Quantitative algebraic reasoning,' in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016 , M. Grohe, E. Koskinen, and N. Shankar, Eds. ACM, 2016, pp. 700-709. [Online]. Available: https://doi.org/10.1145/2933575.2934518 - · DOI
  28. [30][30] --, '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 . IEEE Computer Society, 2017, pp. 1-12. [Online]. Available: https://doi.org/10.1109/LICS.2017.8005102 - · DOI
  29. [31][31] --, 'Free complete Wasserstein algebras,' Logical Methods in Computer Science , vol. 14, no. 3, 2018. [Online]. Available: https://doi.org/10.23638/LMCS-14(3:19)2018 - · DOI
  30. [32][32] M. Mio, 'Upper-expectation bisimilarity and łukasiewicz µ -calculus,' 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 , ser. Lecture Notes in Computer Science, A. Muscholl, Ed., vol. 8412. Springer, 2014, pp. 335-350. [Online]. Available: https://doi.org/10.1007/978-3-642-54830-7 22 - · DOI
  31. [33][33] M. Mio and V. Vignudelli, 'Monads and quantitative equational theories for nondeterminism and probability,' in 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference) , ser. LIPIcs, I. Konnov and L. Kov´ acs, Eds., vol. 171. Schloss Dagstuhl -LeibnizZentrum f¨ ur Informatik, 2020, pp. 28:1-28:18. [Online]. Available: https://doi.org/10.4230/LIPIcs.CONCUR.2020.28 - · DOI
  32. [34][34] 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) , ser. ENTCS, vol. 96. Elsevier, 2003, pp. 7-28. -
  33. [35][35] M. W. Mislove, 'Nondeterminism and probabilistic choice: Obeying the laws,' in CONCUR 2000 . LNCS 1877, 2000, pp. 350-364. [Online]. Available: https://doi.org/10.1007/3-540-44618-4 26 - · DOI
  34. [36][36] --, 'On combining probability and nondeterminism,' Electron. Notes Theor. Comput. Sci. , vol. 162, pp. 261-265, 2006. [Online]. Available: https://doi.org/10.1016/j.entcs.2005.12.113 - · DOI
  35. [37][37] E. Moggi, 'Computational lambda-calculus and monads,' in Fourth Annual IEEE Symposium on Logic in Computer Science , 1989, pp. 1423. -
  36. [38][38] --, 'Notions of computation and monads,' Information and Computation , vol. 93, no. 1, pp. 55-92, 1991. -
  37. [39][39] D. Pous and D. Sangiorgi, 'Enhancements of the bisimulation proof method,' in Advanced Topics in Bisimulation and Coinduction , ser. Cambridge Tracts in Theoretical Computer Science, D. Sangiorgi and J. Rutten, Eds. Cambridge University Press, 2011, pp. 233-289. -
  38. [41][41] R. Segala, 'Modeling and verification of randomized distributed realtime systems,' Ph.D. dissertation, MIT, 1995. -
  39. [42][42] A. Sokolova, 'Probabilistic systems coalgebraically: A survey,' Theor. Comput. Sci. , vol. 412, no. 38, pp. 5095-5110, 2011. -
  40. [43][43] A. Sokolova and H. Woracek, 'Termination in convex sets of distributions,' Logical Methods in Computer Science , vol. 14, no. 4, 2018. -
  41. [44][44] M. Stone, 'Postulates for the barycentric calculus,' Ann. Mat. Pura Appl. (4) , vol. 29, pp. 25-30, 1949. [Online]. Available: http://dx.doi.org/10.1007/BF02413910 - · DOI
  42. [45][45] T. ´ Swirszcz, 'Monadic functors and convexity,' Bull. Acad. Polon. Sci. S´ er . Sci. Math. Astronom. Phys. , vol. 22, pp. 39-42, 1974. -
  43. [46][46] R. Tix, K. Keimel, and G. D. Plotkin, 'Semantic domains for combining probability and non-determinism,' Electron. Notes Theor. Comput. Sci. , vol. 222, pp. 3-99, 2009. [Online]. Available: https://doi.org/10.1016/j.entcs.2009.01.002 - · DOI
  44. [47][47] F. van Breugel, B. Sharma, and J. Worrell, 'Approximating a behavioural pseudometric without discount for probabilistic systems,' Log. Methods Comput. Sci. , vol. 4, no. 2, 2008. [Online]. Available: https://doi.org/10.2168/LMCS-4(2:2)2008 · DOI

Cited by

Sorted by citations

Authors
Mio, M., Sarkis, R., & Vignudelli, V.
Affiliations
École Normale Supérieure de Lyon (FR)
ORCID
Venue
2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Publisher
IEEE
Published
2021-06-29
Pages
1-14
ISSN
1043-6871 (ISSN-L)
DOI
10.1109/lics52264.2021.9470717
OpenAlex
W3176572529
Cited by
13
References
0
Citations by year
2026: 1 · 2025: 2 · 2024: 2 · 2023: 3 · 2022: 3 · 2021: 2
FWCI
1.12
Type
conference paper
Language
en
Open access
Licence
Locations
  • ACM/IEEE Symposium on Logic in Computer Science (LICS) (publishedVersion)
  • arXiv (Cornell University) (submittedVersion)
  • HAL (submittedVersion)
  • arXiv (Cornell University)
Funders
Agence Nationale de la Recherche (ANR-20-CE48-0005, ANR-11-IDEX-0007, ANR-10-LABX-0070, ANR-16-CE25-0011)
Topics
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Advanced Algebra and Logic
Keywords
non-determinism, probability, termination, monads, equational reasoning, program semantics, program equivalence

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review