### CITATION FOR TEST-OF-TIME AWARD FOR LICS 1995 PAPER

*Igor Walukiewicz* (CNRS & Université Bordeaux-1)

**Completeness of Kozen's Axiomatisation of the Propositional mu-Calculus**

The propositional mu-calculus (now more commonly known as the modal
mu-calculus) was first published in 1983 by D. Kozen, although the
system had been studied much earlier by J. de Bakker and D. Scott
(unpublished notes, 1969). The system subsumes many popular
propositional logics of programs, including linear temporal logic,
computation tree logic CTL*, and propositional dynamic logic. Kozen
proposed a deductive system whose chief rule of inference was a
variant of the fixpoint induction rule of D. Park and conjectured it
to be complete. During the decade after its introduction, this
calculus attracted a great deal of attention within computer science
circles. Despite the attention given to this calculus, it was not
until this paper by Walukiewicz a dozen years later that the proof
system was finally shown to be complete. In order to prove the
completeness theorem, several technical innovations were developed. A
full version of this paper appeared in Information and Computation in
2000.