Completeness of Kozen's Axiomatization for the Modal mu-Calculus: A Simple Proof
Logic in Computer Science
2020-10-20 v3 Formal Languages and Automata Theory
Computer Science and Game Theory
Abstract
The modal mu-calculus, introduced by Dexter Kozen, is an extension of modal logic with fixpoint operators. Its axiomatization, Koz, was introduced at the same time and is an extension of the minimal modal logic K with the so-called Park fixpoint induction principle. It took more than a decade for the completeness of Koz to be proven, finally achieved by Igor Walukiewicz. However, his proof is fairly involved. In this article, we present an improved proof for the completeness of Koz which, although similar to the original, is simpler and easier to understand. Keywords: The modal mu-calculus, completeness, omega-automata.
Keywords
Cite
@article{arxiv.1408.3560,
title = {Completeness of Kozen's Axiomatization for the Modal mu-Calculus: A Simple Proof},
author = {Kuniaki Tamura},
journal= {arXiv preprint arXiv:1408.3560},
year = {2020}
}