Trace Semantics via Determinization for Probabilistic Transition Systems

Abstract

A coalgebraic definition of finite and infinite trace semantics for probabilistic transition systems has recently been given using a certain Kleisli category. In this paper this semantics is developed using a coalgebraic method which is an instance of general determinization. Once applied to discrete systems, this point of view allows the exploitation of the determinized structure by up-to techniques. Thereby it becomes possible to algorithmically check the equivalence of two finite probabilistic transition systems.

Alexandre Goy

Postdoc

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