Approximating Markov processes through filtration (Q442296)

The Hennessy-Milner theorem states that image finite Kripke models are bisimilar if and only if they are logically equivalent. This holds for modal logics that are interpreted through Kripke models. The extension of this property to probabilistic logics with probabilistic Kripke models based on continuous state spaces has turned out to present a considerable challenge; it was answered in the positive for analytic spaces by \textit{J. Desharnais} et al. [Inf. Comput. 179, No. 2, 163--193 (2002; Zbl 1096.68103)] through a laborious construction using disintegration of measures, and for Polish spaces by this reviewer [SIAM J. Comput. 35, No. 3, 590--626 (2006; Zbl 1095.68063)] through selection arguments. The present paper deals with this problem through an approximation argument; approximating Markov transition systems has been proposed and studied by \textit{J. Desharnais} et al. [Theor. Comput. Sci. 318, No. 3, 323--354 (2004; Zbl 1068.68093)] and by \textit{F. van Breughel} and \textit{J. Worrell} [Theor. Comput. Sci. 331, No. 1, 115--142 (2005; Zbl 1070.68109)]. These papers construct metrics, so that approximation becomes metric approximation. The present paper constructs a metric as well, but in contrast to the papers mentioned above the metrics are constructed through novel process using filtration, taking a discount factor into account (the later two formulas differ the smaller the distance gets). It is shown that a Polish space is obtained, but, strictly speaking, the authors obtain a pseudometric space which is shown to be Polish after canonically factoring it. The techniques are derived mainly from the first author's Ph.D. thesis and a subsequent paper of his [J. Log. Comput. 19, No. 6, 1427--1454 (2009; Zbl 1191.03018)]. The paper is well written; it carefully explains the development, the proofs are accessible, albeit, as to be expected, fairly technical. It provides a wealth of information about Markov transition systems; the references reflect the state of the art.