Flat coalgebraic fixed point logics (bibtex)
by Lutz Schröder, Yde Venema
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.
Reference:
Flat coalgebraic fixed point logics (Lutz Schröder, Yde Venema), In 21st International Conference on Concurrency Theory, CONCUR 2010 (Paul Gastin, François Laroussinie, eds.), Lecture Notes in Computer Science, vol. 6269, pp. 524–538, Springer, 2010. [preprint]
Bibtex Entry:
@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.
},
}
Powered by bibtexbrowser