2nd Semester 2007/08: Completeness for the Modal μ-Calculus

Instructors

Gaëlle Fontaine, Daisuke Ikegami, Yde Venema.
If you are interested in this project, please contact Yde by e-mail.

ECTS

6

Description

Content. 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 μ-Calculus", Information and Computation 157 (2000) 142--182.

Organisation

The project will take the form of a reading group, with two or three meetings weekly, during which parts of Walukiewicz' paper (and possible, auxiliary material) will be discussed.

Prerequisites

In order to pass the project successfully, students need to

• actively participate in the group meetings, and
• occasionally work out and hand in details of (alternative) proofs.

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.