CSL02 Tutorials

• Introduction to mu-calculi by Julian Bradfield (morning)
• Parameterized Complexity Theory by Martin Grohe (afternoon)

The abstract for Introduction to mu-calculi is

Modal mu-calculus is a logic obtained by adding fixpoint operators to ordinary modal logic, or Hennessy-Milner logic. The result is a very expressive logic, sufficient to subsume many other temporal logics such as CTL and CTL*. The modal mu-calculus is easy to model-check, and so makes a good `back-end' logic for tools; it has an interesting theory, with some major problems still open; but it also has a certain reputation for being hard to read and write.

This tutorial provides an introduction to the modal mu-calculus and mu-calculi more generally, suitable for those with some exposure to modal or temporal logic, but without prior knowledge of fixpoint logics.

I shall start by briefly reviewing basic modal logic and temporal logics such as CTL.

I then introduce the modal mu-calculus itself. I cover the formal syntax and semantics in its traditional presentation, and then give more informally an intuition that is most useful in understanding formulae of the logic -- this intuition has a formal basis in games that will be described in the invited lecture by Damian Niwinski.

I will describe `traditional' global and local model-checking techniques for modal mu-calculus; again, Niwinski's lecture will discuss game-based techniques.

I will then spend the latter part of the tutorial discussing some more general aspects of fix-point logics, such as their role in finite model theory and descriptive set theory.

Note: I am also giving a tutorial at CONCUR'02. The CSL tutorial has a different focus from the CONCUR tutorial; its first half is largely the same as the first half of the CONCUR tutorial, and then it diverges.

The abstract for Parameterized Complexity Theory is:

Parameterized complexity theory provides a framework for a fine-grain complexity analysis of algorithmic problems that are intractable in general. In recent years, ideas from parameterized complexity theory have found their way into various areas of computer science, such as database theory, artificial intelligence, and computational biology. Central to the theory is the notion of fixed-parameter tractability, which relaxes the classical notion of tractability, polynomial time computability, by admitting algorithms whose runtime is exponential, but only in terms of some parameter of the problem instance that can be expected to be small in the typical applications. A good example is the evaluation of database queries: Usually, the size of the query to be evaluated is very small compared to the size of the database. Thus a parameterized complexity analysis may help to get a more realistic picture of the complexity of database query evaluation.

There are surprisingly tight connections between logic and parameterized complexity theory. On the intractability side, logically defined problems, in particular model-checking problems for various fragments of first-order logic, give very clean descriptions of the main parameterized complexity classes. On the tractability side, logic has been used to prove algorithmic meta theorems, the best known of which is Courcelle's theorem stating that problems definable in monadic second-order logic are fixed-parameter tractable when parameterized by the tree-width of the input structure.

In the first part of this tutorial, we will discuss typical algorithmic techniques that are used to establish the fixed-parameter tractability of various problems. The second part is going to be an introduction into the theory of parameterized intractability. Throughout, we will put particular emphasis on the connections between logic and parameterized complexity theory.