Weak MSO+U with path quantifiers

Speaker(s)

Mikołaj Bojańczyk

Affiliation

Uniwersytet Warszawski

Date

Jan. 15, 2014, 2:15 p.m.

Room

room 5870

Seminar

Seminar Automata Theory

---

Over infinite trees, satisfiability is decidable  for weak monadic second-order logic extended by the unbounding quantifier U and  quantification over infinite paths. The proof is by reduction to emptiness for a certain automaton model, while emptiness for the automaton model is decided using profinite trees.

---