(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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [31 references]  Display  Hide  Download

Contributor : Hal Ifip <>
Submitted on : Thursday, February 21, 2019 - 3:41:00 PM
Last modification on : Saturday, February 23, 2019 - 1:16:46 AM
Long-term archiving on : Wednesday, May 22, 2019 - 7:54:58 PM


 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2021-01-01

Please log in to resquest access to the document


Distributed under a Creative Commons Attribution 4.0 International License



Alexandre Goy, Jurriaan Rot. (In)finite Trace Equivalence of Probabilistic Transition Systems. 14th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2018, Thessaloniki, Greece. pp.100-121, ⟨10.1007/978-3-030-00389-0_7⟩. ⟨hal-02044641⟩



Record views