(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

https://hal.inria.fr/hal-02044641
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

File

 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

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

39