Mikołaj Bojańczyk

MSO+U


July 14, 2015
  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

The logic MSO+U is the extension of MSO with the quantifier U, where UX \phi(X) says that there are arbitrarily large finite sets X which make \phi(X) 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 \omega-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.

 

Leave a Reply

Your email address will not be published.