Correctness by design vs. formal verification

One common debate in the programming language community is the notion of correctness by design vs. verifying the correctness of your program. After all, if you can guarantee that all the programs that you write to be correct by construction, then there is no need to separately prove its correctness (using program analysis, formal verification, you name it), which is arguably non-trivial in general. How might you ensure correctness by construction? One easy way is to design a programming language that *rules out* certain bugs. For example, back in the 2001 when I started learning programming in C and then C++, I had to learn how to debug segmentation faults. A switch to higher-level programming languages like Java and Python ensures that I don't have to deal with segmentation faults anymore (assuming the correctness of JVM and Python interpreters). Can you do the same with other kinds of errors?

An interesting CACM article that I recently read (https://cacm.acm.org/magazines/2017/5/216322-ending-null-pointer-crashes/fulltext) discusses how the programming language Eiffel eliminates the problem of null pointer crashes (which could cause serious security vulnerabilities). A null pointer dereferencing happens when you invoke x.f in an object-oriented programming language, where x is a variable pointing to null and f is a field. It turns out that eliminating null pointer dereferencing by language design in a way that does not severely limit the expressiveness and convenience of the language is not straightforward, as discussed in the article. Eiffel instead relies on sophisticated use of type checking and static analysis to ensure that a program that passes an Eiffel compiler cannot exhibit null pointer crashes. So, the case study of Eiffel seems to suggest that correctness should be achieved not only by only language design or software verification alone, but by both of them simultaneously.

What about other kinds of programming errors, e.g., cross-site scripting in HTML5, data race condition in concurrent programming?

When does Bob deserve to be a co-author?

I have recently been reading Bill Gasarch's post about when Alice deserves to be a co-author. This is definitely a sensitive issue; just check the number of ANONYMOUS comments. I have recently found some advice that is more oriented towards faculty-student type of collaborations, but is perhaps also suitable in general. Check this link. Interestingly, it was a document written by Department of City and Regional Planning, University of Berkeley ...

Highland workshop on XML, Logic, and Automata

I'll be attending Highlands Workshop on XML, Logic, and Automata organized by Leonid from tomorrow until this Sunday. The venue is actually quite interesting: a small town in the Highlands called Grantown-on-spey. I'm just hoping that they have a grocery store :) I will give a presentation on recurrent reachability in regular model checking based on this paper. Anyway, I'll post a summary of the workshop later on this week.

Rahul Santhanam has joined Edinburgh

Rahul Santhanam, Lance Fortnow's ex PhD student, has recently joined Edinburgh's School of Informatics. Warm welcome to him!

Finite-variable hierarchy conjecture

It seems that Ben Rossman has resolved another long-standing open problem in finite model theory: finite-variable hierarchy conjecture. Loosely speaking, the conjecture is that over ordered graphs first-order logic with k+1 variable is more powerful than first-order logic with k variable. The problem is nicely summarized in Anuj Dawar's survey. Ben has shown that this hierarchy is strict. What was previously known is that (over ordered graphs) first-order logic with 3 variables is strictly more expressive than first-order logic with 2 variables, but it was not known whether first-order logic with 3 variables is less expressive than first-order logic with k variables, for every k > 3. Worse yet, it wasn't even known whether this hierarchy is strict. See Anuj Dawar's survey for further details.

I believe this is the third big open problems that Ben has resolved in this decade. Go Ben!

Restructuring logicomp

I'm thinking of restructuring my blogs. I've recently found that things have changed a lot since I started my break a year or so ago: Lance has retired from blogging, Andy D has started his new cool blog, and Luca Aceto has his blog. Ah ... also I'm having a lot of difficulty deciphering blogger's word verification mechanism.

Unfortunately, I've become really rusty with HTML and will have to start getting used to it again. Shocked with what a long break can do to one's dexterity ;) Anyway, I'll put all the new links some time soon.

Pushdown systems: reachability via saturations

Finally, I have some time to resume blogging again after finishing several papers (and now with something with more content). Before I continue, I'd like to apologize for not replying some comments because by mistake I had them forwarded to an expired email address. How careless I was!

