Reading Group

I am at present organizing a reading group on "Model Checking on Nice Infinite Structures". Its purpose is to help the participants get a big picture of the area, know which problems are presently open, and understand proof ideas without having to read every paper. In sum, if you want to get up to speed with the state of the art, attend the meetings!

Two upcoming meetings are as follows:

1. My supervisor Leonid Libkin will give an introduction to Automatic Structures on Thursday, March 23, from 2pm-3pm, UofT St. George Campus, PT378.
   
2. Pablo Barcelo will give the first part of his presentation on Walukiewicz's proof of Muchnik's theorem on Friday, March 24, from 3pm-4pm, UofT St. George Campus, PT378.
   

Feel free to stop by if you are in Toronto.

I've tried to give a flavor of the area before. I will say a little bit more. The main concern of the area is to come up with nice infinite structures on which model checking L-formulas (for some nice logic L) is computationally effective. For example, Buchi's theorem and Rabin's theorem give effective procedures for model-checking MSO formulas on, respectively, the infinite one-way successor S1S = (N,‹) and the infinite binary tree S2S = ({0,1}*,S0,S1) where

1. N is the set of natural numbers, and ‹ the graph of the usual successor function on N.
   
2. {0,1}* stands for bit strings (including the empty string),
   
   S0 = { (w,w0) : w ∈ {0,1}* },
   
   and
   
   S1 = { (w,w1) : w ∈ {0,1}* }.
   
   

It turns out that one can obtain a large number of decidability results via interpretation to S2S. As I mention previously, one can show that model checking MSO formulas on pushdown graphs is effective. In fact, using the same technique, one can show that the MSO theory of ordered rational numbers (Q,<) is decidable.

There is more to "Model Checking on Nice Infinite Structures" than what I just mentioned. For example, one of the most important research directions is to come up with "ways of transforming structures" that preserve decidability of L-theories. Examples of such transformations include unfoldings, and iterations. The latter transformation is the main concern of Muchnik's theorem, which will be presented by Pablo Barcelo some time this week. These decidability-preserving transformations are so powerful that one can obtain the decidability of S2S by reducing it to a trivial edge-labeled graph with one node and two self-loops of different labels. It turns out that one can obtain a rich theory by, for example, applying MSO-interpretations and the unfolding operation in alternation. This is the subject of Caucal's hierarchy. For more, see for the link to Thomas's survey in my previous post.

Another hot topic includes "Automatic Structures". Roughly speaking, automatic structures are logical structures that can be presented by finite automata. For example, one can obtain a characterization of regular languages using this technique. For more, see this paper.