Unprovability of the Logical Characterization of Bisimulation

TL;DR

This paper demonstrates that in general measurable spaces, logical characterizations of bisimulation for labelled Markov processes are unprovable and that event and state bisimilarity can differ, challenging existing assumptions.

Contribution

It provides a counterexample showing the unprovability of logical characterization of bisimulation in certain measurable spaces and proves the non-existence of semi-pullbacks for stationary Markov processes.

Findings

Event bisimilarity differs from state bisimilarity in non-analytic spaces.

Logical characterization of bisimulation is unprovable in certain measurable spaces.

Stationary Markov processes lack semi-pullbacks in general measurable spaces.

Abstract

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 logic in 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. ([*] J. Desharnais, Labelled Markov Processes. School of Computer Science. McGill University, Montr\'eal (1999))