Anyway, I'm intending to cover a simple basic topic in the verification of infinite-state systems. Reachability is probably the most basic question when you do verification and we would like to see how to solve this problem efficiently for pushdown systems, which are the simplest well-behaved class of infinite-state systems. For those practically-minded, pushdown systems can naturally be used to model sequential programs and algorithms for pushdown systems have been implemented and used for doing program analysis for real. By the way, the saturation technique also extends to other (more powerful) classes of infinite-state systems and so it's really worth knowing. Anyway, please review the definition of pushdown systems here before you continue.

Roughly speaking, the reachability problem for pushdown systems asks the following question: given a pushdown system P and two configurations C₁ and C₂ of P, is it possible to reach C₂ from C₁ in P? There are other variants of the problem that take sets of configurations instead of just single configurations, and they can be solved using exactly the same saturation technique.

In here I have mentioned that the MSO theory of pushdown systems is decidable and this implies that reachability is also decidable. However, the algorithm that you obtain in this way runs in exponential time.

The idea of saturation construction is to construct a finite automaton A that recognizes the set of configurations that can reach C₂ and then check whether C₁ is in the language of A; recall that membership checking for finite automata is solvable in linear time. First, observe that C₂ is a single word and is obviously regular. We start with an automaton for C₂ and introduce several extra states, each corresponding to a state of the pushdown system P. Call this automaton A. We shall iteratively add transitions to A by the following rules: if there is a transition (p,a,c,v,p') in P, and in the automaton A the state p' can reach a state q via the word v, then we shall add a transition (p,c,q) in A. The intuitive idea is that if a configuration p'vw is accepted by A, then the configuration paw must also be accepted by A because you can apply the transition (p,a,c,v,p'). By the way, notice that we don't add any states in the iteration and so the algorithm can only add polynomially many transitions to A. Hence, the algorithm terminates in polynomial time.

As far as I remember, the idea was first proposed in the paper by Bouajjani, Esparza, and Maler for pushdown systems:

Reachability analysis of pushdown automata: Application to model-checking. CONCUR 1997.

It seems that similar ideas were already proposed earlier for ground tree rewrite systems, a more general class of systems, in:

Coquide, Dauchet, and Gilleron. Bottom-up tree pushdown automata: classification and connection with rewrite systems. Theoretical Computer Science 127, 1994.

By the way, it is worth noticing that simple fixpoint computations might not terminate for pushdown systems, as the state space is infinite. So, the saturation construction is necessary after all.

Happy New Year 2008!

It was exactly a year ago that I wrote my last post. I guess I have been really busy doing research (yes, this is an excuse that always works for us researchers). I am planning on writing a few things on what research I have been doing recently in some details (as I used to do); partly to help me understand more stuff, and partly to spread around some good news about the area of logic and verification (and computation as well, of course).

Without further ado, here are some plans for my posts for the next two to three weeks:

1. Some extensions of pushdown systems and how to do model checking on these structures. I covered the definitions of pushdown systems already in here, but not how to do model checking on these structures. So, I'll start there. Extensions that I will consider including prefix-recognizable systems, ground tree rewrite systems, and some probabilistic extensions.


2. Well-structured transition systems. The theory of WSTS, which rely heavily on the theory of well-ordered quasi ordering, give general decidability results for reachability checking for large classes of infinite-state transition systems (eg, Petri Nets, lossy counter systems, etc).
   

I have moved again ...

It seems like ages since I last wrote for this blog. Last September, I moved with my advisor to the University of Edinburgh to begin my PhD. It took me longer than I thought to settle in Edinburgh as the atmosphere of the city, ESPECIALLY the gloomy weather, is quite different to that which I am accustomed to. Folklore has it that there are only sixty sunny days in Edinburgh in a year on average. I presume that forty of these days are in the summer. The other peculiarity that you can find in Edinburgh is the wind and rain. If you live outside Edinburgh and think that your city is windy, then I suggest that you come to visit Edinburgh. Actually, you'll find that the combination of wind and rain makes umbrella pretty much useless!

Anyway, apologies to my avid readers that I was silent for so long. Provided there is time and interest, I will blog again on a weekly basis.

Australia qualifies for round of 16

After losing 2 - 0 to Brazil, The Socceroos had to at least draw against Croatia. What a nerve-racking (and controversial) game that was! In the end, Australia managed to draw 2 - 2 against Croatia. Although I am supporting Australia through and through, I think that The Socceroos didn't secure the desired result convincingly. In a way, we were lucky to get a draw! Next: Italy vs. Australia.

Linear Temporal Logic (1)

As their name suggests, temporal logics are logics where truth values of formulas may change over time. The significance of temporal logic in computer science is indisputable, especially in verification of safety-critical reactive systems. Model checkers of many flavors of temporal logics have been developed to the extent that they can quickly verify real-world systems with a huge number of states. Furthermore, in contrast to many other tools and techniques of formal methods which are semi-automatic and relatively expensive, model checking is fully-automatic and quite cheap (excellent free model checkers like SPIN exist). Last year these tools and techniques were awarded the ACM Paris Kanellakis Theory and Practice Award. Amir Pnueli, the researcher who introduced the idea of using temporal logic in verification, was awarded the ACM Turing Award in 1996.

As we mentioned, temporal logic comes in a number of flavors. At present we deal only with Linear Temporal Logic (LTL). It is linear because we evaluate each LTL formula with respect to a vertex-labeled infinite path p₀p₁..., where each vertex p_i in the path corresponds to a point in time. "Present" is p₀. "Future" is any of p_i with i ≥ 0. Each vertex is labeled by a subset of 2^Σ where Σ is a set of atomic propositions. In other words, the label of a vertex indicates which atomic propositions are true in that vertex. Here is a somewhat contrived example. Suppose that Σ = {a,b}. As an example, take the path {a}²⁰⁰⁰{a,b}^ω, which is a path whose first 2000 vertices are {a}-labeled and the rest of the vertices are {a,b}-labeled. An example of an LTL formula is "at some point in the future, 'b' holds", which is true. Another example is "a holds until b holds", which is also true.

More formally, the syntax of LTL formulas can be defined in Backus-Naur form as follows:

φ, ψ := p (p ∈ Σ) | φ ∧ ψ | ¬ φ | X φ | φ U ψ

Given a 2^Σ-labeled (infinite) path w, we write wⁱ to refer to the infinite subpath of w starting from the ith vertex (the initial vertex is the 0th vertex). We may now define the semantics of LTL formulas:

1. w |= p (p ∈ Σ) if the label of the initial vertex of w contains p
   
2. w |= φ ∧ ψ if w |= φ and w |= ψ
   
3. w |= ¬ φ if it is not the case that w |= φ
   
4. w |= X φ if w¹ |= φ
   
5. w |= φ U ψ if there exists j ≥ 0 such that w^j |= ψ and for all 0 ≤ i < j, we have wⁱ |= φ
   

We use F φ to abbreviate "true U φ", which says that φ holds in some future. Note that "future" also includes the present. We use G φ to abbreviate ¬ F ¬ φ, which says that φ must hold at all points in the path, i.e., globally. Finally, note that {¬,∧} captures all other boolean connectives, which allows us to freely use any boolean connectives when we write formulas.

How do we use LTL to verify real world systems? The answer requires that we first define the semantics of LTL formulas with respect to Kripke Structures. A Kripke structure K over a finite alphabet Σ is a tuple (S,E,λ: S -> 2^Σ), where S is a set of vertices (or states)and E a set of directed edges on S. It is normally assumed that each vertex in S has at least one outgoing edge. The function λ defines which propositions in Σ are true in a given state. The reader should convince himself that the notion of Kripke structures can be used to model many practical systems. You can first start with traffic lights, in which case &Sigma = {green,red,yellow}, S consists of three states (each corresponding to the event where the light is green, red, or yellow), and E models how traffic lights work (e.g. green -> yellow -> red). A more interesting example includes Dijkstra's algorithm for the dining philosopher problem.

Now, given a state s in structure K, we may define the semantics of LTL formulas: K,s |= φ if for all directed path w in K starting from s, we have w |= φ. For example, if K models traffic lights, then the formulas G( green -> F red ) and G( green -> X yellow ) have to hold in every state of K. [For example, the first formula says that, it is globally true that if the light is presently green, then at some point in the future it will turn red.]

