Nie jesteś zalogowany |
Characterizations of EF over Infinite Trees
- Prelegent(ci)
- Alessandro Facchini
- Afiliacja
- Uniwersytet Warszawski
- Termin
- 23 lutego 2011 14:15
- Pokój
- p. 5870
- 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.
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.
