| Art der Veröffentlichung: |
Artikel in Konferenzband |
| Autor: |
Lutz Schröder, Yde Venema |
| Herausgeber: |
Paul Gastin, François Laroussinie |
| Titel: |
Flat coalgebraic fixed point logics |
| Buch / Sammlungs-Titel: |
21st International Conference on Concurrency Theory, CONCUR 2010 |
| Band: |
6269 |
| Seite(n): |
524 – 538 |
| Serie / Reihe: |
Lecture Notes in Computer Science |
| Erscheinungsjahr: |
2010 |
| Verleger: |
Springer |
| Abstract / Kurzbeschreibung: |
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.
|
| PDF Version: |
http://www.informatik.uni-bremen.de/~lschrode/papers/flatfix.pdf |
| Schlagworte: |
Coalgebra modal logic fixpoints fixed points mu-calculus flat single-variable alternating time graded ATL AMC |
| Status: |
Reviewed |
| Letzte Aktualisierung: |
07. 10. 2010 |
