Game Logic, coalgebraic completeness and automata 

Game Logic (Parikh, 1985) is a multi-modal, monotonic modal logic for
reasoning about strategic ability in 2-player determined games. Game
Logic can be seen as a monotonic generalisation of Propositional Dynamic
Logic (PDL) in which games are interpreted as monotonic neighbourhood
functions, and game operations include all the PDL program operations
together with the operation dual (which denotes role swap of the two
players). We have recently shown that both Game Logic and PDL can be
seen as instances of a coalgebraic framework of dynamic logics in which
the completeness of PDL and dual-free Game Logic can be proved uniformly
(cf. Hansen, Kupke). Completeness of full Game Logic, however, remains
an open challenge, nevermind completeness for the coalgebraic
generalisations. Recent results in the theory of coalgebraic fixpoint
logics (cf. Enqvist, Venema, Seifan) have made crucial use of automata
in proving completeness and other results. An automata-theoretic
characterisation of Game Logic is therefore of interest.

In this talk, I will first introduce Game Logic, and show that it is an
instance of a coalgebraic dynamic logic. Then I will state the
(restricted) coalgebraic completeness theorem, and discuss the
difficulty with completeness of full Game Logic. Finally, I will present
a class of modal automata that characterise Game Logic as a fragment of
the monotonic modal mu-calculus, and discuss future steps towards
completeness.

This is joint work with Clemens Kupke, Johannes Marti and Yde Venema.