How do you mean bisimulation in this case? This seems to be a reduction down to decidable predicates, e.g. a Turing machine for each set. Without a type theory, many obvious algorithms will fail to converge.