Flat coalgebraic fixed point logics

Lutz Schröder, Yde Venema

In: Paul Gastin, François Laroussinie (Hrsg.). Proceedings of the 21st International Conference on Concurrency Theory. International Conference on Concurrency Theory (CONCUR-2010) 21st August 31-September 3 Paris France Lecture Notes in Computer Science Springer Berlin 8/2010.


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.


Weitere Links

flatfix.pdf (pdf, 195 KB )

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence