Bisimilarity is not borel

Abstract

We prove that the relation of bisimilarity between countable labelled transition systems (LTS) is Σ1 1-complete (hence not Borel), by reducing the set of non-well orders over the natural numbers continuously to it. This has an impact on the theory of probabilistic and non-deterministic processes over uncountable spaces, since logical characterizations of bisimilarity (as, for instance, those based on the unique structure theorem for analytic spaces) require a countable logic whose formulas have measurable semantics. Our reduction shows that such a logic does not exist in the case of image-infinite processes.