It is shown how infinite trace semantics of probabilistic transition systems arises through a determinisation construction, which is then used in a bisimulation-based algorithm for infinite trace equivalence.
We show how finite and infinite trace semantics of generative probabilistic transition systems arises through a determinisation construction. This enables the use of bisimulations (up-to) to prove equivalence. In particular, it follows that trace equivalence for finite probabilistic transition systems is decidable. Further, the determinisation construction applies to both discrete and continuous probabilistic systems.