Modal Fixpoint Logic: Some Model Theoretic Questions GaĆ«lle Fontaine Abstract: This thesis is a study into some model-theoretic aspects of the modal \mu-calculus, the extension of modal logic with least and greatest fixpoint operators. We explore these aspects through a `fine-structure' approach to the \mu-calculus. That is, we concentrate on special classes of structures and particular fragments of the language. The methods we use also illustrate the fruitful interaction between the \mu-calculus and other methods from automata theory, game theory and model theory. Chapter 3 establishes a completeness result for the \mu-calculus on finite trees. The proof of the completeness of the \mu-calculus on arbitrary structures is well-known for its difficulty, but it turns out that on finite trees, we can provide a much simpler argument. The technique we use consists in combining an Henkin-type semantics for the \mu-calculus together with model theoretic methods (inspired by the work of Kees Doets). In Chapter 4, we study the expressive power of the \mu-calculus at the level of frames. The expressive power of the \mu-calculus on the level of models (labeled graphs) is well understood, while nothing is known on the level of frames (graphs without labeling). In the setting of frames, the proposition letters correspond to second-order variables over which we quantify universally. Our main result is a characterization of those monadic second-order formulas that are equivalent on trees (seen as frames) to a formula of the \mu-calculus. In Chapter 5, we provide characterizations of particular fragments of the \mu-calculus, the main ones being the Scott continuous fragment and the completely additive fragment. An interesting feature of the continuous formulas is that they are constructive, that is, their least fixpoints can be calculated in at most \omega steps. We also give an alternative proof of the characterization of the completely additive fragment obtained by Marco Hollenberg, following the lines of the proof for the characterization of the continuous fragment. In the next chapter, we investigate the expressive power of a fragment of CoreXPath. XPath is a navigation language for XML documents and CoreXpath has been introduced to capture the logical core of XPath. In Chapter 6, we exploit the tight connection between CoreXPath and modal logic: by combining well-known results concerning the \mu-calculus (one of them appearing in Chapter 5), we establish a characterization of an important fragment of CoreXPath. Finally, in Chapter 7, we develop automata-theoretic tools for coalgebraic fixpoint logics, viz. generalizations of the \mu-calculus to the abstraction level of coalgebras. Coalgebras provide an abstract way of representing evolving systems. We use those tools to show the decidability of the satisfiability problem as well as a small model property for coalgebraic fixpoint logics in a general setting. We also obtain a double exponential upper bound on the complexity of the satisfiability problem.