Completeness for \(\mu\)-calculi: a coalgebraic approach (Q1731842)

The basic modal language is usually extended by a fixed point operator, giving a modal $\mu$-calculus; there are, however, other possible extensions around, yielding a family of modal $\mu$-calculi. This paper addresses the axiomatization problems for these calculi, essentially using coalgebraic methods with some not so little help from automata theory. The easiest accessible results from a plethora of similar ones concern the completeness of the graded $\mu$-calculus, and of the monotone modal $\mu$-claculus; these results are new. An essential technical tool is the introduction of one-step formulas gleaned from a set of predicate liftings (all functors involved are set functors); this opens the way to a careful study of the problem through coalgebaic automata and their interplay through games. One-step formulas have been proposed by e. g. \textit{C. Cîrstea} and \textit{D. Pattinson} [Lect. Notes Comput. Sci. 3170, 258--275 (2004; Zbl 1099.03018)] and \textit{L. Schröder} and \textit{D. Pattinson} [J. Log. Comput. 20, No. 5, 1113--1147 (2010; Zbl 1266.03032)]. This technical tool is accompanied by the investigation of a disjunctive basis, which permits -- roughly speaking -- the elimination of conjunctions. These devices permit an easier and fairly transparent treatment of the interplay of one-step formulas and formulas induced by the predicate lifting proper. The well-written paper is technically rich with a nearly overwhelming body of definitions, notations, etc; there are two companion papers written by the present authors [Theor. Comput. Sci. 727, 37--100 (2018; Zbl 1391.68077)], resp. the first and the last author [LIPIcs -- Leibniz Int. Proc. Inform. 72, Article 11, 16 p. (2017; Zbl 1433.68427)] which belong to this present context, and to which the authors refer from time to time.