Modular Games for Coalgebraic Fixed Point Logics

AbstractWe build on existing work on finitary modular coalgebraic logics [C. Cîrstea. A compositional approach to defining logics for coalgebras. Theoretical Computer Science, 327:45–69, 2004; C. Cîrstea and D. Pattinson. Modular construction of complete coalgebraic logics. Theoretical Computer Science, 388:83–108, 2007], which we extend with general fixed points, including CTL- and PDL-like fixed points, and modular evaluation games. These results are generalisations of their correspondents in the modal μ-calculus, as described e.g. in [C. Stirling. Modal and Temporal Properties of Processes. Springer, 2001]. Inspired by recent work of Venema [Y. Venema. Automata and fixed point logic: a coalgebraic perspective. Information and Computation, 204:637–678, 2006], we provide our logics with evaluation games that come equipped with a modular way of building the game boards. We also study a specific class of modular coalgebraic logics that allow for the introduction of an implicit negation operator