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}
}
