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

(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:

1. 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.
   
2. Expression complexity: the input is f (i.e. M is fixed).
   
3. 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.