Modal mu-Calculus

Course Contents

Abstract from the lecture notes:

In this notes we consider propositional mu-calculus as introduced by Kozen. The main purpose of these notes is to present the completeness proof of the Kozen's axiomatisation of the mu-calculus. To achieve this goal we develop tools which allow us to give relatively simple proofs of results for the logic like:

• syntactic characterisation of satisfiability and validity,
• small model theorem,
• decidability,
• equivalence of the mu-calculus over binary trees and Rabin automata,
• a notion of disjunctive formula and the proof that every formula is equivalent to a disjunctive formula,
• linear satisfiability checking algorithm for disjunctive formulas.

These notes are intended to supplement a 6 hours course given in February 1995 at BRICS centre.

Lecture Notes