Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Eighth Annual IEEE Symposium on

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 Symposium on Logic in Computer Science (LICS 1993)},
    year =	 {1993},
    month =	 {June}, 
    pages =      {136--146},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski