Logicomp

When does Bob deserve to be a co-author?

2008-10-27T06:10:00.000-05:00

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

2008-07-16T14:35:00.002-05:00

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

2008-07-14T10:30:00.001-05:00

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

Finite-variable hierarchy conjecture

2008-07-02T08:47:00.001-05:00

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

2008-06-30T09:03:00.000-05:00

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

2008-06-26T08:08:00.002-05:00

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!

2008-01-14T07:12:00.000-05:00

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:

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.

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

2007-01-10T12:53:00.000-05:00

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

2006-06-22T16:06:00.000-05:00

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)

2006-06-14T15:57:00.000-05:00

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:

w |= p (p ∈ Σ) if the label of the initial vertex of w contains p
w |= φ ∧ ψ if w |= φ and w |= ψ
w |= ¬ φ if it is not the case that w |= φ
w |= X φ if w¹ |= φ
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

2006-06-12T13:30:00.000-05:00

Go Aussie!

Game theoretic characterization of treewidth

2006-05-02T10:42:00.000-05:00

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:

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₀.
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:

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

Automatic Structures: Part 2 -- Buchi-Bruyer Theorem

2006-04-25T12:53:00.000-05:00

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

the universe is the set of all Σ-strings,
x ≤ y iff x is a prefix of y,
L_a(x) is true iff the rightmost symbol of x is a, and
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:

|x| ≤ |y| (i.e. the string x is no longer than the string y),
|x| = |y| + k for some fixed constant k,
im-pref(x,y) (i.e. x = y.a for some letter a ∈ Σ), and
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:

ψ_len asserts that |v_i| = max{|x_j| : 1 ≤ j ≤ n} + 1.
ψ_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.]
ψ_start asserts that the first position of v₀ has value 1.
ψ_end asserts that the last position of some v_j, where q_j ∈ F, has value 1.
ψ_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

2006-04-20T11:42:00.000-05:00

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

2006-03-22T14:04:00.000-05:00

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:

My supervisor Leonid Libkin will give an introduction to Automatic Structures on Thursday, March 23, from 2pm-3pm, UofT St. George Campus, PT378.
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

N is the set of natural numbers, and ‹ the graph of the usual successor function on N.
{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

2006-03-17T12:38:00.000-05:00

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

2006-03-09T13:56:00.000-05:00

"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

It subsumes most modal logics that we use in verification including all the afore-mentioned logics, and
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

2006-03-07T20:36:00.000-05:00

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

2006-03-07T18:07:00.000-05:00

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

New Book on Parameterized Complexity

2006-02-11T13:47:00.000-05:00

Jorg Flum and Martin Grohe just published their new book titled Parameterized Complexity Theory. Flum and Grohe are two giants in finite model theory who have contributed so much towards the development of parameterized complexity theory, especially logical characterizations of parameterized complexity classes. At this moment, one can only purchase the book from Springer as they just appeared some time this week.

I can't compare this book with Downey and Fellow's book as I haven't read Flum and Grohe's. However, I heard from several people who proof-read the book before publications that Flum and Grohe's book is much more well-written and readable than Downey and Fellow's.

How much damage can be caused by a peer reviewer having a bad day?

2006-01-22T12:02:00.000-05:00

Check out this cool article! You will find some hilarious reviews for award-winning papers authored by Dijkstra, Codd, Shannon, etc.

Almost sure theory

2006-01-21T22:01:00.000-05:00

We all know that the Hilbert's Enstceidungsproblem, i.e. deciding whether a first-order sentence is true, is undecidable. Church, Turing, and others proved it. Recall that first-order logic admits the 0-1 law, i.e., every FO sentence is almost surely true (AST) or almost surely false (ASF). So, what about the problem of deciding whether an FO sentence be AST? It turns out that this is decidable. I shall outline some important ideas for proving this statement.

Let us restrict ourselves to graphs as before. In proving that FO admits the 0-1 law, we mentioned the extension axioms EA = {P_k}_{k ∈ N}, where N is the set of all natural numbers. Extension axioms are nothing more than graph properties. In our case, P_ks are FO-expressible. Although for the purpose of this post we need not understand what our extension axioms are, I will just define it for future reference:

∀x₁, ..., x_2k( ∧_{i ≠ j} x_i &ne x_j ->

∃z( ∧_{1 ≤ i ≤ 2k} z ≠ x_i

∧_{i ≤ k} E(z,x_i)

∧_{i > k} ¬E(z,x_i)))

Recall that a theory T is a set of sentences. A model of T is a structure that satisfies all sentences of T. The theory T is consistent if it has a model, and it is complete iff for each sentence f (of the same vocabulary), we have either T |= f, i.e. every model of T is a model of f, or T |= ¬ f. A consistent and complete theory T is decidable if it is possible to decide whether T |= f, for any given sentence f.

Theorem: EA is consistent (and has a unique countable model), complete, and decidable

We will not prove the first two statements, as we will need more model theory (see Libkin's "Elements of Finite Model Theory" for more details). To prove that EA is decidable, we need only invoke an old result from recursive theory that every recursively axiomatizable theory is decidable. The above definition of P_k gives us a recursive enumeration of the axioms.

The unique countable model for EA, denoted RG, is called the random graph, as its probabilistic construction is often emphasized in the literature. Using the above theorem, we derive an easy corollary:

Corollary: For any FO sentence f, RG |= f iff μ(f) = 1.

With these results, it is a breeze to conclude that deciding whether an FO sentence be AST is computable. To determine the exact complexity of the problem, one needs a more hairy analysis, which we will not do here. It turns out that the problem is PSPACE-complete, the proof of which can be found in

E. Granjean. Complexity of the first-order theory of almost all finite structures, Information and Control, Volume 57, 1983.

Recent work in this area mostly deals with determining fragments of second-order logic that admits the 0-1 law, and whether the almost sure theory with respect to the fragment be decidable. [It is easy to see that SO in its full power does not admit the 0-1 law.] This, however, lies outside the scope of our current discussion.

The 0-1 Law

2006-01-07T23:03:00.000-05:00

To start off the year 2006, I want to talk about the 0-1 law, which is an extremely important and elegant topic in finite model theory. A logic L (over a fixed vocabulary σ) is said to admit the 0-1 law if, for any sentence f of L, the fraction of σ-structures with universe {0,...,n-1} that satisfy the sentence f converges to either 0 or 1 as n approaches infinity. We denote this fraction by μ_n(f) and the limit, if exists, by μ(f). [Of course, this means that μ and μ_n ranges between 0 and 1.] In other words, every sentence f is almost surely false or almost surely true. For simplicity, let us restrict our attention to undirected loopless graphs, i.e., σ contains only one binary relation E which is both symmetric and irreflexive. Below is perhaps the most fundamental theorem about the 0-1 law.

Theorem (Fagin 1976, Glebskii et al. 1969): First-order logic admits the 0-1 law

Most finite model theorists equate the admission of 0-1 law with the inability to do "counting". Consider the following properties EVEN = { G : G has even number of vertices }. We see that μ_n(EVEN) = 1 iff n is even, and hence μ(EVEN) does not exist. I am yet to see a property whose asymptotic probability μ converges to something other than 0 or 1, or diverges, but has nothing to do with counting. Consider the following properties:

μ(BIPARTITE) = 0
μ(HAMILTONIAN) = 1
μ(CONNECTED) = 1
μ(TREE) = 0

On the other hand, if you admit constant or function symbols, it is possible to have first-order properties whose asymptotic probability converges to something other than 0 or 1. So, it is crucial to assume that our vocabulary σ be purely relational.

What is the use of 0-1 law in finite model theory apart from the amusement of some theoreticians? [I will have to confess many proofs about the 0-1 law, including Fagin's proof of the above theorem, are usually of great beauty.] Well, a primary concern of finite model theory is to determine how expressive a logic is over a given class of finite structures. By proving that a logic admits the 0-1 law, we show that any property whose asymptotic probability does not converge to either 0 or 1 is not expressible in the logic. For example, an immediate corollary of the above theorem is that first-order logic cannot express EVEN.

Let me briefly outline the proof ideas of the above theorem which recurs in 0-1 law proofs. We only need to show that, for each natural number k, there exists a property P_k of graphs such that

μ(P_k) = 1, and
Any two models of P_k cannot be distinguished by a first-order sentence of quantifier rank k. [Recall that the quantifier rank of a first-order sentence is the maximum depth of any nesting of quantifiers of the sentence.]

Why is this sufficient? Let f be a first-order sentence of quantifier rank k. There are two cases. First, there exists a model of P_k that is also a model of f. In this case, it is not hard to show that any model of P_k is also a model of f, which implies that μ(f) ≥ μ(P_k) = 1. The second case is that all models of P_k are not models of f, i.e., they are models of "not f". Therefore, μ("not f") ≥ μ(P_k) = 1. That is, we have μ(f) = 0.

The property P_k is commonly referred to as an extension axiom. Note that P_k does not have to be L-definable (where L is the logic that is to admit 0-1 law).

Two excellent expositions of the basics of 0-1 laws include Leonid Libkin's Elements of Finite Model Theory chapter 12, and James Lynch DIMACS 1995-1996 Tutorial notes on "Random Finite Models".

Starting the year 2006

2006-01-07T20:08:00.000-05:00

Sorry for having been silent for quite a while. This winter "break" turned out to be quite a busy one for me, with quite a bit of homework and research to do. Anyway, belated happy new year! I hope that this will be a great and productive year for all of us.

I just resumed reading the lattest on the blogsphere, with still quite a bit of catching up to do. For now, I will mention mention a couple of noteworthy things that happened:

Kenny Easwaran wrote an introductory article on "forcing", a well-known technique in set theory for proving independence results. I will write more on it when I finish reading the article.
Igor Naverniouk, a PhD student from University of Toronto, just started a new blog on True Artificial Intelligence. The first couple of entries look quite interesting.

Immerman's descriptive complexity survey

2005-12-19T21:28:00.000-05:00

The most recent issue of SIGACT Newsletter (vol. 36, number 4) contains a guest column concerning progress in descriptive complexity by Neil Immerman. [Thanks to Kurt for making me aware of this article.] The article concisely surveys some recent progress in finite model theory with an emphasis on descriptive complexity. The style is extremely informal, and I believe is a perfect weekend read. I highly recommend the article to anybody interested in logic or computational complexity.

Let me say a little bit about the content of the article (no spoiler!). It starts by motivating the study of descriptive complexity. Then, it moves on to the spectrum problem and Fagin's theorem (that NP = existential second-order logic), which marked the beginning of descriptive complexity. We then see some other capturing results in descriptive complexity (e.g. characterizations of P, PSPACE, etc.). My favorite capturing result mentioned here is DSPACE[n^v] = VAR[v+1], where VAR[k] denotes the set of problems expressible by a sequence of first-order sentences using at most k variables. And so forth ... but let me mention another interesting thing written in the article. We notice that most of the capturing results use a linear ordering on the universe. [In fact, a linear ordering is necessary for these results to work.] For example, Immerman-Vardi theorem says that FO(LFP) captures PTIME over the class of ordered structures. However, FO(LFP) does not capture PTIME over the class of all structures. In fact, a long-standing open problem in finite model theory is whether there exists a logic capturing order-independent PTIME problems. The article nicely surveys our progress towards resolving this problem. Another interesting thing that you will get to know a bit about is the phenomenon that one logic may be exponentially more "succinct" than another logic with the same expressive power.

A fair question to ask now is to what extent has descriptive complexity has helped us to answer structural complexity questions such as separating two complexity classes. Let me try to provide some answers to this question. I believe that the first switching lemma, which separates AC⁰ from LOGSPACE, was proved by Miklos Ajtai using finite model theory. This result was independently discovered by Saxe, Sipser, and Furst around the same time using combinatorics. Most people, even finite model theorists, think that the combinatorial proof provided by Saxe et al. is easier to understand than Ajtai's proof. [Of course, we now have Hastad's switching lemma with some elegant proofs.] Next I will mention Immerman-Szelepscenyi theorem that NSPACE(f(n)) is closed under complementation. Immerman proved this by appealing to descriptive complexity, while Szelepscenyi by using some elementary combinatorics. In this sense, a skeptic might say that descriptive complexity has not really helped structural complexity theory. But, what has? Nothing much really, with expander graphs as one only exception (recall Reingold's recently proved theorem that L = SL). On the other hand, I believe that descriptive complexity helps us understand computational complexity. Many problems or classes in complexity theory have simple and elegant correspondence in descriptive complexity theory. In fact, some logical characterizations of complexity classes are commonly used by computational complexity theorists (e.g. logical characterizations of each level in the poly-time hierarchy). In this sense, I am positive that one day somebody who understands computational complexity, with some help from descriptive complexity, will resolve some of the most tantalizing open problems in structural complexity.

Foundations of XML: Validating XML Documents (1)

2005-12-10T19:10:00.000-05:00

Apologies for my long silence. Things got unexpectedly hectic for me in the past two to three weeks for various reasons. Anyway, as I promised in my previous post, I will further talk about foundations of XML, should the reader be interested. I received two comments expressing interests, one from Jon Cohen, which assure me that at least somebody is going to read this post :-). So, on with our discussion on foundations of XML. Let's spend some time now talking about validation of XML documents. [I am still preparing my post on navigating XML documents and XPath.] In this post, I will talk about a practical validation language that goes by the name of DTD (Document Type Definition).

Roughly speaking, the aim of validation is to ensure that an XML document "makes sense". More precisely, the problem is that, given an XML document (i.e. a labeled unranked tree T) and a statement f in some specification language L, we want to test whether T satisfies f. The most frequently used language L for validation of XML documents is DTD (Document Type Definition). Here, we use a formal model of DTDs that does not incorporate XML "data values", e.g., texts within XML tags (see my previous post). Let us start with an example. As always, we fix a finite alphabet Σ of discourse. Continuing with our example in the previous post, suppose we want to test whether an unranked tree T satisfies the properties:

its root is labeled "books",
every node labeled "books" may have zero or more children labeled "book", and
every node labeled "book" must have four children labeled "title", "author", "year", and "publisher" (in this order), optionally followed by one child labeled "rank".

A DTD that asserts this property is the following:


books     -> book*
book      -> title, author, year, publisher, rank?
title     -> ε
author    -> ε
year      -> ε
publisher -> ε
rank      -> ε

If you have studied regular languages, regular expressions, and context-free grammars, then chances are that you wouldn't have any problem understanding what the previous DTD says. Loosely, each rule (i.e. V -> e, where V is a "label" in Σ and e is a regular expression over Σ) specifies that a V-labeled node in an unranked tree T has children with labels c₁, ..., c_n that can be generated by e. The Kleene star '*' stands for "zero or more". The question mark '?' abbreviates "zero or one". Commas ',' mean "followed by" in the sense of string concatenation. Finally, the symbol 'ε' is the empty string. Therefore, formally, a DTD over Σ is a pair (r,P) where r is the root symbol in Σ and P is a set of rules over Σ such that r does not appear in the "body" of any rules in P (i.e. on the right hand side).

Although DTD is a nice practical specification language for XML, it does not satisfy some nice properties of both practical and theoretical interests. For example, the sets of trees that can be recognized by DTDs are not closed under unions and complementations. [Recall that regular languages are closed under unions, intersection, and complementation (see here for more closure properties of regular languages).] Also, DTDs do not recognize "contexts" (e.g. how do you create a DTD that uses the tag "name" to mean two different things such as "name" of a "book", which should have no children, and "name" of a "person", which should have exactly two children labeled "First Name" and "Last Name"?). Nonetheless, this problem does not seem to bother programmers that much. This explains why DTD is still the most popular XML validation language. However, there are some XML validation languages that address the aforementioned problems. I believe the most popular such language is XSD (XML Schema Definition). We shall consider a formal model of XSD next. We shall later see that XSD has the full power of the yardstick logic for XML validation, which is monadic second-order logic.

Australia qualified for the World Cup 2006 in Germany

2005-11-27T21:25:00.000-05:00

After 30 years of bad luck, Australia has finally qualified for next year's World Cup in Germany after beating Uruguay in a dramatic penalty shoot-out at Sydney's Telstra Stadium, Australia.

XML = Automata + Logic + Database

2005-11-20T10:43:00.000-05:00

What do you get when you mix automata theory, mathematical logic, and database theory in a big bowl, and stir it vigorously? The answer is foundations of XML. In the past 7 - 8 years, the study of XML has generated a large number of elegant and unexpected connections between the three aforementioned areas. How so? Answer: we can view XML documents as labeled unranked trees, and we have numerous formalisms in (tree) automata theory and mathematical logic for querying and manipulating tree-like structures.

I presume you all know a little bit about HTML. XML is just like HTML but you have to define your own tags (e.g. <tag> ... </tag>). According to W3C XML tutorial, unlike HTML, whose primary goal is to display data focusing on how it looks, XML was designed to describe data and to focus on what data is. Well, then, what can you use XML for? Primarily, for information exchange on the web. In fact, one of the greatest promises of XML is to serve as the lingua franca in information exchange. Without further ado, let's look at an example of XML documents:

<books>
    <book>
        <title>Elements of Finite Model Theory</title>
        <author>Leonid Libkin</author>
        <year>2004</year>
        <publisher>Springer</publisher>
        <rank>5/5</rank>
    </book>
    <book>
        <title>Animal Farm</title>
        <author>George Orwell</author>
        <year>2003</year>
        <publisher>Penguin Books</publisher>
    </book>
</books>

One can view this document as a labeled unranked tree:

When we study foundations of XML, we care only about the structure of the tree. Consequently, we omitted the texts within the innermost tags. By definition, this tree is different from the tree that you get from exchanging the two children of "books". That is, a sibling ordering is assumed. Also, note that a node in an XML tree may have an arbitrarily large number of children. This is why the tree is said to be unranked.

We are interested in both procedural formalisms (i.e. automata) and logical formalisms (i.e. logical languages) for querying unranked trees. The intention is that we express the query in a logical language, which will then be converted to an automaton that one can run to compute the query against the XML document.

Of course, we should ask why we want to have query languages in the first place. Some answers are:

Validation - we wish to distinguish XML documents that make sense and those that don't. A common example arises when two parties want to exchange some information using XML documents. They of course have to agree on the formatting of the documents that they accept. Elaborating on the example above, one may insist that "books" have zero or more children with tags "book", each of which must have four children with tags (in order) "title", "author", "year", and "publisher", and one optional child with tags "rank".
Navigation. For example, one may want to ask for all nodes in the document that are tagged "book" and have a child tagged "rank".

For validation, the yardstick logic is monadic second-order logic (MSO). This is because MSO is essentially equivalent to XSD (XML Schema Definition) which people use for validation in practice. For navigation, the yardstick logic is first-order logic (FO). This is because FO and its fragments is closely connected to XPath, a practical XML navigational language which people use.

What kind of procedural formalisms do we have for validation and navigation? For validation, we have what we call nondeterministic unranked tree automaton (NUTA). Its connection to MSO is very tight:

Theorem: A set of unranked trees (over a fixed finite set of labels) is recognizable by a NUTA iff it is definable in MSO.

What about navigation? This is still open.

Another research direction in foundations of XML concerns finding logics, which are equivalent to the yardstick logics, whose model-checking/query evaluation is polynomial in the size of the formula and tree. It is known that both MSO and FO have horrible complexity for model-checking over trees. Research in this direction often requires one to use some kinds of modal logics. For example, we know that CTL* (Computational Tree Logic*) with past operator, which researchers in model-checking community love, is equivalent to FO over unranked trees. There are also other research directions with a plethora of interesting open problems (such as streaming XML documents). If the reader is interested, I will further elaborate on foundations of XML.

Upcoming theory talk at UofT

2005-11-12T07:25:00.000-05:00

For those of you in Toronto, you might want to stop by at UofT next Friday for a talk on P vs. NP. Here is the description:

Title: Can the P vs NP question be independent of the axioms of mathematical reasoning?
Speaker: Shai Ben-David, University of Waterloo
Venue: Galbraith Bld, Rm. 248
Time: 18 November, 11.10 AM
Abstract:
I'll discuss the possibility that the failure to resolve basic complexity theoretic statements stems from these statements being independent of the logical theories that underly our mathematical reasoning. In the first part of the talk, I shall briefly survey independence (from the axioms of set theory) of questions in various areas of mathematics. I shall then go on to discuss independence results that seem relevant to the P vs NP question. Finally, I shall outline some results of myself and Shai Halevi that imply that, as far as current proof techniques for such questions go, the task of proving that P vs NP is independent of Peano Arithmetic is as hard as proving very strong upper bounds on the (deterministic) complexity of the SAT problem.

Favorite Logic of November 2005: Second-Order Logic

2005-11-07T22:56:00.000-05:00

Last month we talked about monadic second-order logic (MSO). We now shall proceed to a more expressive logic: second-order logic (SO) and some of its fragments, such as existential second-order logic (ESO) and universal second-order logic (ASO). In fact, some of the most tantalizing open questions in complexity theory can be reduced to questions about the expressive power of the afore-mentioned logics. More precisely, ESO equals NP, whereas ASO equals coNP. Hence, to separate P from NP, it is sufficient to prove that ASO and ESO have different expressive power. Since we have numerous tools for proving inexpressibility results in finite model theory, it is natural to ask whether it is possible to separate NP from coNP using finite model theory. This, as you would have expected, is still open. However, we have managed to prove a weaker version: that Monadic NP is different from Monadic coNP.

So, what exactly is SO? MSO permits quantifications over sets (i.e. unary relations). SO is just a generalization of this idea: you are allowed to quantify over k-ary relations. So, formulas in SO will look like

ψ := Q₁X₁...Q_mX_m φ

where Q ∈ {∃,∀}, X_i is a k_i-ary "second-order variable" to be interpreted as a k_i-ary relation, and φ is just a first-order (FO) formula that talks about these second-order variables as well as some relations in the given vocabulary. An example of a sentence in this logic has been given in here, in which case all second-order variables are unary. Another example that uses non-unary relations is hamiltonianicity:

∃ L ∃ S ( (L is a strict linear ordering over the vertices) and (S is L's successor relation) and ∀ x ∀ y( S(x,y) -> E(x,y) ) )

A graph is hamiltonian iff there exists a path that visits every vertex in the graph. You can think of L as the transitive closure of the path P that witnesses the hamiltonianicity of the graph, and of S as the path P. [Example: a strict linear ordering on {1,2,3} is the binary relation ≤ = {(1,2),(1,3),(2,3)}, while its successor relation is the binary relation {(1,2),(2,3)}. Perhaps, it is more descriptive to say "immediate successor" than just "successor".] Notice that in these two examples we only used ∃ quantifiers for the second-order variables. We use ESO (read: existential second-order logic) to denote all formulas in SO of this kind, i.e., where all the Q_i is ∃. We use ASO (read: universal second-order logic) to denote formulas in SO where Q_i equals ∀.

Theorem (Fagin 1974): ESO captures NP. ASO captures coNP.

The notion of "capture" here has been defined in a previous post. The examples above give two concrete NP properties (hamiltonianicity, and 3-colorability) that you can express in ESO. How do you express non-hamiltonianicity in ASO? It's simple: just negate the formula above and use the fact that "not ∃ X_i ψ" is equivalent to "∃ X_i not &psi". This can easily be generalized to other coNP properties. Let's summarize the results.

Theorem: NP = coNP iff ESO = ASO iff 3-colorability is expressible in ASO.

What complexity class does SO correspond to?

Theorem (Stockmeyer 1977) SO captures PH.

Actually, Stockmeyer proved a much stronger result relating the kth level in the hierarchy to an SO fragment that contains formulas with k second-order quantifier alternation.

Of course, we have not been successful in proving that ESO != ASO. However, a weaker version has been proven in the literature.

Theorem (Fagin 1975) Monadic NP is different from Monadic coNP.

By monadic NP, we mean ESO formulas all of whose second-order variables are unary. The same goes for monadic coNP. So, monadic NP is just existential monadic second-order logic (EMSO), while monadic coNP is universal MSO (AMSO). The separation query given in Fagin's proof was "graph connectivity"; it is expressible in AMSO, but not in EMSO. A simplified version of this proof has been given in a paper by Ajtai, Fagin, and Stockmeyer (AFS) in 1995. [Correction: the paper is by Fagin, Stockmeyer, and Vardi (FSV) instead. Thanks to Ron Fagin for pointing this out.] In my opinion, this is also the most beatiful proof I have ever seen in finite model theory: simple, but extremely powerful. In a nutshell, this proof cleverly employs hanf-locality (which I have discussed here) which gives us a way of easily providing a winning strategy in "Ehrenfeucht-Fraisse games", which can be used to prove inexpressibility results. Is it possible to generalize the proof technique to ESO? Unfortunately no: Hanf-locality is not useful as soon as we permit binary second-order variables. On the other hand, we still have Ehrenfeucht-Fraisse games, which are in general hard to play. So, FSV proposed the following project: develop tools to easily establish a winning strategy in Ehrenfeucht-Fraisse games! Thus far, most tools of this kind uses some notions of locality, which is only useful for "sparse" structures. I hope that a more powerful tool can be discovered some time in the near future to prove a separation of ESO from ASO, although it seems that we are far from it.

The best way to learn AFS techniques for separating NP and coNP is to read Ron Fagin's

Easier ways to win logical games, DIMACS 1997

It is available from his website. A more complete reference is Leonid Libkin's excellent textbook titled Elements of Finite Model Theory (see chapter (3,4, and) 7).

Lance Fortnow's ComplexityCast

2005-11-07T22:42:00.000-05:00

Check out Lance Fortnow's ComplexityCast, in which he and Bill Gasarch engaged in an after-dinner talk about P vs. NP. I think it's really fun!

NL != P?

2005-11-04T19:46:00.000-05:00

Howdy! It's been some time since I posted last. Being a graduate student, I don't think it is possible for me to post 3 - 4 times per week without sacrificing the quality of the posts. [Maybe, successful bloggers, like Professor Lance Fortnow, would care to tell me how they manage to cope well with both blogging and academic life.] However, my dear readers, rest assured! I do love posting here, and will try to post at least once a week.

Anyway, I just remembered that Stephen Cook told me some time ago that Michael Taitslin claimed to have a proof that NL is different from P, and at that time Steve was checking his proof. His paper can be found here. I am not quite sure of the progress. Incidentally, when I was in Los Alamos a couple of months back, a complexity theorist briefly looked at the paper and told me that it looks "fishy". Of course, in view of the many fallacious proofs that P != NP claimed by some novices (as discussed in here, people often tend to avoid reading "proofs" of this type of statements. Again, I am not sure of Taitslin's "proof". I read the first few pages, and all I can say is that he definitely uses some logic. One thing I can say though is that he has published some nice results in the areas of database theory and finite model theory in well-known journals and conference proceedings. This gives him some credentials, which perhaps will attract some of the readers to read his manuscript and find subtle bugs in his proof or verify the validity of his proof. In any case, if you decide to do so, please keep me informed :-)

Favorite Logic of October 2005: Monadic Second-Order Logic

2005-10-29T11:02:00.000-05:00

previous

We now move to a logic that is much more expressive than FO. In the previous "Favorite Logic" posts, I have talked about the gory details of FO. Now, rather than babble about the current logic under consideration, I shall just sample some results that are particularly interesting from my point of view. The readers that happen to be "inspired" by this post are welcome to send me an email for further results or references.

Monadic second-order logic (MSO) is a natural extension of first-order logic with quantifiers over sets of elements in the universe. More precisely, if σ is a vocabulary, MSO sentences ψ over σ are of the form

ψ := Q₁X₁...Q_mX_m φ

where Q_i ∈ {∃,∀}, X_i is a second-order variable, and φ is an FO sentence over σ ∪ {X_i: 1 ≤ i ≤ m}. So, that's the syntax. I will define the semantics by means of an example, the reader should be able to generalize easily.

Suppose σ = {E} is just a vocabulary with one binary relation symbol. We wish to express 2-colorability, i.e., the property

2COL = { G : G is a 2-colorable graph }

It can be proved that 2COL is inexpressible in FO. But, is it expressible in MSO? Positive.

∃ X ∃ Y( (X and Y partitions the vertex-set) and (any two adjacent vertices cannot both belong to X or Y) )

Suppose we are given a graph G = (V,E). Then, we can evaluate this formula as follows: this formula is true in G iff there exist unary relations (i.e. sets) X and Y over G (i.e. X, Y ⊆ V) such that the body of this formula evaluates to true in the structure (V,E,X,Y) (i.e. iff G is 2-colorable). In this case, we intend X and Y to correspond to the two color classes that partition the vertex-set.
The first conjunct above can be expressed by the FO sentence ∀x( X(x) <-> Y(x) ). As an exercise, the reader might enjoy coming up with an FO formula that expresses the second conjunct.

In fact, we can use the same trick to express k-colorability in MSO. Hence, we can immediately conclude that model-checking for MSO is NP-hard when only the models are part of the input (i.e. data-complexity is NP-hard). In fact, since MSO sentences are closed under negation, we also conclude that non-k-colorability is in MSO and therefore model-checking is coNP-hard as well.

Let's conclude this post with a beatiful result that connects MSO to formal language theory. The proof of the result can be found in Straubing's monograph

Finite Automata, Formal Logic, and Circuit Complexity

[Incidentally, David Molnar had a nice post that explores the connection between Straubing's result on "simulating monoids" and homomorphic cryptosystems. So, I thought it would be nice to mention a result from his book, although it was originally proven by Buchi in 1960s.] Roughly speaking, the result says:

A language (a set of strings) L is regular iff L is MSO-definable

What does it mean for a language to be MSO-definable? For notational convenience, let's restrict ourselves to the alphabet {0,1}. First, a binary string s = s₀...s_n-1 can be considered as a logical structure

S(s) := ({0,...,n-1}; <, U)

whose universe is {0,...,n-1} encoding the "positions" of the string, < is interpreted as the usual linear ordering over such universe, and U is a unary relation with the interpretation that i ∈ U iff s_i=1. So, if S(s) is a logical encoding of a string s and φ is a formula over the vocabulary {<,U}, the notion of 'S(s) |= φ' makes sense. The language defined by φ, then, is

{ s ∈ {0,1}^* : S(s) |= φ }

Buchi's result says that MSO-definable languages are precisely regular languages. Doner, Thatcher, and Wright extended this result to trees:

A set of trees is regular iff it is definable in MSO.

These days, this result is widely employed in the area of "Foundations of XML", which have put automata, logic, and complexity theory under the same roof, which is no short of wondrous. If this interests you, take a loot at some surveys in here.

Let's play games

2005-10-24T17:02:00.001-05:00

About a month ago I saved a draft on the complexity of games in finite model theory. Suddenly, this morning David Eppstein left a comment on my previous post, which reminded me about this draft. Incidentally, I have been a fan of his recreational math pages, especially the combinatorial game theory page, since two years ago, after taking a course on the theory of computation. Anyway, let's play some games now! The games that we will play are not something I invent myself ;-). They are actually pervasive in finite model theory.

Here is the description. Two graphs G and G', and a natural number k are given. There are two players in this game, Spoiler and Duplicator. They will play for k rounds. In the i'th round (1 ≤ i ≤ k), Spoiler starts by picking a vertex in one of the graphs. Then, Duplicator will have to respond by picking a vertex in the other graph. After k rounds have been played, we obtain the vertices a₀, ..., a_k of G, and the vertices b₀, ..., b_k of G'. Duplicator is declared to be the winner if the subgraphs of G and G' that are induced by a_i's and b_j's are isomorphic. Otherwise, Spoiler wins. By the way, why are the players called Spoiler and Duplicator? If you think about this, Spoiler's goal is to show that the two graphs are not isomorphic (i.e. to spoil), while Duplicator's goal is to show that the two graphs are isomorphic by matching (or "duplicating") each of Spoiler's moves in such a way no difference in the two graphs are revealed. So, Duplicator is the "good" guy, while Spoiler is the "bad" guy. Duplicator has a winning strategy on this game if no matter how Spoiler moves in the i'th round, Duplicator can always find a move that will guarantee a "win" for Duplicator.

The problem is, given G, G', and k, decide whether Duplicator has a winning strategy. Determine its complexity! I will post the solution and some open problems later.

But, let me give you a simple example. Suppose G = K_k and G' = K_k+1. Then, it is easy to see that Duplicator has a winning strategy for the i-round game, where 0 ≤ i ≤ k (why?). However, a moment's thought will reveal that, for any i-round game on G and G' where i > k, Spoiler has a winning strategy. Where G and G' are more complicated structures, it becomes harder to decide whether Duplicator has a winning strategy.

Some links of interests

2005-10-23T17:42:00.000-05:00

I have just added some new links to several interesting blogs to my blogroll: David Molnar's blog, Kurt Van Etten's, and Scott Aaronson's (the complexity zoo keeper). It's great to see that the blogging community grows very well. This comes at one price however: there is just no time to visit regularly every single interesting blog there is. There are just too many good ones these days!

Also, I have recently discovered a nice-looking online textbook on 'universal algebra'. I haven't read it yet, though. But, it has some nice applications to computer science (automata theory, rewriting systems, etc.) and model theory. If you are a complexity theorist, a motivation to look at this book may be Straubing's monograph

Finite Automata, Formal Logic, and Circuit Complexity (Progress in Theoretical Computer Science), Springer, 1994.

In this monograph, Straubing demonstrates the possibility of attacking tantalizing open problems in circuit complexity using automata theory, semigroup theory, and finite model theory. In fact, I have heard a rumour that Straubing very recently proved a separation result in complexity theory using this technique ...

Strange things happen

2005-10-22T19:44:00.000-05:00

Around this time last year I was busy preparing my applications to PhD programs in the U.K. and North America. In particular, University of Cambridge, which happened to be one of those universities I was interested in , requires each applicant to write a short research proposal. [As you of course know, I chose University of Toronto, which was my first preference all along.] So, I had a discussion with Anuj Dawar, who was the finite model theorist at Cambridge I wished to work with, on what sort of research directions to pursue for PhD studies. He gave me two research problems:

Homomorphism preservation theorem in the finite.
Do order-invariant FO properties have the zero-one law?

Don't worry if you don't know what they mean. The important thing to know is that both of these problems are long-standing open problems in the area. Both of these problems looked formidable to me then (and they still do now), and so I didn't bother thinking about them. Anyway, to my surprise, both of these problems have been resolved this year in quick succession. The first problem was solved positively by Benjamin Rossman, who this year just started his graduate school. His paper titled

Existential Positive Types and Preservation Under Homomorphisms

was recently published in this year's LICS proceeding and awarded Kleene's award for the best student paper. [Congratulation Ben!] You can find his paper on his web site. The second problem was very recently solved by Leonid Libkin, my supervisor. You have to wait if you want to get the paper.

I wish I had collaborated with these guys on these problems. D'oh!

Special Programmes on Logic and Algorithms in Cambridge

2005-10-20T19:49:00.000-05:00

During the first half of next year, there will be a series of workshops on Logic and Algorithms (broadly construed) at Isaac Newton Institute for Mathematical Sciences (Cambridge). Looking at their workshop titles is enough to convince ourselves that there is something for everyone:

Finite and Algorithmic Model Theory (9-13 January).

Logic and Databases (27 February - 3 March).

Mathematics of Constraint Satisfaction: Algebra, Logic, and Graph Theory (20-24 March).

New Directions in Proof Complexity (10-13 April).

Constraints and Verification (8-12 May).

Games and Verification (3-7 July).

There will be quite a number of invited speakers from University of Toronto. They include Stephen Cook, Leonid Libkin, and Toniann Pitassi.

Logics capturing complexity classes

2005-10-17T16:59:00.000-05:00

David Molnar asked a good question: (in my words) what does it mean to have a logic for a complexity class over ordered structures and over all (i.e. both ordered and unordered) structures? To answer this question, I will have to define what it means for a logic to capture a complexity class. As always, I assume that you have read preliminaries 1 and 2, which can be accessed from the sidebar. [Please let me know if your browser has any problem displaying the symbols.]

We will first recall the definition of "expressibility" of a property in a logic. Suppose we are given a σ-property (or boolean query) Q over a class C of σ-structures, i.e., Q is just a subset of C. Then, Q is said to be expressible in a logic L over C if there exists an L-sentence f such that, for any A ∈ C, A ∈ Q iff A |= f. When C is not mentioned, C is assumed to be the class of all finite σ-structures.

Observe that one can think of boolean queries as an analogue of the notion of languages, in the sense of formal language theory, or, more loosely, "computational problems". For example, consider the problem of testing hamiltonianicity of a graph. We can think of this problem as a boolean query H over the graph vocabulary such that a (finite) graph is in H iff it is hamiltonian. As a matter of fact, it is possible to encode any σ-structure as a (binary) string, and a string as a τ-structure for some vocabulary τ. Therefore, we can view any σ-boolean query as a language, and vice versa. So, we may redefine any complexity class K to be the set of all σ-properties that are computable in K, where σ ranges over all relational vocabularies. Hence, PTIME is the set of boolean queries that are computable in polynomial-time. For convenience, given a class C of structures, we also define K_C to be the set of properties Q that are computable in K, when we restrict the input to Q to be all structures in C that have the same vocabulary as Q. When C is not mentioned, we assume C to be the set of all finite structures.

We are now ready to define the most important definition in descriptive complexity. A logic L is said to capture a complexity class K over a class C of finite structures if for any Q ∈ C: Q ∈ K_C iff Q is expressible in L over C. Again, when C is not mentioned, it is assumed to be the set of all finite structures.

We know that existential second-order logic (ESO) captures NP. This is Fagin's result, which was discussed in Lance's blog recently. On the other hand, it is open whether there exists a logic that captures PTIME. We know, however, that there exists a logic (FO+LFP: first-order logic + least fixed point operator) that captures PTIME over all ordered structures. [Ordered structures mean that, we assume a binary relation in the structure to be interpreted as a total linear ordering on the universe.] This result was proven independently by Neil Immerman and Moshe Vardi in the 80's. You might be wondering whether FO+LFP captures PTIME. The answer is no: even testing whether a graph has an even number of elements cannot be done in FO+LFP without the help of an "external" linear order. The question whether there exists a logic for PTIME was first raised by Chandra and Harel in the 70's. Also, as I mentioned in a previous post, Yuri Gurevich conjectured that there is no logic for P (and this will imply that P ≠ NP). On a related note, it is also open whether there is a logic for any important complexity class below NP such as PTIME, L, NL, etc.

A relevant question is the following: why do we want to have a logic that capture complexity classes over all finite structures (not just over ordered structures)? The answer is technical: linear orderings make an inexpressibility proof more complicated by an order of magnitude!

Fun Proof Techniques

2005-10-15T17:10:00.000-05:00

About three years ago, I took a course on the theory of computation. I remember that during the second lecture, our instructor introduced us to the mathematical background, and in particular proof techniques. He started saying "in mathematics, we have proof by induction, proof by construction, and proof by contradiction ...". Before he finished the lecture, he presented to us a list of fun proof techniques which work in practice, some of which are listed here. My favorite ones are:

Proof by blatant assertion: this is marked by expressions like "obviously", "trivially", "any moron can see that".
Proof by example: you sketch a proof that the theorem is true for n = 4, and claim that this proof generalizes to all n.
Proof by picture: picture + handwaving makes a pretty compelling argument in a classroom.
Proof by omission: we state the theorem and the proof is left as an exercise for the reader.
Proof by accumulated evidence: for three decades we have worked very hard to produce an efficient algorithm for NP-complete problems without results; therefore P != NP.
Proof by reference to famous people: I saw Karp on the elevator, and he thought that our problem is NP-complete!
Proof by confusion: P = NP <=> P - NP = 0 <=> P(1-N) = 0 <=> P = 0 or N = 1; but the last expression is false and therefore P != NP.

What are your favorite proof techniques?

An approach to prove P != NP

2005-10-15T11:27:00.000-05:00

Let K be a complexity class. We wish to recursively enumerate exactly those "graph languages" that can be decided in K. By graph languages, we mean languages whose inputs are graphs (say in adjacency matrix format) such that two isomorphic graphs are either both in the language or both not in the language. So, graph languages are "closed under isomorphisms". If this can be done for K, we say that the set of K graph properties is recursively indexable.

The set of NP graph properties is known to be recursively indexable. This is due to the fact that we have a logic for NP (i.e. existential second-order logic). On the other hand, it is a long-standing open problem whether P graph properties are recursively indexable. [No, you can't use the usual enumeration for clocked poly-time Turing machines as they contain "bad" graph languages.] Of course, the existence of a logic for P, which is another big open problem in finite model theory, will imply that P graph properties are recursively indexable. [(LFP+<)_inv captures PTIME properties over ordered structures only.] Yuri Gurevich conjectured that P graph properties are not recursively indexable, and therefore, there is no logic for P. See his paper. In particular, if the conjecture is true, then P is different from NP as NP graph properties are recursively indexable! So, try to prove that P graph properties are not recursively indexable!

Favorite Logic of September 2005: First-order Logic (3)

2005-10-13T21:17:00.000-05:00

previous|
next

We are somewhat behind our schedule. So, let's close it out now. This post concludes our series of posts on first-order logic as the favorite logic of last month (oops!). I will give a glimpse of the expressiveness of first-order logic, and tools for showing inexpressibility results. The literature on this topic is so vast that it is impossible to cover all possible results and tools; so, I will mention only a selection of results and tools, and give examples on how to apply the tools mentioned. Also, see the preliminaries before reading this post.

Let's get right down to business. Our main problem can be described as follows: suppose Q is a σ-property (i.e. boolean query), and we want to know whether there exists a first-order sentence that defines Q. If there is one, then it suffices to come up with a sentence f that defines Q. If not, what shall we do?

Well ... in model theory, we have a plethora of tools in our toolbox:

Compactness: a theory T is consistent iff every finite subset of T is consistent.
(Restricted form of) Lowenheim-Skolem: If a theory has an infinite model, then it has a countable model.

Let's try compactness on an example. Suppose we want to show that the property GC testing graph connectivity is not first-order definable. Suppose to the contrary that f defines GC. Then, consider the theory T = {f} ∪ { π_n : n is positive nat. number } where π_n is the first-order sentence

∃x∃y( there is no path of length n from x to y )

Clearly, this sentence is first-order. By compactness, it is easy to show that T is consistent (just take the biggest n for which π_n appears in this finite subset of T and "elongate" the path from x to y by increasing the number of elements in the universe). So, we have a model M for T. But in M, x and y are not connected by a (finite) path, contradicting f. Therefore, f cannot be a first-order sentence.

That's short and simple! The problem, however, is that this doesn't prove that FO cannot express GC in the finite (i.e. the ground set of GC is restricted to all finite graphs only), as compactness theorem fails in the finite. So, how do we prove that GC cannot be expressed in the finite? It is a sad fact that most of the tools from model theory fails in the finite. Some of the few that survive include Ehrenfeucht-Fraisse game theorem, Gaifmann-locality, and Hanf-locality. Here we shall use the notion of Hanf-locality to prove that GC is not FO definable.

Let me try to intuitively illustrate the notion of Hanf-locality for graphs. A graph property P (over all finite structures) is said to be hanf-local if there exists a number d such that for every two finite graphs A and B:

that A and B d-locally look the same implies that A and B agree on P.

The smallest such number d is called hanf-locality rank of P. What do we mean by "d-locally look the same"? A and B d-locally look the same if there exists a bijection g from V(A) to V(B), the vertices of A and B, such that for every c in V(A) there exists an isomorphism from the d-neighborhood of A around c to the d-neighborhood of B around g(c) which maps c to g(c). That is, if you have only limited local vision (say up to d distance) and if you pick a spot c in the graph A, I can always give you another spot in the graph B (via the bijection) such that you cannot see the difference between your surroundings on these two different spots.

Now, our strategy for proving that GC is not first-order expressible is:

Show that every first-order definable query is hanf-local.
Show that GC is not hanf-local.

We won't prove item 1. We will however sketch how to prove item 2. Suppose GC is hanf-local with rank d. Then, define two graphs G and G' as follows. Take a number p >> d. G is a cycle with 2p nodes, and G' is a disjoint union of cycles each with p nodes. You can easily check that there is only one type of d-neighborhood (up to isomorphism) around any vertex c in G and G', i.e., the 2d+1-path with c right in the middle. So, just take any arbitrary bijection between G and G' to show that they d-locally look the same. However, G is connected but G' is not, contradicting the assumption that GC is hanf-local!

I would love to talk about Ehrenfeucht-Fraisse games and Gaifmann locality, which are equally important tools in finite model theory for proving FO inexpressibility. Sadly, this will only make this post longer than it already is. So, I will refer you to Leonid Libkin's Elements of Finite Model Theory for more on this (and also for the proper acknowledgement of these results!).

Happy Thanksgiving!

2005-10-11T15:04:00.000-05:00

Most of you in the U.S. might probably be bewildered by what I'm saying. However, yesterday was a thanksgiving day in Canada. This was my first encounter of any kind of "thanksgiving day" in my entire life as I am from Australia.

Anyway, I guess I will have to get used to this custom as I will be here for another 5 years. So, happy thanksgiving! Thanks to all of you who have left useful comments on my blog. I do learn a lot from all these comments.

Lance's Recent Post on Fagin's Theorem

2005-10-11T10:14:00.000-05:00

Lance Fortnow posted his favorite theorem of this month on his blog: it's Fagin's theorem, one of the most important results (and the first of its kind) in descriptive complexity theory. Nice!

Favorite Logic of September 2005: First-order Logic (2)

2005-10-10T15:45:00.000-05:00

(previous|next)

Howdy! Today we will resume on our discussion of first-order logic. In particular, we will talk about model-checking.

Diving right in ... the problem is as follows: given a finite structure M and an FO formula f, we want to test whether M |= f, i.e., f is true in M. Immediately, I hear you say that this problem is trivially decidable as we can use the inductive definition of M |= f to do the testing. Well ... it is decidable, but we want to know its complexity. We won't talk about how to represent M, although it matters in this case, as we will only mention results. You can represent f in any way you like, e.g., the parse tree for f.

There are three common measures for the complexity of this problem:

Data Complexity: the input is M (i.e. f is fixed). So, we measure the performance of any algorithm for the problem in terms of |M| only.
Expression complexity: the input is f (i.e. M is fixed).
Combined complexity: the input is (M,f).

Data complexity measure is commonly used in the field of databases, where usually M is very big and the query f is small. Combined complexity and expression complexity measure is commonly used in the area of verification (commonly called model-checking), where f can be very large and complex. If the reader is curious about any of these areas, I will gladly recommend "Foundations of Databases" by Abiteboul et al. and "Logic in Computer Science" by Huth et al.

It is not hard to analyze the running time of the algorithm for testing M |= f induced by the usual inductive definition of |=. You will get O(|f| x |M|^k) where k is the width of f, i.e., the maximum number of free variables in every subformula of f. So, k does depend on f. That is, the algorithm runs polynomial in |M| but exponential in |f|. In fact, one can show that the data complexity of this problem with respect to FO is AC^0, where as the expression and combined complexity is PSPACE-complete. As an exercise, the reader might want to try to prove the latter as it is quite simple (hint: reduce the problem QBF).

Papadimitriou and Yannakakis have an interesting paper that refines these complexity measures using the theory of parameterized complexity. The motivation of this paper is the following: although |f| << |M|, the fact that |f| is an exponent of |M| is no good because even for "small" |f|, say |f| = 20, an algorithm that runs in O(n^20) cannot be considered tractable (especially when n is really big, like in database applications). So, the question then is whether it is possible to have an algorithm for testing M |= f that runs in g(|f|)|M|^c where g is a function from natural numbers to natural numbers, and c is a constant independent of both |M| and |f|. The result of this paper essentially stipulates that any algorithm for evaluating M |= f must have |f| as an exponent of |M|, unless the W hierarchy collapses. See the following reference if interested:

On Complexity of Database Queries, Papadimitriou and Yannakakis, JCSS, Vol 58, 1999.

We will next talk about the expressive power of FO.

Bugs!

2005-10-01T17:52:00.000-05:00

I have just spent about two hours writing about the second part of favourite logic of september 2005 and, when I saved it as a draft, my firefox just freezed and all the text got erased. Ah well. In view of this and that there is no working computers in my office, I think I will just start posting when I get my powerbook back, which is next week.

P vs. NP: let's think out loud

2005-09-24T08:30:00.000-05:00

We all know this question. It is listed as one of the seven millenium problem by Clay Mathematic Institute. We also know that most people believe that P is different from NP. For example, in the P vs. NP Poll by Gasarch (published in ACM SIGACT Newsletter), out of the 77 people who offered opinion, 61 believed that P is different from NP, 9 believed that P = NP, and others believed that the question is "formally independent" in some form. Well, what do you believe? If you are as yet undecided, I will try to unravel the reasons why most people believe that P is different from NP, and then speak about why it is equally reasonable to believe that P = NP. I will not talk about whether P vs. NP is formally independent of ZFC.

Two most common reasons for believing that P is different from NP are the following:

There are (literally) tons of problems which are NP-complete (i.e. if one is in P, and all will be in P), and nobody has been able to devise any polynomial-time algorithm for any of these problems. However, from our experience, we know that we are "good" at devising polynomial-time algorithms, but not very good at proving lower bounds. [Just look at all the great
algorithms we have devised. Also witness that we can't even prove that satisfiability for propositional logic cannot be solved in O(n²).]
We can intuitively think of P as the set of problems for which we can produce proofs in polynomial time, and of NP as the set of problems for which, given a proof, we can check that it is indeed a proof in polynomial time. Well, from our experience with math, we know that producing proofs is usually much harder than verifying proofs.

Well, both of these reasons sound very reasonable. However, I also think that there are holes in these arguments (because of which, it is equally reasonable to believe that P = NP). Most people associate the complexity class P with the set of problems that we can solve "efficiently", and classify non-polynomial algorithms as bad (or inefficient) algorithms. [If you have done some computer science courses, you should see this immediately.] But this is a wrong assumption. For example, the Simplex algorithm for solving linear programming runs in exponential time in the worst case (I believe the same is true in average case), but the algorithm runs very efficiently in practice. There are also polynomial-time algorithms for linear programming, but it seems that none of those have outperformed the simplex algorithm in practice. Furthermore, the exponentiallity of the simplex algorithm's running time only occurs on some pathological examples that never appear in practice. On the other hand, there are many polynomial-time algorithms that do not actually run efficiently in practice. A counterexample for this (quoting Cook's paper) is due to a result by Robertson-Seymour that says that every minor closed family of graphs can be recognized in O(n³), but the hidden constant is so huge that the algorithm is inefficient in practice.

So, maybe there exist polynomial-time algorithms for satisfiability for propositional logic, it's just that the smallest exponents are so big (maybe bigger than the number of atoms in the visible universe, 10⁹⁰). [Of course, the time hierarchy theorem tells us that there is an problem solvable in n^k, but not solvable in n^k-1.] Perhaps, the smallest size of the polynomial-time algorithm that solve satisfiability for propositional logic already outnumbers 10⁹⁰. Who knows! Perhaps, we are good at devising efficient algorithms, but not so good at devising polynomial-time algorithms in general. Maybe the following question is more relevant: assuming that P = NP, give an upper bound on the size of the algorithm (by this I mean, multi-tape Turing Machine) that solves satisfiability in polynomial-time; does it necessarily consist 10, 100, or 10⁹⁰ states?

In a sense, if you're a practical-minded person, P vs. NP doesn't really matter at all, and there is technical reason why. Recall that the linear speedup theorem (look at Papadimitriou's Computational Complexity) says that if a problem is solvable in `f(n)`, then for any `epsilon > 0`, there exists an algorithm that solves the same problem which runs in `epsilon f(n) + n + 2`. So, if your algorithm runs in 2ⁿ, then just use this theorem to speed up your algorithm for all n that is relevant in practice. [Of course, if you check the proof, the size of the resulting algorithm grows quite so quickly in the size of `n`, that there is no way you can write your algorithm on earth. So, the practically-minded people will probably settle with heuristics instead.]

Anyway, I think that it is very possible [correction: 'very' -> 'equally'] that P equals NP, and the proof of which is non-constructive (or we may never actually find the proof, because the length of the shortest possible proofs exceeds the number of atoms in the visible universe).

Toronto's temperature: the extremes

2005-09-23T21:43:00.000-05:00

The last couple of weeks have been quite hot in Toronto (mostly around 25 degrees C). I actually heard that this is unusually hot for September in Toronto. The humidity just makes it worse. You'll find yourself taking a shower three to four times per day.

Since last night, Toronto's temperature has cooled off quite a bit. Throughout today it's been around 18 degree C, just the perfect temperature. I wish it would be like this all year round. But that was just wishful thinking, because I have to be prepared for -20 degrees C in December and January. Actually somebody told me that during winter in Toronto, the wind can be quite strong. This will just make it worse ...

Favorite Logic of September 2005: First-order logic (1)

2005-09-23T20:30:00.000-05:00

next

Some time ago I promised to make a series of postings on "My Favourite Logic of The Month" every month starting from September 2005. Well, here we officially start until we run out of "nice" logics.

Why first-order logic (FO)? It is the simplest non-trivial logic that we can use to express many mathematical statements. In fact, it is believed that first-order set theory is sufficient to axiomatize mathematics. Besides, most of you have already been exposed to FO, which will make my task much simpler. If any terminologies here sound obscure, check out preliminaries.

We will take a look at three aspects of FO: (1) the problem of testing satisfiability and finite satisfiability, (2) model-checking, and (3) expressive power. I am trying to cover topics that hopefully satisfy finite model theorists, and other logicians. In this posting, I will only speak about (1), saving the other two for some time next week.

Satisfiability: given an FO formula, test whether it is satisfiable. Well, what can we say about this problem with respect to FO? It is undecidable (actually r.e.-complete) [correction: complete for co-r.e, thanks to Richard Zach.]; this is a well-known result proven by Turing, which shattered Hilbert's dream to axiomatize mathematics. If you're into this kind of problem, check out the following book

The Classical Decision Problem by Grädel et al.

Actually, many fragments of FO are decidable, but most are provably intractable. The most complicated such result that I know of is Rabin's result of the decidability of monadic second order theory of infinite binary tree. [Whatever this means, but we may want to delve into this awesome result in the near future.] Although decidable, the problem has non-elementary complexity.

Finite Satisfiability: given an FO formula, test whether it has a finite model. I believe that this problem, if decidable, has more practical applications, e.g., databases. Unfortunately, this problem is also undecidable (actually complete for co-r.e.) [correction: complete for r.e.]. This result is due to Trakhtenbrot. Combining this result and that satisfiability is complete for co-r.e., we can readily imply that completeness theorem, which says that satisfiability is r.e. [correction: satisfiability is co-r.e., thanks to Richard Zach.], fails in the finite. Trakhtenbrot's result in fact marks the beginning of finite model theory. Later on, Fagin proved a logical characterization of NP with a technique that is "isomorphic" to that used to prove Trakhtenbrot's theorem (see this page). For more on finite satisfiability of FO, see Libkin's Elements of Finite Model Theory.

CAPTCHA

2005-09-08T09:17:00.000-05:00

It stands for Completely Automated Public Turing Test to Tell Computers and Humans Apart. Although I still wonder why it is abbreviated CAPTCHA instead of CAPTTTCHA, it was (re)brought to my attention due to the spam I got for my posting yesterday. Anyway, CAPTCHA is developed by researchers from Carnegie Mellon University. Here is their main website. Briefly, the goal of CAPTCHA project is to use Artificial Intelligence to help internet security (e.g. to prevent spams). The underlying assumption behind CAPTCHA is that there are tasks that humans can do, but computers can't. For example, since I enabled the word verification (from CAPTCHA project), each time you wish leave a comment on this blog, you will be asked to read and verify a distorted text (which is an image file). Although the task seems trivial to humans, tasks like this are non-trivial for computers (at least for now). We don't know whether computers will someday possess our ''intelligence''. But CAPTCHA is one reason why a 'no' answer will have positive impact on our society.

Ironically, the distorted texts are actually generated by computers ...

Back!

2005-09-07T21:44:00.000-05:00

Hello all! It's been quite some time since I blogged last. But I am happy to inform you that I can start blogging again on a regular basis.

A little bit about my summer internship in Los Alamos ... I'll start with my work in Los Alamos. I worked mostly on the complexity aspect of Sequential Dynamical Systems (SDS). Briefly, SDSs are a formal model of computer simulation (somewhat like cellular automata) proposed by Los Alamos researchers. I won't tell you more about it (if you are curious as to what they are, read this survey). Anyway, in retrospect Los Alamos was a nice place to visit. The scenery was awesome, the people were friendly, and you can do some cool research there. [Fortunately, what Jon said didn't happen to me or any of my friends.] The down side, however, is that there is pretty much nothing else in Los Alamos. The town is practically dead after 6 --- there is virtually nobody walking on the street. And ... to my surprise, there was no shopping mall whatsoever in Los Alamos. One has to go to Santa Fe, which is the closest biggest city to Los Alamos, to find the nearest shopping mall. Anyway, I will put some pictures from my stay in Los Alamos when I finish developing the pictures.

It is a nice feeling to know that I will be doing logic on a regular basis from this time onwards. I arrived in Toronto last Saturday to start my graduate studies. I haven't completely settled yet, but I couldn't help myself blogging again after the internet connection was set up in my apartment here. Incidentally, this week is Toronto's Computer Science Department's orientation week. I am so happy to meet many logicians here, including some of the most well-known ones. For instance, Moshe Vardi (Rice University) came to visit this Tuesday and gave a talk outlining the development of logic and how computer science was born. I, and I believe most people in the audience (including the non-logicians), found the talk extremely entertaining and insightful. As my advisor, Leonid Libkin, put it this morning, Vardi has the rare gift to be both a top-notch researcher and an excellent speaker. [As you and I know, most researchers who do great research are poor at explaining their research to others.]

Anyhow, that is all I have for now. As a final remark, I haven't forgotten about my favourite logic of the month and will write on it some time next week after I have completely settled.

Interning in Los Alamos National Laboratory

2005-06-07T18:14:00.000-05:00

Howdy! I have just recently started a summer research internship in Los Alamos National Laboratory. As my summer research topic is not directly related to logic, I will probably have to switch to a hibernation mode as far as blogging Logicomp is concerned. I will definitely resume with Logicomp when I start my graduate studies in Toronto (early September). One interesting thing that I plan to post on Logicomp in the future is the "Favorite Logic of the Month" in which I will mention my favorite logic of that month and a general method for proving (in)expressibility.

Anyway, until then I hope everyone have a great time!

Nice finite model theory course notes

2005-05-30T00:02:00.000-05:00

I have recently found nice introductory course notes on finite model theory. You can find it here. Thanks to the author for making the notes publicly available.

No compactness in finite model theory

2005-05-29T23:15:00.000-05:00

The compactness theorem for first-order logic is indisputably the most fundamental theorem in model theory. It says that

A theory has a model iff every finite subset of it has a model

I will say no more about the usefulness of this theorem in model theory. But what I will speak about now is the failure of compactness in finite model theory, as I already remarked before.

In finite model theory (FMT), we are only concerned with finite structures. Hence compactness theorem in FMT would read

A theory has a finite model iff every subset of it has a finite model

It is easy to conjure a counterexample for this statement. Consider the first-order theory `T` over the empty vocabulary containing sentences of the following form (for all `k >= 2`):

`S_k = EE x_1,...,x_k( x_1 != x_2 ^^ x_1 != x_3 ^^ cdots ^^ x_{k-1} != x_k )`

It is easy to see that every subset `T'` of `T` has a finite model; if `n` is the largest integer such that `S_n in T'`, then the structure containing `n` elements satisfies `T'`. It is also easy to see that `T` has no finite model. (QED)

Likewise, many other fundamental theorems in model theory, such as Craig Interpolation Theorem, are also casualties of finitization (more on this later); Ehrenfeucht-Fraisse games being the only general tool available for proving inexpressibility results in finite model theory.

Finite Model Theory: Preliminaries (2)

2005-05-28T19:23:00.000-05:00

We now focus on a very important concept in finite model theory: `k`-ary queries. In fact, one goal of finite model theory is to establish a useful, if possible complete, criterion for determining expressibility (ie, definability) of a query in a logic (such as, first-order logic) on finite structures. For example, we may ask if the query connectivity for finite graphs, which asks whether a finite graph is connected, is expressible in first-order logic. The answer is 'no', though we won't prove this now. [Curious readers are referred to Libkin's Elements of Finite Model Theory or Fagin's excellent survey paper.]

We shall start by recalling the notion of homomorphisms and isomorphisms between structures. Given two `sigma`-structures `fr A` and `fr B`, a homomorphism between them is a function `h: A -> B` such that `h(c^{fr A}) = c^{fr B}` for every constant symbol `c in sigma`, and `h(bb a) := (h(a_1), ..., h(a_r)) in R^{fr B}`, for every `r`-ary relation symbol `R in sigma` and `bb a := (a_1,...,a_r) in R^{fr A}`. So, homomorphisms are tuple-preserving functions (here, think of a tuple as an `r`-ary vector prepended by an `r`-ary relation symbol, eg, `R(1,2,3)`). Now isomorphisms are basically bijective homomorphisms whose inverse are also homomorphisms. Intuitively, this means that two isomorphic structures are the same after relabeling the elements of the universe in one of these structures. We write `fr A ~= fr B` to denote that `fr A` and `fr B` be isomorphic.

Now we define what we mean by queries. Fix a vocabulary `sigma` and a class `cc M` of (not necessarily all) finite `sigma`-structures. This class `cc M` will be referred to as a ground set. Now, for `k >= 0`, a `k`-ary query `cc Q` is a function associating each `fr A in cc M` to a subset of `A^k` such that `cc Q` is closed under isomorphisms, ie, whenever `h: A -> B` is an isomorphism, we have `h( cc Q(fr A)) = cc Q(fr B)`. Now this query `cc Q` is said to be expressible (or definable) in a logic `L` over `cc M` if there exists a `L`-formula `phi` over `sigma` with `k` free variables such that for every `fr A in cc M`, `cc Q(fr A) = phi(fr A)` where

`phi(fr A) := { (a_1,...,a_k) in A^k : fr A |= phi(a_1,...,a_k) }`.

Whenever `cc M` be the set of all finite structures, we shall omit mention of `cc M`.
An important special case occurs when `k = 0`. Such queries are normally called boolean queries or just properties. In this case, the image of `cc Q` can only be either a singleton `{()}` containing the trivial tuple `()`, or the empty set `O/`. We will identify `{()}` with `true` and `O/` with `false`. So, a property `cc Q` is expressible in a logic `L` over `cc M` if there exists an `L`-sentence `phi` over `sigma` such that `cc Q(fr A) = true` iff `fr A |= phi`, for each `fr A in cc M`. Examples of boolean queries (for finite graphs) are:

Hamiltonian: `cc Q(fr G) = true` iff the graph `fr G` is hamiltonian.
Self-loop: `cc Q(fr G) = true` iff the graph `fr G` has a self-loop (ie, `fr G |= EE x( E(x,x))`).
Isolated: `cc Q(fr G) = true` iff the graph `fr G` has an isolated vertex.
Connected: `cc Q(fr G) = true` iff the graph `fr G` is connected.
Acyclic: `cc Q(fr G) = true` iff the graph `fr G` is acyclic.

An example of 2-ary queries is the transitive closure query of finite graphs:

`Q: fr G |-> { (a,b) in G^2 : text{there exists a path from } a text{ to } b text{ in} fr G }`

Question: which of the above queries are expressible in first-order logic? Well, we already saw that Self-loop is expressible in first-order logic. So, it is enough to exhibit a first-order formula to show that a query be expressible in first-order logic. But how do we prove first-order inexpressibility results? In classical model theory, we have tools like compactness and Lowenheim-Skolem theorems for proving first-order inexpressibility. However, most of these tools including the two afore-mentioned theorems fail to "work" in the finite. The only one result that survives is the Ehrenfeucht-Fraisse games (a good exposition of the result can be found here). [Incidentally, does this imply that finite model theory is more difficult than classical model theory?] The games, for example, can be used to prove that the queries Hamiltonian, Connected, Acyclic, and Transitive Closure are not definable in first-order logic. These results will be discussed in subsequent postings.

Finite Model Theory: Preliminaries (1)

2005-05-27T19:02:00.000-05:00

I realize that in the previous postings I haven't been as precise as I can possibly be. It's all about to change: we shall now fix terminologies for our subsequent discussion on finite model theory. We will however have to divide this "section" into two postings, as it is too long for one. We shall also assume that the reader knows basic facts from mathematical logic (see Enderton's A Mathematical Introduction To Logic).

We can start by discussing what finite model theory is. One common definition for finite model theory is the model theory of finite structures. Precise, but perhaps too succinct. What makes it different from classical model theory? Finite model theory is primarily concerned with finite structures, while model theory with both finite and infinite structures. Hence, one can expect that the definitions used in finite model theory are very similar to those in classical model theory. The restriction to finite structures is necessary for studying computers and computation due to their finite nature. Note also that finiteness doesn't necessarily imply triviality. For example, witness that (finite) graph theory is a deep, rich, and beautiful subject, which has captivated brilliant mathematicians from many generations including Euler and Erdos.

Unless otherwise stated, we shall make the following assumptions in subsequent postings on finite model theory:

Every vocabulary and structure is relational, ie, has no function symbols and functions.
Every vocabulary has finitely many (constant and relation) symbols.
Capital Fraktur fonts are used to denote structures; their corresponding letters in Latin correspond to their universes. For example, a structure `fr A` has universe `A`.

I am going to adopt an extremely useful definition of expansion of structures from Libkin's Elements of Finite Model Theory, which will allow us to convert back and forth between formulas and sentences. Let `fr A` and `fr A'` be structures over, respectively, `sigma` and `sigma'` where `sigma nn sigma' = O/`. The expansion of `fr A` by `fr A'`, denoted by `(fr A,fr A')`, is the `sigma uu sigma'`-structure with all symbols from `sigma` interpreted according to `fr A`, and from `sigma'` interpreted according to `fr A'`. An important special case is when `sigma'` be the vocabulary `sigma_n` containing only constant symbols `c_1,cdots,c_n`. In this case, if `fr A' = (a_1, cdots, a_n)` (with `a_i` interpreting `c_i`), we can omit some redundant brackets and write `(fr A, fr A') = (fr A, a_1, cdots, a_n)`. We have the following lemma:

Lemma: Suppose `phi(x_1, cdots, x_n)` be a `sigma`-formula, and `fr A` be a `sigma`-structure. Let `Phi` be the formula `phi(c_1/x_1,cdots,c_n/x_n)`, ie, each occurence of `x_i` is replaced by a brand new constant symbol `c_i`. Then, we have: `fr A |= phi(a_1,cdots,a_n)` iff `(fr A,a_1,cdots,a_n) |= Phi`.

Finally, we need to define the notion of `k`-ary queries, which we will do in the next posting.

The Unusual Effectiveness of Logic in Computer Science

2005-05-23T00:57:00.000-05:00

A couple of days ago I found a non-technical logic-in-computer-science paper in my folder of unused papers that has turned out to be a highly interesting read. The paper is:

On the Unusual Effectiveness of Logic in Computer Science by Halpern, Halper, Immerman, Kolaitis, Vardi, and Vianu

The authors of these papers are well-renowned authorities in the area of logic in computer science, each with his own enormous contribution to the area.

Here is a summary of the paper. The authors start by mentioning two attempts of explaning the unreasonable effectiveness of mathematics in natural sciences by E.P. Wigner, a Nobel Laureate for Physics, and R.W. Hamming, an ACM Turing Award (which can be construed as the Nobel Prize for Computer Science) winner. In their separate papers, Wigner and Hamming give a number of examples supporting his argument, but conclude that the question "Why is mathematics so unreasonably effective" remains open. The above paper by Halpern et al. is basically an attempt to answer the question "why logic is so effective in computer science". Like Wigner and Hamming did, Halpern et al. give a number of examples supporting their assertion:

Example 1: Descriptive Complexity. The reader should know roughly what this is by now.
Example 2: Logic as a Database Query Language. This area is devoted to the study of abstract query languages in database theory. Examples of abstract query languages are relational calculus (equivalent to first-order logic), and conjunctive queries (see here for a definition).
Example 3: Type Theory in Programming Language Research. Type theory is often used for building useful type systems for strongly-typed programming languages including Haskell (the computer science reader should know that C, for example, is not strongly-typed).
Example 4: Reasoning about Knowledge. You may think of this area as "the theory of agents". Reasoning about knowledge plays a key role in burgeoning computer science fields including distributed computing, game theory, and AI.
Example 5: Automated Verification in Semiconductor Designs. The meaning is self-explanatory.

Aside: I would love to see proof complexity and bounded arithemetic discussed in this paper.

Incidentally, Halpern et al. make a very interesting remark in their paper --- that logic seems more connected to computer science than to mathematics. To a theoretical computer scientist like myself, this claim is so conspicuous. I'm curious whether philosophers and/or mathematicians and/or logicians think so too ...

MathML

2005-05-20T20:20:00.000-05:00

Recently I said that a good logic blogger needs to learn something like MathML. Well ... I have just taken a first step in this direction: enable the MathML mode on this website.

Also, I have just recently found ASCIIMathML, thanks to a posting in Andrej Bauer's blog. This script allows you to write math formulas in a LaTeX-like notation. This takes away the burden of learning MathML.

If your browser cannot display MathML, then here is a suggestion (look at 'system requirements' section).

What the tortoise said to achilles

2005-05-20T08:10:00.000-05:00

Howdy! Today I am pleased to learn that somebody is actually reading my blog and has left some useful and encouraging comments. Thanks to all who have participated.

One of the good comments I received was a reference to What The Tortoise Said to Achilles by Lewis Carrol, in response to my question in the previous posting whether logicians have a sense of humor. Incidentally, my hunch says I've seen this article in Douglas Hofstadter's excellent Godel, Escher, Bach: An Eternal Golden Braid.

Anyway, on with the story. Basically, Carrol's article contains a clever and well-constructed argument that reasoning is impossible without using an infinite series of modus ponens. I personally feel this argument itself already shows that logicians are humorous (well ... more precisely, logically humorous). I leave the reader to ponder whether Carrol's article shows that logicians have a sense of humor.

Oh, incidentally, I was quite surprised to learn the well-renowned 'Alice's Adventures in Wonderland' is also written by Lewis Carrol, a logician. Wow!

How to be a good blogger

2005-05-18T23:46:00.000-05:00

Having just started my own blog, I have recently been thinking about what one needs to do to be a good math/logic blogger. After some serious meditations, I realize that this question is equivalent to 'how to make a fine piece of math/logic writing', whose answers can be found in books like Mathematical Writing by Donald Knuth et al. Nevertheless, there are some additional, but equally important, things that good bloggers need to do:

Be controversial.
Utilize the ability to hyperlink (preferrably to free online resources).
Learn how to use MathML. Here is a seemingly good
tutorial (I haven't perused this meticulously enough though). If you already know LaTeX and are using a Unix-like OS, you may want to use Ttm to convert LaTeX to MathML.
Lastly, having just a bit of sense of humor doesn't hurt. I wonder though if logicians have a sense of humor?

I guess I have hitherto successfully and continuously violated every single one of these tips (Oops). Ah well ... I guess there is still tomorrow.

Unary-conjunctive-view Query Language (1)

2005-05-17T19:22:00.000-05:00

Last December I completed my BSc(Honours) degree, the Australian equivalent of American BSc degree, at the University of Melbourne (Australia). So, before I am leaving for North America for graduate studies, I thought it might be a good idea to write something about the finite-model-theory related problem I worked on for my undergraduate thesis. It might also be a good topic to get this blog started.

The story is somewhat lengthy. So, I will divide it into a series of bite-size chunks.

To get under way, recall that pure first-order logic is undecidable. [When we say that a logic is (un)decidable, we mean that its satisfiability problem is (un)decidable.] Here pure first-order logic basically consists of all first-order sentences without equality and function symbols. Turing proved this by reducing the halting problem for Turing machines to deciding the satisfiability of first-order logic. We know on the other hand that pure monadic first-order logic (MFO) is decidable, actually complete for NEXPTIME. Here the term 'monadic' simply means that the relation symbols in each formula in MFO are of arity 1. This decidability result actually lies at the border of the decidable and the undecidable because permitting merely one binary relation symbol to MFO immediately results in undecidability.

So, the question boils down to how much more can we extend MFO before we get an undecidable logic? Strictly speaking, this is not really a mathematical question, and so has no single correct answer. I'll mention three known successful attempts to extend the decidability of MFO:

MFO with equality. Lowenheim, who proved the decidability of MFO, proved this too.
MFO with any number of function symbols. This is Lob-Gurevich theorem.
MFO with equality and one function symbol. This is proved by Rabin in one of his groundbreaking papers.

All of these results are optimum. For example, adding one more function symbol to the third logic in this list results in undecidability. For more information on these logics, the reader is referred to the reference book for the classical decision problem. We will however explore a different avenue to answer this question.

Database theorists often talk about conjunctive queries: pure first-order formulas that can be written as

F (x_{1}, \dots, x_{n}) : = (\exists y_{1}, \dots, y_{k}) (R_{1} (u_{1}) \land \dots \land R_{m} (u_{m}))

where the x's are the free variables, the y's are the bound variables, and the u's are tuples of variables appropriate for the (arities of the) R's. Following notations from logic programming, we will write the formula F as

F (x_{1}, \dots, x_{n}) \leftarrow R_{1} (u_{1}), \dots, R_{m} (u_{m})

The set of all these F's forms the conjunctive query language. Now, it is easy to see that any conjunctive query is satisfiable --- so its satisfiability problem is trivial. Here is the twist. We can combine MFO and a restricted version of conjunctive query language to make a decidable logic.

Let U be the set of all conjunctive queries with exactly one free variable (a.k.a. unary conjunctive queries). We call U a view vocabulary (signature). Let UCV be the smallest set that satisfies the following conditions:

U is a subset of UCV.
UCV is closed under boolean operations and first-order quantifications.

The Unary-Conjunctive-View query language is the logic UCV. To get a feel for UCV, let us start speaking in it. For example, this logic can assert the following graph-theoretic sentence "any vertex has a 4-walk but no self-loop". How? Consider the following two conjunctive queries:

${CW}_{4} (x_{0}) \leftarrow E (x_{0}, x_{1}), E (x_{1}, x_{2}), E (x_{2}, x_{3}), E (x_{3}, x_{4})$
$Loop (x) \leftarrow E (x, x)$

Then, the desired sentence is $AA x ( text{CW_4}(x) ^^ not text{Loop}(x) )$. We can readily see that this logic is quite expressive as it permits any number of relation symbols of any arity. This also shows that UCV is strictly more expressive than MFO and the conjunctive query language, considered individually. Nonetheless, the logic is much less expressive than the first-order logic. For example, UCV cannot even assert simple query like "there exists a path (ie, walks where none of the vertices are visited twice) of length k", for any fixed k > 0. [We'll prove this later.]

In the next posting, I will sketch a proof that UCV is decidable, actually solvable in 2-NEXPTIME but is NEXPTIME-hard. Our proof taps into the fact that UCV has the bounded model property, i.e., every satisfiable query Q in UCV has a model of size at most f(|Q|) for some computable function f:N->N where |Q| denotes the size of the encoding of Q. Note that bounded model property immediately implies decidability in SPACE(f(|Q|)), assuming that f is a proper complexity function, as a Turing machine can start by computing f(|Q|), enumerate every possible structure A appropriate for Q one-by-one, and for each A test whether A satisfies Q (which can be also be done in SPACE(f(|Q|)) ).

Later on we will explore the expressive power of UCV and a general method for proving inexpressibility in UCV.

Welcome to Logicomp!

2005-05-16T02:56:00.000-05:00

Hello all! Throughout the past two years, I have learned a lot from Lance Fortnow's successful complexity blog. Professor Fortnow has been an excellent blogger, and kept his avid readers informed on the lattest and the must-know about complexity theory. His blog was certainly one of the things that got me interested in complexity theory, and will continue inspiring me in the future.

Although Professor Fortnow's blog covers many topics in complexity theory, it is a pity that the blog rarely touches on the elegant connection between logic and complexity theory, which --- God knows why --- many finite model theorists think will be a key to proving that P does not equal NP. For example, here are some deep results in the area:

Fagin's theorem: the set of properties of (relational) finite structures expressible in existential second-order logic (ESO) coincides with NP.
Dual Fagin's theorem: the set of properties of finite structures expressible in universal second-order logic (ASO) coincides with co-NP.
The set of properties of finite structures expressible in second-order logic (SO) coincides with PH.

So, in order to prove that P does not equal NP, it suffices to prove that the set of properties of finite structures expressible in ESO is different from that expressible in ASO. In fact, to prove this it is enough to show that the property 3-colorability is not expressible in ASO on the class of finite graphs. That is, we have reduced an important problem in complexity theory to a problem in finite model theory. The area of theoretical computer science that explores the connection between finite model theory and complexity theory is called descriptive complexity.

In view of these, I thought it would be a good idea for me to start a blog that aims to explore the deep connection between logic and complexity. Nonetheless, I realize that it is a formidable task to be a good blogger even for a small subarea of logic and complexity, especially for a newbie like myself. Thus, I will try to focus on areas that I will explore during my graduate studies: (finite and infinite) model theory and descriptive complexity, proof complexity, and perhaps bounded arithmetic. [Nonetheless, I will probably have to every now and then violate this rule and speak about other things that I find interesting and fun.] So, from now on, when I speak about 'Logic and Complexity', I will be referring to these subareas. There are already excellent blogs that cover logic, like this one maintained by Professor Restall at The University of Melbourne's Department of Philosophy, and logic and computation, like this one. However, none of these cover the stuff that I plan to talk about here such as finite model theory and descriptive complexity.

Anyway, for a starter, I plan to write a concise introduction to finite model theory that other mathematical readers, who know a bit of logic, can read. I will try to post this bit-by-bit every week. Any other ideas? Feel free to comment.