We investigate multi-agent epistemic modal logic with common knowledge modalities for groups of agents and obtain van Benthem style model-theoretic characterisations, in terms of bisimulation invariance of classical first-order logic over the non-elementary classes of (finite or arbitrary) common knowledge Kripke frames. The fixpoint character of common knowledge modalities and the rôle that reachability and transitive closures play for the derived accessibility relations take our analysis beyond classical model-theoretic terrain and technically pose a novel challenge to the analysis of model-theoretic games. Over and above the more familiar locality-based techniques we exploit a specific structure theory for specially adapted Cayley groups: through the association of agents with sets of generators, all epistemic frames can be represented up to bisimilarity by suitable Cayley groups with specific acyclicity properties; these support a locality analysis at different levels of granularity as induced by distance measures w.r.t. various coalitions of agents.

We study definability questions for positional winning strategies in infinite games on graphs. The quest for efficient algorithmic constructions of winning regions and winning strategies in infinite games, in particular parity games, is of importance in many branches of logic and computer science. A closely related, yet different, facet of this problem concerns the definability of winning regions and winning strategies in logical systems such as monadic second-order logic, least fixed-point logic LFP, the modal μ-calculus and some of its fragments. While a number of results concerning definability issues for winning regions have been established, so far almost nothing has been known concerning the definability of winning strategies. We make the notion of logical definability of positional winning strategies precise and study systematically the possibility of translations between definitions of winning regions and definitions of winning strategies. We present explicit LFP-definitions for winning strategies in games with relatively simple objectives, such as safety, reach ability, eventual safety (Co-Büchi) and recurrent reach ability (Büchi), and then prove, based on the Stage Comparison Theorem, that winning strategies for any class of parity games with a bounded number of priorities are LFP-definable. For parity games with an unbounded number of priorities, LFP-definitions of winning strategies are provably impossible on arbitrary (finite and infinite) game graphs. On finite game graphs however, this definability problem turns out to be equivalent to the fundamental open question about the algorithmic complexity of parity games. Indeed, based on a general argument about LFP-translations we prove that LFP definable winning strategies on the class of all finite parity games exist if, and only if, parity games can be solved in polynomial time, despite the fact that LFP is, in general, strictly weaker than polynomial time.