Document Open Access Logo

Denotational Semantics for Probabilistic and Concurrent Programs

Authors Noam Zilberstein , Daniele Gorla , Alexandra Silva

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2025.39.pdf
  • Filesize: 0.97 MB
  • 24 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Parallel computing models
  • Theory of computation → Denotational semantics
  • Theory of computation → Probabilistic computation
Keywords
  • Denotational Semantics
  • Pomsets
  • Concurrency
  • Convex Powerset

Metrics

Abstract

We develop a denotational model for probabilistic and concurrent imperative programs, a class of programs with standard control flow via conditionals and while-loops, as well as probabilistic actions and parallel composition. Whereas semantics for concurrent or randomized programs in isolation is well studied, their combination has not been thoroughly explored and presents unique challenges. The crux of the problem is that interactions between control flow, probabilistic actions, and concurrent execution cannot be captured by straightforward generalizations of prior work on pomsets and convex languages, prominent models for those effects, individually. Our model has good domain theoretic properties, important for semantics of unbounded loops. We also prove two adequacy theorems, showing that the model subsumes typical powerdomain semantics for concurrency and convex powerdomain semantics for probabilistic nondeterminism.

Cite As Get BibTex

Noam Zilberstein, Daniele Gorla, and Alexandra Silva. Denotational Semantics for Probabilistic and Concurrent Programs. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 39:1-39:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CONCUR.2025.39

Author Details

Noam Zilberstein
  • Cornell University, Ithaca, NY, USA
Daniele Gorla
  • Sapienza Università di Roma, Italy
Alexandra Silva
  • Cornell University, Ithaca, NY, USA
  • University College London, UK

Funding

This work was partially supported ARIA’s Safeguarded AI programme.

References

  1. Samson Abramsky and Achim Jung. Domain theory, pages 1-168. Oxford University Press, Inc., USA, 1995. Google Scholar
  2. Krzysztof Apt and Gordon Plotkin. Countable nondeterminism and random assignment. J. ACM, 33(4):724-767, August 1986. URL: https://doi.org/10.1145/6490.6494.
  3. Steve Awodey. Category Theory. Oxford Logic Guides. Ebsco Publishing, 2006. Google Scholar
  4. Ralph-Johan Back. Semantics of unbounded nondeterminism. In Jaco de Bakker and Jan van Leeuwen, editors, Automata, Languages and Programming, pages 51-63, Berlin, Heidelberg, 1980. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-10003-2_59.
  5. Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. An Assertion-Based Program Logic for Probabilistic Programs. In Programming Languages and Systems, pages 117-144, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-89884-1_5.
  6. Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. Presenting Convex Sets of Probability Distributions by Convex Semilattices and Unique Bases. In Fabio Gadducci and Alexandra Silva, editors, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021), volume 211 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1-11:18, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CALCO.2021.11.
  7. Stephen Brookes. Traces, Pomsets, Fairness and Full Abstraction for Communicating Processes. In Luboš Brim, Mojmír Křetínský, Antonín Kučera, and Petr Jančar, editors, CONCUR 2002 - Concurrency Theory, pages 466-482, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-45694-5_31.
  8. Stephen Brookes. A semantics for concurrent separation logic. In Philippa Gardner and Nobuko Yoshida, editors, CONCUR 2004 - Concurrency Theory, pages 16-34, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-28644-8_2.
  9. J. W. de Bakker and J. H. A. Warmerdam. Metric pomset semantics for a concurrent language with recursion. In Irène Guessarian, editor, Semantics of Systems of Concurrent Processes, pages 21-49, Berlin, Heidelberg, 1990. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-53479-2_2.
  10. Jerry den Hartog. Verifying Probabilistic Programs Using a Hoare like Logic. In P. S. Thiagarajan and Roland Yap, editors, Advances in Computing Science - ASIAN'99, pages 113-125, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-46674-6_11.
  11. Edsger W. Dijkstra. Hierarchical ordering of sequential processes. Acta Inf., 1(2):115-138, June 1971. URL: https://doi.org/10.1007/BF00289519.
  12. Luc Edixhoven and Sung-Shik Jongmans. Realisability of Branching Pomsets. In Silvia Lizeth Tapia Tarifa and José Proença, editors, Formal Aspects of Component Software, pages 185-204, Cham, 2022. Springer International Publishing. URL: https://doi.org/10.1007/978-3-031-20872-0_11.
  13. Luc Edixhoven, Sung-Shik Jongmans, José Proença, and Ilaria Castellani. Branching pomsets: Design, expressiveness and applications to choreographies. Journal of Logical and Algebraic Methods in Programming, 136:100919, 2024. URL: https://doi.org/10.1016/j.jlamp.2023.100919.
  14. Luc Edixhoven, Sung-Shik Jongmans, José Proença, and Guillermina Cledou. Branching Pomsets for Choreographies. Electronic Proceedings in Theoretical Computer Science, 365:37-52, August 2022. URL: https://doi.org/10.4204/eptcs.365.3.
  15. Ira Fesefeldt, Joost-Pieter Katoen, and Thomas Noll. Towards Concurrent Quantitative Separation Logic. In Bartek Klin, Sławomir Lasota, and Anca Muscholl, editors, 33rd International Conference on Concurrency Theory (CONCUR 2022), volume 243 of Leibniz International Proceedings in Informatics (LIPIcs), pages 25:1-25:24, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.25.
  16. Robert W. Floyd. Assigning Meanings to Programs. In Mathematical Aspects of Computer Science, volume 19 of Proceedings of Symposia in Applied Mathematics, pages 19-32, Providence, Rhode Island, 1967. American Mathematical Society. URL: https://doi.org/10.1007/978-94-011-1793-7_4.
  17. Jay L. Gischer. The equational theory of pomsets. Theoretical Computer Science, 61(2):199-224, 1988. URL: https://doi.org/10.1016/0304-3975(88)90124-7.
  18. Jan Grabowski. On Partial Languages. Fundamenta Informaticae, 4(2):427-498, 1981. URL: https://doi.org/10.3233/fi-1981-4210.
  19. Sergiu Hart, Micha Sharir, and Amir Pnueli. Termination of probabilistic concurrent program. ACM Trans. Program. Lang. Syst., 5(3):356-380, July 1983. URL: https://doi.org/10.1145/2166.357214.
  20. Jifeng He, Karen Seidel, and Annabelle McIver. Probabilistic models for the guarded command language. Science of Computer Programming, 28(2):171-192, 1997. Formal Specifications: Foundations, Methods, Tools and Applications. URL: https://doi.org/10.1016/S0167-6423(96)00019-6.
  21. Charles Antony Richard Hoare. An Axiomatic Basis for Computer Programming. Commun. ACM, 12(10):576-580, October 1969. URL: https://doi.org/10.1145/363235.363259.
  22. Tony Hoare, Bernhard Möller, Georg Struth, and Ian Wehrman. Concurrent Kleene Algebra and its Foundations. J. Log. Algebraic Methods Program., 80(6):266-296, 2011. URL: https://doi.org/10.1016/J.JLAP.2011.04.005.
  23. Bart Jacobs. Coalgebraic trace semantics for combined possibilitistic and probabilistic systems. Electronic Notes in Theoretical Computer Science, 203(5):131-152, 2008. Proceedings of the Ninth Workshop on Coalgebraic Methods in Computer Science (CMCS 2008). URL: https://doi.org/10.1016/j.entcs.2008.05.023.
  24. Bart Jacobs. From Multisets over Distributions to Distributions over Multisets. In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '21, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1109/LICS52264.2021.9470678.
  25. Radha Jagadeesan, Alan Jeffrey, and James Riely. Pomsets with preconditions: a simple model of relaxed memory. Proc. ACM Program. Lang., 4(Oopsla), November 2020. URL: https://doi.org/10.1145/3428262.
  26. Peter Jipsen and M. Andrew Moshier. Concurrent Kleene algebra with tests and branching automata. Journal of Logical and Algebraic Methods in Programming, 85(4):637-652, 2016. Relational and algebraic methods in computer science. URL: https://doi.org/10.1016/j.jlamp.2015.12.005.
  27. Tobias Kappé, Paul Brunet, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi. Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness, pages 381-400. Springer International Publishing, 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_20.
  28. Joost-Pieter Katoen. Quantitative and Qualitative Extensions of Event Structures. Phd thesis - research ut, graduation ut, University of Twente, Netherlands, 1996. URL: https://doi.org/10.3990/1.9789036507998.
  29. Ryan Kavanagh and Stephen Brookes. A Denotational Semantics for SPARC TSO. Electronic Notes in Theoretical Computer Science, 336:223-239, 2018. The Thirty-third Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIII). URL: https://doi.org/10.1016/j.entcs.2018.03.025.
  30. Klaus Keimel and Gordon Plotkin. Mixed powerdomains for probability and nondeterminism. Logical Methods in Computer Science, Volume 13, Issue 1, January 2017. URL: https://doi.org/10.23638/LMCS-13(1:2)2017.
  31. Dexter Kozen. Semantics of probabilistic programs. In 20th Annual Symposium on Foundations of Computer Science (SFCS '79), pages 101-114, 1979. URL: https://doi.org/10.1109/SFCS.1979.38.
  32. Dexter Kozen and Alexandra Silva. Multisets and distributions. In Venanzio Capretta, Robbert Krebbers, and Freek Wiedijk, editors, Logics and Type Systems in Theory and Practice: Essays Dedicated to Herman Geuvers on The Occasion of His 60th Birthday, pages 168-187, Cham, 2024. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-61716-4_11.
  33. L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, SE-3(2):125-143, 1977. URL: https://doi.org/10.1109/TSE.1977.229904.
  34. Michael R. Laurence and Georg Struth. Completeness Theorems for Bi-Kleene Algebras and Series-Parallel Rational Pomset Languages. In Peter Höfner, Peter Jipsen, Wolfram Kahl, and Martin Eric Müller, editors, Relational and Algebraic Methods in Computer Science, pages 65-82, Cham, 2014. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-06251-8_5.
  35. Daniel Lehmann and Michael O. Rabin. On the advantages of free choice: a symmetric and fully distributed solution to the dining philosophers problem. In Proceedings of the 8th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '81, pages 133-138, New York, NY, USA, 1981. Association for Computing Machinery. URL: https://doi.org/10.1145/567532.567547.
  36. Annabelle McIver and Carroll Morgan. Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, 2005. URL: https://doi.org/10.1007/b138392.
  37. J. J. Ch. Meyer and E. P. de Vink. Pomset semantics for true concurrency with synchronization and recursion. In Antoni Kreczmar and Grazyna Mirkowska, editors, Mathematical Foundations of Computer Science 1989, pages 360-369, Berlin, Heidelberg, 1989. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-51486-4_83.
  38. J. J. Ch. Meyer and E.P. de Vink. Applications of compactness in the smyth powerdomain of streams. Theoretical Computer Science, 57(2):251-282, 1988. URL: https://doi.org/10.1016/0304-3975(88)90042-4.
  39. Michael Mislove. Nondeterminism and probabilistic choice: Obeying the laws. In Catuscia Palamidessi, editor, CONCUR 2000 - Concurrency Theory, pages 350-365, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-44618-4_26.
  40. Michael Mislove, Joël Ouaknine, and James Worrell. Axioms for probability and nondeterminism. Electronic Notes in Theoretical Computer Science, 96:7-28, 2004. Proceedings of the 10th International Workshop on Expressiveness in Concurrency. URL: https://doi.org/10.1016/j.entcs.2004.04.019.
  41. Carroll Morgan, Annabelle McIver, and Karen Seidel. Probabilistic Predicate Transformers. ACM Trans. Program. Lang. Syst., 18(3):325-353, May 1996. URL: https://doi.org/10.1145/229542.229547.
  42. Carroll Morgan, Annabelle McIver, Karen Seidel, and J. W. Sanders. Refinement-oriented probability for CSP. Form. Asp. Comput., 8(6):617-647, November 1996. URL: https://doi.org/10.1007/bf01213492.
  43. Robert Morris. Counting large numbers of events in small registers. Commun. ACM, 21(10):840-842, October 1978. URL: https://doi.org/10.1145/359619.359627.
  44. Renato Neves. An adequacy theorem between mixed powerdomains and probabilistic concurrency, 2024. URL: https://doi.org/10.48550/arXiv.2409.15920.
  45. Louis Parlant. Monad Composition via Preservation of Algebras. PhD thesis, University College London, 2020. URL: https://discovery.ucl.ac.uk/id/eprint/10112228/.
  46. Gordon Plotkin. A powerdomain construction. SIAM Journal on Computing, 5(3):452-487, 1976. URL: https://doi.org/10.1137/0205035.
  47. Vaughan R. Pratt. Semantical Considerations on Floyd-Hoare Logic. In 17th Annual Symposium on Foundations of Computer Science (sfcs 1976), pages 109-121, 1976. URL: https://doi.org/10.1109/SFCS.1976.27.
  48. Vaughan R. Pratt. Modeling concurrency with partial orders. Int. J. Parallel Program., 15(1):33-71, 1986. URL: https://doi.org/10.1007/BF01379149.
  49. Michael O. Rabin. N-process synchronization by 4.log2n-valued shared variable. In 21st Annual Symposium on Foundations of Computer Science (sfcs 1980), pages 407-410, 1980. URL: https://doi.org/10.1109/SFCS.1980.26.
  50. Michael O. Rabin. The choice coordination problem. Acta Inf., 17(2):121-134, June 1982. URL: https://doi.org/10.1007/BF00288965.
  51. Dana Scott. Outline of a Mathematical Theory of Computation. Technical Report PRG02, OUCL, November 1970. Google Scholar
  52. Dana Scott and Christopher Strachey. Toward A Mathematical Semantics For Computer Languages. Technical Report Prg06, OUCL, August 1971. Google Scholar
  53. Michael Smyth. Power domains. Journal of Computer and System Sciences, 16(1):23-36, 1978. URL: https://doi.org/10.1016/0022-0000(78)90048-X.
  54. Harald Søndergaard and Peter Sestoft. Non-determinism in Functional Languages. The Computer Journal, 35(5):514-523, October 1992. URL: https://doi.org/10.1093/comjnl/35.5.514.
  55. Joseph Tassarotti. Verifying Concurrent Randomized Algorithms. PhD thesis, Carnegie Mellon University, December 2018. URL: https://csd.cmu.edu/academics/doctoral/degrees-conferred/joseph-tassarotti.
  56. Joseph Tassarotti and Robert Harper. A Separation Logic for Concurrent Randomized Programs. Proc. ACM Program. Lang., 3(POPL), January 2019. URL: https://doi.org/10.1145/3290377.
  57. Regina Tix. Continuous D-cones: convexity and powerdomain constructions. PhD thesis, Darmstadt University of Technology, Germany, 1999. URL: https://d-nb.info/957239157.
  58. Regina Tix. Convex power constructions for continuous d-cones. Electronic Notes in Theoretical Computer Science, 35:206-229, 2000. Workshop on Domains IV. URL: https://doi.org/10.1016/S1571-0661(05)80746-7.
  59. Regina Tix, Klaus Keimel, and Gordon Plotkin. Semantic domains for combining probability and non-determinism. Electronic Notes in Theoretical Computer Science, 222:3-99, 2009. URL: https://doi.org/10.1016/j.entcs.2009.01.002.
  60. Daniele Varacca. The powerdomain of indexed valuations. In Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pages 299-308, 2002. URL: https://doi.org/10.1109/LICS.2002.1029838.
  61. Daniele Varacca. Probability, Nondeterminism and Concurrency: Two Denotational Models for Probabilistic Computation. PhD thesis, University of Aarhus, November 2003. URL: https://www.brics.dk/DS/03/14/.
  62. Daniele Varacca, Hagen Völzer, and Glynn Winskel. Probabilistic event structures and domains. Theoretical Computer Science, 358(2):173-199, 2006. Concurrency Theory (CONCUR 2004). URL: https://doi.org/10.1016/j.tcs.2006.01.015.
  63. Daniele Varacca and Glynn Winskel. Distributing probability over non-determinism. Mathematical Structures in Computer Science, 16(1):87-113, 2006. URL: https://doi.org/10.1017/S0960129505005074.
  64. Daniele Varacca and Nobuko Yoshida. Probabilistic π-Calculus and Event Structures. Electronic Notes in Theoretical Computer Science, 190(3):147-166, 2007. Proceedings of the Fifth Workshop on Quantitative Aspects of Programming Languages (QAPL 2007). URL: https://doi.org/10.1016/j.entcs.2007.07.009.
  65. Glynn Winskel. Probabilistic and Quantum Event Structures. In Franck van Breugel, Elham Kashefi, Catuscia Palamidessi, and Jan Rutten, editors, Horizons of the Mind. A Tribute to Prakash Panangaden: Essays Dedicated to Prakash Panangaden on the Occasion of His 60th Birthday, pages 476-497, Cham, 2014. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-06880-0_25.
  66. Noam Zilberstein, Derek Dreyer, and Alexandra Silva. Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning. Proc. ACM Program. Lang., 7(OOPSLA1), April 2023. URL: https://doi.org/10.1145/3586045.
  67. Noam Zilberstein, Daniele Gorla, and Alexandra Silva. Denotational Semantics for Probabilistic and Concurrent Programs (Full Version), 2025. URL: https://arxiv.org/abs/2503.02768.
  68. Noam Zilberstein, Dexter Kozen, Alexandra Silva, and Joseph Tassarotti. A demonic outcome logic for randomized nondeterminism. Proc. ACM Program. Lang., 9(POPL), January 2025. URL: https://doi.org/10.1145/3704855.
  69. Noam Zilberstein, Angelina Saliling, and Alexandra Silva. Outcome separation logic: Local reasoning for correctness and incorrectness with computational effects. Proc. ACM Program. Lang., 8(OOPSLA1), April 2024. URL: https://doi.org/10.1145/3649821.
  70. Noam Zilberstein, Alexandra Silva, and Joseph Tassarotti. Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants, 2024. URL: https://doi.org/10.48550/arXiv.2411.11662.
  71. Maaike Zwart. On the Non-Compositionality of Monads via Distributive Laws. PhD thesis, University of Oxford, 2020. URL: https://ora.ox.ac.uk/objects/uuid:b2222b14-3895-4c87-91f4-13a8d046febb.
  72. Maaike Zwart and Dan Marsden. No-Go Theorems for Distributive Laws. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13, 2019. URL: https://doi.org/10.1109/lics.2019.8785707.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact