In this part of the lecture, we discuss how logic can be used to describe graphs or trees or words. The logic of interest is monadic second-order logic (mso). The main result is Courcelle’s Theorem, which says that every fixed formula of mso can be evaluated in linear time on graphs that are similar to trees.

---

Monadic second-order logic. 

Monadic second-order logic (mso) is a logic with two types of quantifiers: one can quantify over elements, and one can quantify over sets of elements. One cannot, however, quantify over sets of pairs, or over sets triples, etc.

Our main interest here is to use mso to describe properties of undirected graphs. For example, suppose that we view a undirected graph as relational structure (i.e. a model as in logic), where the universe is the vertices and there is one binary relation for the edges; this relation is symmetric. The following formula

   

says that the graph is a clique. The formula only quantifies over vertices, i.e. it uses only first-order quantification. Now we consider a formula which uses also set quantification. We adopt the convention that small variables range over elements and big variables range over sets of elements.  The following formula says that input graph is not connected:

   

The above formula illustrates all constructs in mso: one can quantify over elements, over sets of elements, one can test membership of elements in sets, and one can use the predicates available in the input model.

Here is another example: an mso formula which says that the input graph is three colourable:

   

We say that a property of graphs (or more generally, structures over some vocabulary) is mso definable if there is a formula of mso which is true exactly in those graphs which have the property.

---

Model checking of mso

Model checking of mso formulas is the problem of checking if a given formula is true in a given structure (here, a graph). This problem is computationally hard: if we assume that the input is both the graph and the formula, then the problem is PSPACE complete (actually, it is PSPACE complete even when the graph is fixed, e.g. the one vertex graph, by encoding QBF in a straightforward way). If the formula is fixed and the graph is the only input, then the problem can be NP complete, as the example of 3-colorability shows. Since mso has built in negation, then we can also get coNP problems, e.g. non-3-colorability, and by using alternation of set quantifiers we can get problems that are complete for any level of the polynomial hierarchy. Summing up – in general, the model checking problem is hard.

The goal of this lecture is to show that the model checking becomes tractable – even linear time – when the formula is fixed and the graphs are similar to trees. In particular, 3-colorability is tractable on graphs similar to trees, but the same holds for any graph problem which can be formalised in mso.

---

Treewidth and Courcelle’s Theorem.

We now come to the main result of this part of the lecture, namely Courcelle’s theorem. The theorem is about evaluating model checking mso on graphs of bounded tree width. Treewidth is a graph parameter, i.e. every graph has a some treewidth, which is a natural number. The treewidth of a graph describes the smallest width of a tree decomposition that can produce the graph. Treewidth, tree decompositions and their width are defined here. The general idea is that small width tree decompositions can be obtained for graphs that are similar to trees, although there exists other inequivalent ways of quantifying similarity to a tree, e.g. clique width.

Bodlaender and Kloks have shown that tree decompositions can be computed in linear time, when the width is fixed, i.e. every there is a linear time algorithm which inputs a graph and outputs, if it exists, a tree decomposition of width . The constant in the linear time is exponential in . We will show an easier result, which is weaker in two ways: the algorithm is not linear, and the computed tree decomposition is not optimal.

Theorem 1. For every there is a cubic time algorithm which inputs a graph and fails or outputs a tree decomposition of width . The algorithm succeeds if the graph has treewidth .

Theorem 1 is proved here. The constant in the running time is exponential in .

The second ingredient in Courcelle’s theorem is that, once the tree decomposition is given,  mso formulas can be evaluated in linear time.

Theorem 2. Let  and let be an mso formula over the vocabulary of graphs, i.e. using a binary relation .  There is a linear time algorithm which inputs a tree decomposition of width and decides if the underlying graph satisfies .

Theorem 2 is proved in two steps: we introduce automata over trees and show that they are equivalent to mso and then we show that evaluating mso on a graph of bounded treewidth can be simulated by running a tree automaton over a tree decomposition. The constant in the running time is nonelementary in , i.e. it is more than exponential, more than doubly exponential, etc. Combining the two results above we get the following.

Corollary (Courcelle’s Theorem). Let and let be an mso formula over the vocabulary of graphs, i.e. using a binary relation .  There is a cubic algorithm which inputs an unidrected graph and fails or answers if the graph satisfies . The algorithm succeeds if the graph has tree width .

Note that in the algorithm above, there are three possible outcomes: fail (don’t know), satisfies , and does not satisfy . Using the stronger, linear time, version of Theorem 1, we could get a linear running time for the algorithm in Courcelle’s Theorem.

 

COMMENTS