@InProceedings{SchroderVenema10,
  author = {Lutz Schr{\"o}der and Yde Venema},
  title = {Flat coalgebraic fixed point logics},
  year = {2010},
  editor = {Paul Gastin and Fran\c{c}ois Laroussinie},
  booktitle = {21st International Conference on Concurrency Theory, CONCUR 2010},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {6269},
  pages = {524-538},
  keywords = {Coalgebra modal logic fixpoints fixed points mu-calculus flat single-variable alternating time graded ATL AMC},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/flatfix.pdf"> [preprint] </a>},
  abstract = {Fixed point logics
  are widely used in computer science, in particular in artificial
  intelligence and concurrency. The most expressive logics of this
  type are the mu-calculus and its relatives. However, popular
  fixed point logics tend to trade expressivity for simplicity and
  readability, and in fact often live within the single variable
  fragment of the mu-calculus. The family of such flat fixed
  point logics includes, e.g., CTL, the *-nesting-free fragment of
  PDL, and the logic of common knowledge. Here, we extend this notion
  to the generic semantic framework of coalgebraic logic, thus
  covering a wide range of logics beyond the standard mu-calculus
  including, e.g., flat fragments of the graded mu-calculus and the
  alternating-time mu-calculus (such as ATL), as well as
  probabilistic and monotone fixed point logics. Our main results are
  completeness of the Kozen-Park axiomatization and a timed-out
  tableaux method that matches ExpTime upper bounds inherited from the
  coalgebraic mu-calculus but avoids using automata.
},
}