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