Completeness of Flat Coalgebraic Fixpoint Logics

TL;DR

This paper proves the completeness of a broad class of flat coalgebraic fixpoint logics, including many well-known modal fixpoint logics, within a generic semantic framework.

Contribution

It provides a generic proof of completeness for the Kozen-Park axiomatization applicable to various flat coalgebraic fixpoint logics.

Findings

Completeness proof for flat coalgebraic fixpoint logics.

Applicability to a wide range of logics including probabilistic and monotone variants.

Unification of several fixpoint logics under a generic framework.

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., LTL, 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 ATL), 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.