We study trace-based equivalences for labelled transition systems combining nondeterministic and probabilistic choices. We do so via a coalgebraic construction known as the generalized powerset construction, which consists in first determinizing a system and then recovering trace equivalence as bisimilarity on the determinized system. The generalized powerset construction allows us to apply these two steps, inspired by the standard powerset construction for nondeterministic automata, to a variety of systems, such as labelled transition systems with different computational effects captured by monads (e.g., systems with probabilistic choices). We show how trace semantics for labelled transition systems combining nondeterministic and probabilistic choices can be recovered by instantiating the generalized powerset construction, and we characterise and compare the resulting semantics to known definitions of trace equivalences appearing in the literatures. Most of our results are based on the exciting interplay between monads and their presentations via algebraic theories.

This talk is based on joint work with Filippo Bonchi and Ana Sokolova, available at https://arxiv.org/abs/1808.00923