Completeness of Flat Coalgebraic Fixpoint Logics

Journal article


Publication Details

Author(s): Schröder L, Venema Y
Journal: ACM Transactions on Computational Logic
Publisher: ASSOC COMPUTING MACHINERY
Publication year: 2018
Volume: 19
Journal issue: 1
ISSN: 1529-3785


Abstract

Modal fixpoint logics traditionally play a central role in computer science, in particular in artificial intelligence and concurrency. The mu-calculus and its relatives are among the most expressive logics of this type. However, popular fixpoint 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 fixpoint logics includes, e.g., Linear Temporal Logic (LTL), Computation Tree Logic (CTL), and the logic of common knowledge. Extending this notion to the generic semantic framework of coalgebraic logic enables 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 alternating-time temporal logic), as well as probabilistic and monotone fixpoint logics. We give a generic proof of completeness of the Kozen-Park axiomatization for such flat coalgebraic fixpoint logics.


FAU Authors / FAU Editors

Schröder, Lutz Prof. Dr.
Lehrstuhl für Informatik 8 (Theoretische Informatik)


External institutions with authors

University of Amsterdam


How to cite

APA:
Schröder, L., & Venema, Y. (2018). Completeness of Flat Coalgebraic Fixpoint Logics. ACM Transactions on Computational Logic, 19(1). https://dx.doi.org/10.1145/3157055

MLA:
Schröder, Lutz, and Yde Venema. "Completeness of Flat Coalgebraic Fixpoint Logics." ACM Transactions on Computational Logic 19.1 (2018).

BibTeX: 

Last updated on 2019-04-01 at 22:10