(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.

Alexandre Goy

Postdoc

I am interested in theoretical computer science, especially logic, category theory, coalgebra, and probabilistic aspects of these topics.