Flat coalgebraic fixed point logics.

link: http://arxiv.org/abs/1004.2717
Abstract

Fixed point logics have a wide range of applications 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.