Published online by Cambridge University Press: 09 December 2015
We prove that the relation of bisimilarity between countable labelled transition systems (LTS) is Σ11-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.
Partially supported by CONICET, ANPCyT project PICT 2012-1823, SeCyT-UNC project 05/B284, and EU 7FP grant agreement 295261 (MEALS). Part of this work was presented at Dagstuhl Seminar 12411 on Coalgebraic Logics.