Characterizing Ef Over Infinite Trees And Modal Logic On Transitive Graphs

We provide several effective equivalent characterizations of EF (the modal logic of the descendant relation) on arbitrary trees. More specifically, we prove that, for EF-bisimulation invariant properties of trees, being definable by an EF formula, being a Borel set, and being definable in weak monadic second order logic, all coincide. The proof builds upon a known algebraic characterization of EF for the case of finitely branching trees due to Bojanczyk and Idziaszek. We furthermore obtain characterizations of modal logic on transitive Kripke structures as a fragment of weak monadic second order logic and of the mu-calculus.