Trace Semantics for Probabilistic Transition Systems – A ...


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


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.


trace semantics, probabilistic transition system

Suggested BibTeX entry:

    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)
© University of Duisburg-Essen, Theoretical Computer Science group