Bisimilarity is not Borel

What is it about?

Bisimilarity is one of the main notions of “equivalence of behavior” in Theoretical Computer Science; in particular it can be defined on the space of all countable transition systems with a fixed countable set of labelled actions. The latter has a natural topological structure, and it is proved that the relation of bisimilarity on this space has high complexity in the hierarchy of its subsets; namely, more complex than open and closed sets, and their countable unions and interesections (it is not Borel).

Featured Image

Why is it important?

Most of the time, one wants to characterize bisimilar states of a transition system as those satisfying the same formulas of a given logic; here, “satisfying a formula” is akin to “passing a test”. Therefore, one chooses a family of tests and expects that states passing exaclty the same test turn out to be related by bisimilarity. The most important application of this result is that for transitions systems that include probabilities and “infinite non-determinism”, the complexity of bisimilarity obstructs all known techniques known to prove the logical characterization.

Perspectives