Coalgebraic trace semantics for continuous probabilistic transition systems

DOI10.2168/LMCS-9(4:16)2013MaRDI QIDQ2871468zbMATH OpenOpenAlexFDO

Authors Henning Kerstan, Barbara König

Publication date 8 January 2014

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1310.7417

zbMATH Keywords

coalgebraMarkov processesprobabilistic transition systemstrace semantics

Mathematics Subject Classification ID

Categorical semantics of formal languages (18C50) Continuous-time Markov processes on general state spaces (60J25) Semantics in the theory of computing (68Q55) Abstract data types; algebraic specification (68Q65) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: Coalgebras in a Kleisli category yield a generic definition of trace semantics for various types of labelled transition systems. In this paper we apply this generic theory to generative probabilistic transition systems, short PTS, with arbitrary (possibly uncountable) state spaces. We consider the sub-probability monad and the probability monad (Giry monad) on the category of measurable spaces and measurable functions. Our main contribution is that the existence of a final coalgebra in the Kleisli category of these monads is closely connected to the measure-theoretic extension theorem for sigma-finite pre-measures. In fact, we obtain a practical definition of the trace measure for both finite and infinite traces of PTS that subsumes a well-known result for discrete probabilistic transition systems. Finally we consider two example systems with uncountable state spaces and apply our theory to calculate their trace measures.

Recommendations

• Coalgebraic Trace Semantics for Probabilistic Transition Systems Based on Measure Theory
• Generic Trace Semantics via Coinduction
• Generic trace theory
• Trace semantics for coalgebras
• Trace semantics via determinization

Cited in

(20)

• (In)finite trace equivalence of probabilistic transition systems
• Probabilistic mediator: a coalgebraic perspective
• Generic trace theory
• Coalgebraic trace semantics for combined possibilitistic and probabilistic systems
• Traces, Executions and Schedulers, Coalgebraically
• Behavioural equivalences for timed systems
• scientific article; zbMATH DE number 1973223 (Why is no real title available?)
• Coalgebraic infinite traces and Kleisli simulations
• scientific article; zbMATH DE number 6851946 (Why is no real title available?)
• scientific article; zbMATH DE number 6864542 (Why is no real title available?)
• scientific article; zbMATH DE number 7376040 (Why is no real title available?)
• Generic trace semantics and graded monads
• Sound and complete axiomatization of trace semantics for probabilistic systems
• Graded monads and graded logics for the linear time -- branching time spectrum
• Graded semantics and graded logics for Eilenberg-Moore coalgebras
• Fractals from regular behaviours
• A complete inference system for probabilistic infinite trace equivalence
• Quantitative simulations by matrices
• Generic weakest precondition semantics from monads enriched with order
• Behavioural equivalences for coalgebras with unobservable moves

This page was built for publication: Coalgebraic trace semantics for continuous probabilistic transition systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2871468)