Trace Semantics for Probabilistic Transition Systems
– A Coalgebraic Approach
published on Tue, 27 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.