What we are interested in is an algorithm that solves the following model-checking problem: given a Kripke structure K over Σ, a state s in K, and an LTL formula φ over Σ, decide whether K,s |= φ. The problem is PSPACE-complete. The best known algorithm, which runs in 2^O(|φ|) x |K|, was given by Vardi and Wolper by utilizing automata theory on infinite strings. Although the complexity of the algorithm is exponential in the size of the formula, the algorithm runs quite fast in practice because practical specifications are usually short. We shall talk about this algorithm in the near future.

Australia vs. Japan: 3 - 1

Go Aussie!

Game theoretic characterization of treewidth

There is no doubt that the notion of treewidth introduced by Robertson and Seymour is one of the most important concepts in math and computer science introduced in the past thirty years. Roughly speaking, treewidth of a graph G measures how much G looks like a tree. For example, the treewidths of a tree, of a cycle, and of a clique (with n vertices) are respectively 1, 2, and n.

Some of the readers might not be aware of an intuitive way of understanding the concept of treewidths that is provided by the cops-and-robber games, as pointed out by Seymour and Thomas in their paper "Graph searching and a min-max theorem for treewidth", Journal of Combinatorial Theory B, Vol. 58 (1993). The following presentation follows the second paper cited at the bottom. The k-cops-and-robber games, where k > 1, takes a graph G = (V,E) as a parameter. Each game has two players: the cops and the robber. The game goes as follows:

1. In round 0, the cops choose a subset X₀ of V of size at most k. The robber chooses a vertex v₀ of V - X₀.
   
2. In round i+1, the cops choose a subset X_i+1 of V of size at most k. If possible, the robber chooses a vertex v_i+1 of V - X_i+1 such that there is a (possibly empty) path from v_i to v_i+1 which does not pass through X_i ∩ X_i+1. Otherwise, the cops win the game right there.
   

If this game has no end (i.e. the robber can evade capture), then the robber wins. The cops are said to have a winning strategy on the k-cops-and-robber game on G if they can play in such a way that they will eventually win the game. Otherwise, we say that the robber has a winning strategy on this game.

It is helpful to think of the set X_i+1 - X_i as set of vertices above which the cops are hovering in helicopters in round i+1. [This tells us that cops can move from vertices to vertices unrestrictedly.] Also, the set X_i+1 ∩ X_i can be thought of as the vertices where the cops have landed from helicopters. So, it takes two moves for a cop to be at a particular vertex v (i.e. on the ground): she must first ride a helicopter to v, and second land the helicopter at v. On the other hand, a cop may take off to another vertex (but still is in a helicopter) in just one move. In addition, the robber can see the cops in the helicopter, and may elude capture by running at great speed to another vertex as long as he does not run through a cop on the ground during his escape.

Theorem (Seymour and Thomas): A graph G has treewidth ≤ k-1 iff the cops have a winning strategy in the k-cops-and-robber game on G.

Equivalently, a graph G has treewidth k-1 iff k is the smallest number k' such that the cops have a winning strategy in the k'-cops-and-robber game on G. Let's try this game on a tree. The cops can win the game using 2 cops only. The idea is to gradually shrink the set of vertices the robber can go to in the next round by alternately moving the two cops in a "depth-first traversal" manner. On the other hand, it is clear that the robber player has a winning strategy on a tree if he is chased by only a poor lone cop.

In recent years, some researchers in databases and verification have proposed variants of the cops-and-robber games so as to explain some phenomena in those fields. Let me conclude by mentioning two such papers:

1. Gottlob, Leone, and Scarcello. Robbers, marshals, and guards: game theoretic and logical characterization of hypertree width, JCSS 66, 2003.
   
2. Berwanger, Dawar, Hunter, and Kreutzer. DAG-width and Parity Games, STACS 2006.
   

Automatic Structures: Part 2 -- Buchi-Bruyer Theorem

We now concentrate on the proof of Buchi-Bruyer Theorem, probably the most important theorem concerning automatic structures, which says that the set of regular relations coincides with the set of relations definable in M_univ (defined below). By the way, this theorem is folklore in the sense that its proof is unpublished, but well-known to everybody in the community.

