You are not logged in |
joint work with Balder ten Cate
- Speaker(s)
- Alessandro Facchini
- Affiliation
- Uniwersytet Warszawski
- Date
- Feb. 23, 2011, 2:15 p.m.
- Room
- room 5870
- Seminar
- Seminar Automata Theory
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.
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.
