User Tools

Site Tools

Deciding the First Level of the $mu$-calculus Alternation Hierarchy (BibTeX)

  author      = {Ralf K{\"u}sters and Thomas Wilke},
  title       = {{Deciding the First Level of the $\mu$-calculus Alternation Hierarchy}},
  booktitle   = {FSTTCS 2002: Foundations of Software Technology and Theoretical Computer Science --- 22nd Conference},
  pages       = {241--252},
  year        = 2002,
  editor      = {M.~Agrawal and A.~Seth},
  volume      = 2556,
  series      = {Lecture Notes in Computer Science},
  publisher   = {Springer-Verlag},
  abstract    = {We show that the following problem is decidable and complete for deterministic exponential time. Given a formula of modal mu-calculus, determine if the formula is equivalent to a formula without greatest fixed point operators. In other words, we show that the first level of the mu-calculus fixed point alternation hierarchy is decidable in deterministic exponential time.}