(In)finite Trace Equivalence of Probabilistic Transition Systems

Abstract

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.

Publication
Coalgebraic Methods in Computer Science