1. Mikołaj Bojańczyk
   A Bounding Quantifier. CSL, 2004   PDF

2. Mikołaj Bojańczyk, Thomas Colcombet
   Bounds in w-Regularity. LICS, 2006   PDF

3. Mikołaj Bojańczyk, Pawel Parys, Szymon Torunczyk
   The MSO+U Theory of (N, <) Is Undecidable. STACS, 2016   PDF

4. Mikołaj Bojańczyk
   Weak MSO with the Unbounding Quantifier. Theory Comput. Syst., 2011   PDF

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

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

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

The logic MSO+U is the extension of MSO with the quantifier U, where says that there are arbitrarily large finite sets which make true. The point of the logic is to express boundedness properties like: “a graph has bounded outdegree” or “a sequence of numbers tends to infinity”. When introducing the logic [1], I thought that it would be decidable. The first signs were promising, e.g. the paper [2] showed that counter automata could be used to decide fragments of the logic. Now we know that the full logic is undecidable [3], but the problems seem to come from quantifying over infinite sets, and weak fragments are decidable [4,5,6,7]. Here are some slides.

 

Undecidability of MSO+U

The logic MSO+U is undecidable: more specifically, paper [3] shows that satisfiability of MSO+U over -words is undecidable. This is an improvement on a previous paper

• Mikołaj Bojańczyk, Tomasz Gogacz, Henryk Michalewski, Michal Skrzypczak
  On the Decidability of MSO+U on Infinite Trees. ICALP (2), 2014   PDF

which showed undecidability for infinite trees, and with an additional set-theoretic assumption called V=L.

Decidability of weak MSO+U

The group of papers [4,5,6,7] 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.  As mentioned above, without the weak restriction, i.e. for MSO+U, the logic is undecidable [3]. 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 [4], 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 [5], 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 [6] and [7] 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.