Semipullbacks of labelled Markov processes

arXiv1706.02801MaRDI QIDQ6287675FDOQ6287675

Authors: Jan Pachl, Terraf Pedro Sánchez 

Publication date: 8 June 2017

Abstract: A labelled Markov process (LMP) consists of a measurable space $S$ together with an indexed family of Markov kernels from $S$ to itself. This structure has been used to model probabilistic computations in Computer Science, and one of the main problems in the area is to define and decide whether two LMP $S$ and $S^{\prime }$ "behave the same". There are two natural categorical definitions of sameness of behavior: $S$ and $S^{\prime }$ are bisimilar if there exist an LMP $T$ and measure preserving maps forming a diagram of the shape $SleftarrowTightarrow{S}^{\prime }$; and they are behaviorally equivalent if there exist some $U$ and maps forming a dual diagram $SightarrowUleftarrow{S}^{\prime }$. These two notions differ for general measurable spaces but Doberkat (extending a result by Edalat) proved that they coincide for analytic Borel spaces, showing that from every diagram $SightarrowUleftarrow{S}^{\prime }$ one can obtain a bisimilarity diagram as above. Moreover, the resulting square of measure preserving maps is commutative (a semipullback). In this paper, we extend the previous result to measurable spaces $S$ isomorphic to a universally measurable subset of a Polish space with the trace of the Borel $sigma$-algebra, using a version of Strassen's theorem on common extensions of finitely additive measures.

Mathematics Subject Classification ID

Discrete-time Markov processes on general state spaces (60J05) General theory of categories and functors (18Axx) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Special categories (18Bxx)

This page was built for publication: Semipullbacks of labelled Markov processes

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