We first need some definitions. Suppose that s := (s₁, ...,s_n) ∈ (Σ*)ⁿ. Then, define a string [s] over the alphabet (Σ∪ {#})ⁿ whose length is max{s₁,...,s_n}, and whose ith symbol is (a₁,...,a_n) where a_j is the ith symbol of s_j, if i ≤ |s_j|, and a_j is #, otherwise. One might visualize [s] as the string obtained by placing s₁,...,s_n in a left-aligned column and pad each string s_i with # so that each of the resulting rows is of equal length. After that, we consider this matrix as a string [s] whose jth position is the jth column of the string. A subset S of (Σ*)ⁿ is said to be regular if the set { [s] : s ∈ S } is regular.

Fix an alphabet of size at least two. Consider the infinite structure M_univ := (Σ*, ≤, (L_a)_{a ∈ Σ}, el) where

1. the universe is the set of all Σ-strings,
   
2. x ≤ y iff x is a prefix of y,
   
3. L_a(x) is true iff the rightmost symbol of x is a, and
   
4. el(x,y) is true iff |x| = |y| (|x| denotes the length of x).
   

What properties are (first-order) definable in M_univ? Here are some simple ones:

1. |x| ≤ |y| (i.e. the string x is no longer than the string y),
   
2. |x| = |y| + k for some fixed constant k,
   
3. im-pref(x,y) (i.e. x = y.a for some letter a ∈ Σ), and
   
4. the kth symbol of x is a (where k is fixed and a ∈ Σ).
   

Apologize for the overloading of the symbol '≤' because of the lack of HTML symbols. For example, the first property above can be expressed as

∃ s( s ≤ y ∧ el(x,s) ).

The second property is also easily expressible, but you might need more quantifiers and make use of the relation im-pref. The third property can be expressed by saying that |x| ≤ |y| and there is no z with x < z < y (here '<' is the irreflexive version of the prefix relation ≤).

Now, a subset S of (Σ*)ⁿ is said to be definable in M_univ if there exists a first-order formula φ(x₁,...,x_n) in the vocabulary of M_univ such that

S = { s : M_univ |= φ(s) }.


Theorem (Buchi-Bruyer): A subset S of (Σ*)ⁿ is definable in M_univ iff S is regular.

Proof sketch:
(<=) Suppose that S is recognized by the automaton A = (Q,q₀,F,δ: Q x Σ -> Q), where Q = {q₀,...,q_l} is a finite set of states, q₀ ∈ Q is the initial state, F ⊆ Q is the set of final states, and δ the transition function. So, for all s ∈ (Σ*)ⁿ, s ∈ S iff the string s₁...s_k = [s] is accepted by A,i.e., there exists a run p₀...p_k such that p₀ = q₀, p_k ∈ F, and δ(p_i,s_i+1) = p_i+1. The defining formula for S is

φ(x₁,...,x_n) = ∃v₀,...,v_l( ψ_len ∧ ψ_char ∧ ψ_start ∧ ψ_end ∧ ψ_trans )

where:

1. ψ_len asserts that |v_i| = max{|x_j| : 1 ≤ j ≤ n} + 1.
   
2. ψ_char asserts that [(v₁,...,v_l)] = w₀...w_k is a characteristic sequence, i.e., each v_i is a string of 0s and 1s, and that, for each position h, exactly one of the strings v_is have value 1. [Intuitively, we want each w_j to represent the state p_j in our accepting run.]
   
3. ψ_start asserts that the first position of v₀ has value 1.
   
4. ψ_end asserts that the last position of some v_j, where q_j ∈ F, has value 1.
   
5. ψ_trans asserts that the transition from w_j to w_j+1 respects δ. [This will be a huge table, quite tedious to write down.]
   

The reader should convince herself that all of the above sentences are definable in M_univ.

(=>) The proof is by induction on the formula φ(x₁,...,x_n) defining S. The base case (i.e. atomic formulas) is very easy (left to the reader). Further, the case where φ is of the form ψ₁ ∨ ψ₂ or ¬ ψ follows immediately from the properties that regular languages are closed under union and complementation. What remains is to prove this for the case where φ is of the form ∃x_n+1 ψ(x₁,...,x_n+1). Suppose that the n+1-ary regular relation R defined by ψ is recognized by the automaton A = (Q,q₀,F,δ). To construct an automaton A' for S, one first applies the pumping lemma to show that: there exists a number K such that if (s₁,...,s_n+1) ∈ R, where |s_n+1| > |s_j| for 1 ≤ j ≤ n, then there exists another string s'_n+1 such that (s₁,...,s'_n+1) ∈ R and |s'_n+1| ≤ max{|s_j| : 1 ≤ j ≤ n} + K. We construct A' as follows. First, make K+1 isomorphic copies of A (with different labels), where the ith copy is denoted by Aⁱ = (Qⁱ = {q₀ⁱ,...,q_lⁱ},q₀ⁱ,Fⁱ,δⁱ). The states of A' are the union of the Qⁱs. The start states consist of all the q₀ⁱs. The final states are the union of the Fⁱs. The transition function δ' works as follows: whenever δⁱ(q_jⁱ,(c₁,...,c_n+1)) = q_hⁱ, where c_m ∈ (Σ &cup {#}), we put δ'(q_jⁱ,(c₁,...,c_n) = q_hⁱ. Note that A' is non-deterministic. It is easy to check that A' recognizes S. (QED)

Automatic Structures: Part 1

Several weeks ago, my supervisor Leonid Libkin gave a presentation about automatic structures in our reading group meeting. I would like to talk about these nice animals in some details. This is the first part in the series of posts giving a flavor of automatic structures and sketching some important proofs. If there are interests, I will also talk about how one might apply automatic structures to program verification (this line of research is still under intense development).

Finite model theory primarily concerns finite structures, and has been successfully applied to database theory, and logical approaches to verification (i.e. model checking). On the other hand, finite structures are often too restrictive. For example, when modeling C programs, the use of infinite structures is often inevitable. For this reason, a lot of effort has been put into extending the framework of finite model theory to infinite structures. Several such approaches include metafinite model theory, embedded finite model theory, and automatic structures. In the sequel, we are primarily interested in automatic structures.

Roughly speaking, automatic structures are structures whose universe, and relations can each be represented by a finite automaton. A simple example of automatic structures is Presburger arithmetic (N,+), where N is the set of natural numbers. Here is how one might represent (N,+) using finite automata. Represent the universe N in binary in reverse order (e.g. 4 = 001, 2 = 01); call such a representation bin(N). So, bin(N) is a language over Σ = {0,1}. It is simple to devise a finite automaton that recognizes precisely bin(N). Now, how do we represent the 3-ary relation

+ = { (bin(i),bin(j),bin(k)) : i + j = k, i,j,k ∈ N }

with an automaton? First, it is possible to represent the relation + as a language L over the alphabet {0,1,#}³ defined in the following way. For i,j,k ∈ bin(N), concatenate i,j,k with the padding symbol # so that the resulting strings i',j',k' are of the same length. For example, if i = 001, j = 01, and k = 00001, then i' = 001##, j' = 01###, and k' = 00001. Now, we may treat the tuple (i',j',k') as a string over the alphabet {0,1,#}³, e.g., for i',j',k' in the above example, the resulting string is (0,0,0)(0,1,0)(1,#,0)(#,#,0)(#,#,1). Then, if i + j = k, put the string (i',j',k') in L. Having defined L, it is not hard to exhibit an automaton that recognizes precisely L. [This automaton resembles the commonplace algorithm for addition.]

What is so cool about automatic structures? First, it is somewhat immediate that automatic structures have decidable FO theories. Second, there exists a universal automatic structure M_univ, which is a structure in which all other automatic structures can be interpreted with FO translation (or reduction). Furthermore, the set of all relations definable in M_univ captures precisely all regular relations, which gives an easy way to prove properties about regular languages. By the way, automatic structures also give a nice way of proving that model checking some types of infinite transition systems be decidable.

Anyway, this post was merely intended to whet the reader's appetite. I hope this was enticing enough. In the next post, I will give a precise definition of automatic structures and prove the Buchi-Bruyer theorem that the set of relations definable in M_univ coincides with all regular relations.

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.]