A Bounding Quantifier. CSL, 2004 PDF
Mikołaj Bojańczyk, Thomas Colcombet
Bounds in w-Regularity. LICS, 2006 PDF
Mikołaj Bojańczyk, Pawel Parys, Szymon Torunczyk
The MSO+U Theory of (N, <) Is Undecidable. STACS, 2016 PDF
Weak MSO with the Unbounding Quantifier. Theory Comput. Syst., 2011 PDF
Mikołaj Bojańczyk, Szymon Torunczyk
Deterministic Automata and Extensions of Weak MSO. FSTTCS, 2009 PDF
Mikołaj Bojańczyk, Szymon Torunczyk
Weak MSO+U over infinite trees. STACS, 2012 PDF
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 , I thought that it would be decidable. The first signs were promising, e.g. the paper  showed that counter automata could be used to decide fragments of the logic. Now we know that the full logic is undecidable , but the problems seem to come from quantifying over infinite sets, and weak fragments are decidable [4,5,6,7]. Here are some slides.
The logic MSO+U is undecidable: more specifically, paper  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.
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 . 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 , which is a journal version of
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 , 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  and  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.
Leave a Reply