Logic in Computer Science (LICS 1993)

Paper: On completeness of the μ-calculus (at LICS 1993)

Authors: Igor Walukiewicz

Abstract

The long-standing problem of the complete axiomatization of the propositional μ-calculus introduced by D. Kozen (1983) is addressed. The approach can be roughly described as a modified tableau method in the sense that infinite trees labeled with sets of formulas are investigated. The tableau method has already been used in the original paper by Kozen. The reexamination of the general tableau method presented is due to advances in automata theory, especially S. Safra's determinization procedure (1988), connections between automata on infinite trees and games, and experience with the model checking. A finitary complete axiom system for the μ-calculus is obtained. It can be roughly described as a system for propositional modal logic with the addition of a induction rule to reason about least fixpoints

BibTeX

  @InProceedings{Walukiewicz-Oncompletenessofthe,
    author = 	 {Igor Walukiewicz},
    title = 	 {On completeness of the μ-calculus},
    booktitle =  {Proceedings of the Eighth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1993},
    year =	 1993,
    editor =	 {Moshe Vardi},
    month =	 {June}, 
    pages =      {136--146},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }