DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2025.39

Denotational Semantics for Probabilistic and Concurrent Programs

Authors: Noam Zilberstein, Daniele Gorla, and Alexandra Silva

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

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

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)

Copy BibTex To Clipboard

@InProceedings{zilberstein_et_al:LIPIcs.CONCUR.2025.39,
  author =	{Zilberstein, Noam and Gorla, Daniele and Silva, Alexandra},
  title =	{{Denotational Semantics for Probabilistic and Concurrent Programs}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{39:1--39:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.39},
  URN =		{urn:nbn:de:0030-drops-239890},
  doi =		{10.4230/LIPIcs.CONCUR.2025.39},
  annote =	{Keywords: Denotational Semantics, Pomsets, Concurrency, Convex Powerset}
}

Search Results

Documents authored by Zilberstein, Noam

Denotational Semantics for Probabilistic and Concurrent Programs

Abstract

Cite as

Thanks for your feedback!

Could not send message