Coalgebraic logic for stochastic right coalgebras (Q1023291)

The main object of this work is to transfer expressivity results previously obtained in set-based coalgebraic modal logic [\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); \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)] to the setting of probabilistic coalgebraic logics on analytic spaces, continuing previous work by the first author [\textit{E.-E.\ Doberkat}, ``Stochastic coalgebraic logic: bisimilarity and behavioral equivalence'', Ann. Pure Appl. Logic 155, No.~1, 46--68 (2008; Zbl 1147.03014)]. The functors under study are of the form \(\mathfrak{F}^\sharp=\mathfrak{F}\circ\mathfrak{S}\) where \(\mathfrak{S}\) is the subprobability functor (the subprobabilistic variant of the well-known Giry monad) and \(\mathfrak{F}\) is a functor on analytic spaces. The logics in question are interpreted over \(\mathfrak{F}^\sharp\)-coalgebras \(A\to\mathfrak{F}^\sharp(A)\), where \(A\) is an analytic space. The framework is parametric in a set of predicate liftings, which in this setting are natural transformations \(\mathfrak{B}\to\mathfrak{B}\circ(\mathfrak F^\sharp)^{\text{op}}\) where \(\mathfrak B\) is the contravariant functor sending a space to its set of Borel sets. These predicate liftings serve to interpret modal operators following the standard paradigm of coalgebraic logic. One has three notions of equivalence of states in stochastic coalgebras: logical equivalence; behavioural equivalence, defined via cospans of morphisms; and bisimilarity, defined via spans of morphisms. The main results of the present work are on the one hand that, under a suitable separation condition involving coalgebraic models (rather than just the functor as in corresponding set-based results), logical equivalence coincides with behavioural equivalence; and on the other hand that if \(\mathfrak F\) satisfies additional assumptions, in particular is compatible in a suitable sense with pullbacks in the category of sets, then behavioural equivalence coincides with bisimilarity.