Stochastic coalgebraic logic (Q1049890): Difference between revisions

Stochastic logics over measurable spaces, specifically analytic spaces, originally go back to \textit{J. Desharnais, A. Edalat} and \textit{P. Panangaden}, [``Bisimulation for labelled Markov processes'', Inf. Comput. 179, No.~2, 163--193 (2002; Zbl 1096.68103)]. The main result on stochastic logics is that they characterize bisimilarity of probabilistic systems. The present monograph lifts these results to the level of generality of coalgebras over analytic spaces, in analogy to the set-based case developed by \textit{D. Pattinson} [``Expressive logics for coalgebras via terminal sequence induction'', Notre Dame J. Formal Logic 45, No.~1, 19--33 (2004; Zbl 1088.03031)] and \textit{L. Schröder} [``Expressivity of coalgebraic modal logic: the limits and beyond'', Theor. Comput. Sci. 390, No.~2--3, 230--247 (2008; Zbl 1132.03008)]. Here, a coalgebra is a system of the shape \(\xi:X\to FX\) where \(F\) is some endofunctor on the base category, i.e., an assignment of a structured collection \(\xi(x)\) of successors to each state \(x\), where the nature of the structured collection is determined by the functor \(F\), which may, e.g., encapsulate \(n\)-ary relations for arbitrary finite or infinite \(n\). (In the set-based case, \(F\) often encodes also much more complex behaviour; such examples are not yet developed in the measurable case.) The basic example in the stochastic setting is for \(F\) to be the subprobabilities functor, so that coalgebras for \(F\) are stochastic transition systems. The monograph is concerned almost entirely with the question of when two basic equivalences on stochastic (coalgebraic) models coincide, namely logical equivalence (indistinguishability under the formulas of a given logic), behavioural equivalence (identification under a \textit{cospan}, i.e., two morphisms into a common target model), and bisimilarity (identification via a \textit{span}, i.e., two model morphisms from a common source). It is well known (and is formally discussed at a fair level of generality in [\textit{L. S. Moss} and \textit{I. D. Viglizzo}, ``Final coalgebras for functors on measurable spaces'', Inf. Comput. 204, No.~4, 610--636 (2006; Zbl 1103.68084)]) that the equivalence between logical equivalence and behavioural equivalence holds over arbitrary measurable spaces; this is also covered in the monograph under review (Section 2.6). The main technical issue is coincidence with the third equivalence, bisimilarity; it is this point which requires restricting the scene to analytic spaces. The book begins with an extensive and useful introduction to basic concepts from the theory of measurable and analytic spaces required for the further technical development. A second chapter introduces the most important ones of the modal logics under study, as well as the semantic setting and the mentioned notions of semantic equivalence. It also provides a detailed development of the basic result stating that the three basic equivalences coincide in a setting where stochastic transitions are indexed over an uncountable set (specifically the positive reals, thought of as time spans), provided that the model obtained by factoring through logical equivalence is standard Borel. There follows an excursion to an extended setting where not only the models themselves but also their morphisms are stochastic; in this setting, two additional equivalences are identified, \textit{distributional equivalence} and mutual relation via \textit{\(\mathcal{L}\)-ergodic morphisms}, and their coincidence with the other three equivalences is proved for stochastic Kripke models over analytic spaces. Finally, the setup is generalized in an orthogonal direction to coalgebraic stochastic models in the proper sense, i.e.\ involving a general (rather than just polynomial) functor \(\mathfrak{F}\) on the category of analytic spaces. Here, two cases are distinguished according to whether \(\mathfrak{F}\) appears to the left or to the right of the subprobabilities functor, thus generalizing generative probabilistic automata in the former case and reactive probabilistic automata in the latter case. In both cases, the equivalence of behavioural equivalence with bisimilarity requires additional technical conditions on \(\mathfrak{F}\), which are shown to hold for some examples. In summary, the book provides an overview of a large amount of technically challenging material; it is suitable reading, e.g., for graduate students in the field of stochastic logics.