BRICS · Contents · Lecture Notes

**A BRICS Mini-Course**

**February, 1995**

**Lectures by
Igor Walukiewicz
**

**
**

*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.