Characterizations of EF over Infinite Trees

Prelegent(ci)

Alessandro Facchini

Afiliacja

Uniwersytet Warszawski

Termin

23 lutego 2011 14:15

Pokój

p. 5870

Tytuł w języku angielskim

joint work with Balder ten Cate

Seminarium

Seminarium „Teoria automatów”

---

We provide several equivalent effective 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
Bojańczyk and Idziaszek. As a corollary, we obtain that over transitive models, for every formula \phi of the modal \mu-calculus: \phi is equivalent to a modal formula iff \phi is equivalent to a WMSO (or FO) formula iff the class of models of \phi is Borel.

---