# Trace Semantics for Probabilistic Transition Systems – A ...

## Reference

Henning Kerstan.

Trace semantics for probabilistic transition systems – a coalgebraic approach. Diplomarbeit, Universität Duisburg-Essen, sep 2011.

## Abstract

Probabilistic transition systems, short PTS, are labelled transition systems where each transition depends on a probability. As in the case of finite automata, we are interested in analyzing the behaviour of these systems. A method to do this is to define the trace of a state. While the concept of trace semantics is easy to grasp for finite automata, the introduction of probabilities complicates the definition of a trace. We need measure and integration theory to obtain a mathematically sound definition of trace semantics for PTS with continuous state space and even for discrete PTS without explicit termination. Instead of defining trace semantics directly, we use a coalgebraic approach: We define two endofunctors on the category of measurable spaces and measurable functions and prove that they can be lifted to endofunctors on the Kleisli category of the (sub-)probability monad. Then we model PTS with and without explicit termination as a coalgebra for this lifted functor and prove that a final coalgebra exists. The unique homomorphism into the final coalgebra yields a definition of trace semantics for PTS which is a sub-probability measure on the set of all finite words in the case of a PTS with explicit termination and a probability measure on the set of all infinite words for PTS without explicit termination.

## Keywords:

trace semantics, probabilistic transition system

## Suggested BibTeX entry:

@

mastersthesis{Ker11,

author= {Henning Kerstan},

month= {sep},

school= {Universit{\"a}t Duisburg-Essen},

title= {Trace Semantics for Probabilistic Transition Systems -- A Coalgebraic Approach},

type= {Diplomarbeit},

year= {2011}

}

PDF (813 kB)