Project
Completeness for the modal mu-calculus (June 2008)
This page concerns the project `Completeness for the modal mu-calculus',
taught at the University of Amsterdam in June 2008.
Contents of these pages
-
Here is the paper that is the topic of the
project.
-
A brief introductory meeting of the project was held on Thursday, May
29, from 10-11 am in P327.
The first meeting was on Tuesday June 3. Section 3 was discussed. The second meeting was on Friday June 6. We finished discussing Section 3. Third meeting was on Tuesday June 10. We discussed Section 4 and beginning of Section 5. On June 13 we finished discussing Section 5. On June 17 we discussed Section 6. On June 20 we discussed the beginning of Section 7, until the end of Observation 39.3. On June 25, we discussed Observation 39.4 and the beginning of Observation 3.5. On June 27, we finished discussing Observation 3.5.
The modal mu-calculus is an extension of modal logic with fixpoint operators
which was introduced in the early 1980s. It is an important formalism with
many applications, in computer science and elsewhere, and an interesting
mathematical theory. It shares many attractive properties with ordinary modal
logic, but has a much bigger expressive power.
In 1983 an axiomatization for the modal mu-calculus was proposed by Dexter
Kozen, and this axiomatization was proved to be complete by Igor Walukiewicz
in the 1990s. The aim of the project is to go in detail through Walukiewicz'
notoriously difficult paper
``Completeness of Kozen's axiomatization of the Propositional mu-Calculus",
Information and Computation 157 (2000) 142--182.
Prerequisites
Students are assumed to have a working knowledge of the syntax and semantics
of the modal mu-calculus.
More precisely, we build on the material covered in the course
Capital Selecta in Modal
Logic, Algebra and Coalgebra of this year.
Staff
Dates/location:
-
The project will run from June 2 to June 27.
-
There will be two or three meetings weekly, of which the exact coordinates
are to be determined.
Course material
- Here is a pdf file of the paper by Walukiewicz: (to be supplied)
- Here is a pdf file of the lecture notes on the modal mu-calculus:
(to be supplied)
-
In order to pass the project successfully, students need to
- participate actively in the group meetings, and
- occasionally work out and hand in details of (alternative) proofs.
Comments, complaints, questions: mail Yde Venema