Zilberstein, N; Gorla, D; Silva, A; (2025) Denotational Semantics for Probabilistic and Concurrent Programs. In: 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs). (pp. 39:1-39:24). Leibniz-Zentrum für Informatik: Dagstuhl, Germany.

Preview

Text LIPIcs.CONCUR.2025.39.pdf - Published Version Download (1MB) | Preview

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.

Download activity - last month

Export as XMLCSVJSON

Download activity - last 12 months

Export as JSONXMLCSV

Downloads by country - last 12 months

Export as CSVXMLJSON

Archive Staff Only

View Item