Mikołaj Bojańczyk

## Weak MSO+U on infinite words and trees

May 17, 2015
1. Mikołaj Bojańczyk
Weak MSO with the Unbounding Quantifier. Theory Comput. Syst., 2011   PDF

2. Mikołaj Bojańczyk, Szymon Torunczyk
Deterministic Automata and Extensions of Weak MSO. FSTTCS, 2009   PDF

3. Mikołaj Bojańczyk, Szymon Torunczyk
Weak MSO+U over infinite trees. STACS, 2012   PDF

4. Mikołaj Bojańczyk
Weak MSO+U with Path Quantifiers over Infinite Trees. ICALP (2), 2014   PDF

This group of papers is about the weak fragment of MSO+U. This is a logic where one can quantify over elements, finite sets of elements (hence the name weak), and use the quantifier U, which is used to say that certain sets have unbounded size.  Without the weak restriction, i.e. for MSO+U, the logic is undecidable already on infinite words. This undecidability motivates the study of fragments of MSO+U, and the “weak” restriction which allows only quantification over finite sets is one obvious way to go.

The first result is in paper [1] from the list above, which is a journal version of

• Mikołaj Bojańczyk
Weak MSO with the Unbounding Quantifier. STACS, 2009   PDF

The paper shows that weak MSO+U is decidable over infinite words. The proof uses the automata method, and shows that over infinite words, weak MSO+U has the same expressive power as deterministic max-automata, which are a kind of counter automata where the counters can be incremented or set to the maximum of two other counters. (The acceptance is a Boolean combination of statements “counter c is bounded”.)

The above result was extended in the paper [2], which considers other weak fragments of MSO+U on infinite words. One example is a logic, which is like weak MSO+U, except that U is replaced by a quantifier called R, which says that “property is satisfied by infinitely many sets of the same size”. This quantifier is used to express properties like “the length of blocks of a’s have infinite liminf”, as opposed to U which works only for limsup. The paper also considers other extensions, including weak MSO with both U and R, and a quantifier that talks about ultimately periodic sets. The upshot is that weak MSO can be quite robustly extended with quantifiers that talk about limit behavior.

The two papers [3] and [4] are about weak MSO+U on infinite trees. The first paper shows that the logic is decidable, and the second paper shows that it remains decidable even after adding quantification over infinite paths (also known as branches). The papers are very technical, with the entire proof having over a hundred pages. The main idea is to prove something like Rabin’s Basis Theorem, which says that if a formula is satisfiable, then it is true in some regular tree. In the presence of U, the notion of regularity needs to be refined, and for this we use profinite techniques.