Trace Semantics for Nondeterministic Probabilistic Automata via Determinization.

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. This inspires, in turn, a general theory of may and must testing where tests are finite traces. Most of our results are based on the exciting interplay between monads and their presentations via algebraic theories.