Unprovability of the logical characterization of bisimulation

We quickly review labelled Markov processes (LMP) and provide a counterexample showing that in general measurable spaces, event bisimilarity and state bisimilarity differ in LMP. This shows that the Hennessy–Milner logic proposed by Desharnais does not characterize state bisimulation in non-analytic measurable spaces. Furthermore we show that, under current foundations of Mathematics, such logical characterization is unprovable for spaces that are projections of a coanalytic set. Underlying this construction there is a proof that stationary Markov processes over general measurable spaces do not have semi-pullbacks.