Bisimilarity is not Borel

TL;DR

This paper demonstrates that bisimilarity for countable labelled transition systems is highly complex, not Borel, and cannot be characterized by a countable logic with measurable semantics, impacting probabilistic and nondeterministic process theory.

Contribution

It proves bisimilarity is $ ext{Σ}_1^1$-complete, showing it is not Borel, and establishes the non-existence of a suitable countable logic for image-infinite processes.

Findings

Bisimilarity is $ ext{Σ}_1^1$-complete and not Borel.

Logical characterizations of bisimilarity require non-measurable formulas.

No countable logic with measurable semantics exists for image-infinite processes.

Abstract

We prove that the relation of bisimilarity between countable labelled transition systems is $\Sigma_1^1$-complete (hence not Borel), by reducing the set of non-wellorders over the natural numbers continuously to it. This has an impact on the theory of probabilistic and nondeterministic 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.