Bisimilarity is not Borel

PEDRO SÁNCHEZ TERRAF

Seminario; Dagstuhl Seminar on Coalgebraic Logics; 2012

Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH

We prove that the relation of bisimilarity between countable labelled transition systems is analytic-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 the proofs of logical characterizations of bisimilarity 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.