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.
CITATION STYLE
Goy, A., & Rot, J. (2018). (In)finite trace equivalence of probabilistic transition systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11202 LNCS, pp. 100–121). Springer Verlag. https://doi.org/10.1007/978-3-030-00389-0_7
Mendeley helps you to discover research relevant for your work.