The Theory of Traces for Systems with Nondeterminism, Probability, and Termination
arXiv:1808.00923 · doi:10.46298/lmcs-18(2:21)2022
Abstract
This paper studies trace-based equivalences for systems combining nondeterministic and probabilistic choices. We show how trace semantics for such processes can be recovered by instantiating a coalgebraic construction known as the generalised powerset construction. We characterise and compare the resulting semantics to known definitions of trace equivalences appearing in the literature. Most of our results are based on the exciting interplay between monads and their presentations via algebraic theories.
References in corpus (9)
- Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints
- A Convenient Category for Higher-Order Probability Theory
- Generic Trace Semantics via Coinduction
- Relating coalgebraic notions of bisimulation
- Mixed powerdomains for probability and nondeterminism
- Revisiting Trace and Testing Equivalences for Nondeterministic and Probabilistic Processes
- Coalgebraic trace semantics via forgetful logics
- Trace and Testing Metrics on Nondeterministic Probabilistic Processes
- Termination in Convex Sets of Distributions