Publikation
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.
Zusammenfassung
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.
Projekte
FormalSafe - Formale Entwicklung für Sichere Robotik,
GenMod - Generische Algorithmen und Komplexitätsschranken für Koalgebraische Modallogiken
GenMod - Generische Algorithmen und Komplexitätsschranken für Koalgebraische Modallogiken