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.

403 Forbidden

Some of you have informed me of not being able to access this blog recently. In fact, I am aware of this problem when trying to publish some of my recent posts.

I recently learned that is caused by problems with some of the Blogger's servers (for more, read this). This affects some, but not all, blogs from Blogger (unfortunately, including Logicomp). But, this problem goes away usually within 24 hours. So, if your computer fails to access this blog next time, please be patient and come back the following morning :-)

Model-checking on infinite transition systems

"Program testing can be used to show the presence of bugs, but never to show their absence!", said Edsger Dijkstra. Model-checking is one well-known approach to automatic verification of programs. The framework of model-checking can be described as follows. Given a representation of a program P as a finite transition system (a.k.a. Kripke Structures) M(P) and given a formal specification f in a specification language L, check whether f is true in M(P), in symbols M(P) |= f. The specification language can be any of your favorite logics; but, the most frequently used ones include LTL, CTL, CTL*, and μ-calculus. Recently, a lot of effort has been made to extend the framework to suitable classes of infinite structures. In this post, I will mostly talk about model-checking on infinite transition systems. The logic that we frequently use in this case is monadic second-order logic (MSO) as

1. It subsumes most modal logics that we use in verification including all the afore-mentioned logics, and
   
2. MSO is a well-behaved and well-studied logic.
   

Here is a quick memory refresher: MSO is first-order logic (FO) that is extended by quantification over sets and atomic formulas of the form "x ∈ X" with the meaning that the element x of the domain D of given interpretation belongs to the set X, which is interpreted as a subset of D.

I will talk about one simple kind of infinite transition systems that goes by the name of pushdown graphs. A pushdown graph is nothing but the transition graph of a pushdown automaton. Here, a pushdown automaton is a tuple (Q,A,Γ, q₀, Z₀, Δ), where Q is a finite set of states, A the input alphabet, Γ the stack alphabet, Z₀ ∈ Γ the initial stack symbol, and the transition relation Δ is a finite subset of Q x A x Γ x Γ^* x Q, where (q,a,v,&alpha,q') is to be interpreted as "Whenever I am on a state q, see the letter a on the input tape, and see the letter v on the stack tape, I will replace v by the word α and move to a new state q'". Further, for a technical reason, it is usually wise to assume that there is no transition rule that pops the stack symbol Z₀. Now a pushdown graph for this automaton is the infinite graph G = (V,(E_a)_{a ∈ A}) where:

• V is the set of configurations of the automaton (i.e. words from QΓ^*, a product of the current state and the stack configurations) that are reachable from q₀Z₀ by a finite number of applications of Δ,
  
• E_a is the set of all pairs (qvw,q'αw) from V² for which there is a transition (q,a,v,α,q').
  

A result of Muller-Schupp is that MSO model-checking problem on pushdown graphs is decidable. The proof of this result is by direct MSO-interpretation to S2S (MSO theory of 2-successors), and uses Rabin's deep result that S2S be decidable. I recommend

W. Thomas. Constructing Infinite Graphs with a Decidable MSO-theory

for a nice presentation of this proof.

Now comes the most important question. What sort of queries can you ask in MSO regarding pushdown graphs? The most useful one is reachability, i.e., given two configurations C and C', determine whether C' is reachable from C. This is how you write it in MSO:

REACH(x,x') ≡ ∀ X( x∈X and ∀y,z( y∈X and E(y,z) --> z∈X) --> x'∈X)

As usual, E(x,y) is an abbreviation for "OR_{a ∈ A} E(x,y)". It turns out that there are lots of fancy infinite graphs on which MSO model-checking are decidable. But, this is a subject of future posts.

Slides from Logic and Databases Workshop at Cambridge

Last week I was attending a logic and databases workshop at Cambridge, UK, as part of a special programme on logic and algorithms at Newton Institute. As there were some excellent talks, I want to point out that there the slides are available online. I personally recommend the following slides: Neven's, Lynch's, Segoufin's, Schweikardt's, Libkin's, Szeider's, and Koch's.

Resuming to Blog

Apologies for being silent for a long time. Thanks for those who for the last few months left comments on my blog or emailing me directly, and apologies if I did not reply. Until very recently, I was not so sure of which research track in finite model theory I wanted to pursue for my graduate studies, even though I have a general overview of the area. It is a difficult, but crucial, task for a new researcher in finite model theory (I believe even for 1st year graduate students like myself) to pin down exactly where (s)he should start, as the area is both deep and diverse. Realizing that this is extremely important, I desperately tried to read more and talk more with my advisor and others (yes, at the expense of blogging and replying emails). I am glad to say that I have found something that I really like and am confident that I can contribute to; which also implies that I may resume blogging.

I realize that it will take some time for my blog readers to resume reading this blog (I certainly hope they will), and so I will start slow. Just in case you are in Toronto, I am planning to start a reading group focusing on "monadic theory of tree-like structures" and applications to computer verification (e.g. see this book). If you're curious but not sure of what it is, don't worry as I will give you a flavor of the area in the next few posts. The goal is to get a big picture of the area, know which problems are open, and understand important proof ideas without having to read each paper. [Each participant will take turn to present one result each time we meet.] Everyone is warmly welcome to participate. [I will make a more detailed announcement in a week.]