A Bounding Quantifier. CSL, 2004 PDF
Mikołaj Bojańczyk, Thomas Colcombet
Bounds in w-Regularity. LICS, 2006 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 in the first paper above, I thought that it would be decidable. The first signs were promising, e.g. the paper “Bounds in -regularity” 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. Here are some slides.