Fragments of Fixpoint Logics: Automata and Expressiveness Facundo Carreiro Abstract: This dissertation, entitled Fragments of Fixpoint Logics: Automata and Expressiveness, studies the relative expressive power and properties of several fixpoint and second-order logics. We use the term fixpoint logic in a broad sense, referring to any logic which can encode some type of recursion, iteration or repetition. Our main objective is to systematically identify several important logics as precise fragments of other well-known logics. In order to accomplish this task, we develop automata-theoretic tools to analyze these fragments. The results of this dissertation provide new insight on the relationship of fixpoint and second-order logic and provides further evidence of the successful logic-automata connection. In Chapter 3 we define and analyze fragments of both modal and first-order fixpoint logics. The main method that we use to define these fragments is the restriction of the application of the fixpoint operator μp.φ (and the first-order equivalent) to formulas φ having a special property. The main properties that we consider are complete additivity and continuity, but we also consider other syntactic restrictions and their effects. On the modal side, we give precise syntactic and semantic characterizations of PDL, Concurrent PDL and GL inside the μ-calculus. On the first-order side, we give an analogous characterization of FO(TC^1) inside FO(LFP^1). In Chapter 4 we introduce several subclasses of parity automata and discuss the intuitions and motivations behind these definitions. The subclasses are inspired by the fragments of Chapter 3 and try to parallel, on the automata side, the additivity and continuity constraints of the syntactic fragments. In the last part of this chapter we introduce a general technique (due to Janin [Jan06]) to bring parity automata into a tree-like shape. This structure has the advantage of being ‘almost a (fixpoint) formula’ and therefore it is easy to translate it to an appropriate fixpoint language. To finish, we introduce other possible equivalent definitions of parity automata (i.e., modal, first-order, chromatic and achromatic) and discuss the (dis)advantages of each perspective. One of the advantages of taking an automata approach to fixpoint logics is that their complexity can be divided in two simpler and clearly defined parts: a graph structure representing the repetitions (i.e., the states of the automata) and a transition map with a simple one-step logic. In Chapter 5 we focus on the latter part. We introduce the one-step logics that we use in this dissertation and carry on an in-depth study of them. Our objective is to provide normal forms and characterize several fragments of this logics (continuous, completely additive, etc.) The results of this analysis will be crucial in later chapters, when we prove properties of automata based on these languages. In Chapter 6 we give automata characterizations for a number of modal logics. The results of this chapter are obtained using parity automata based on modal one-step languages. We show that (1) test-free PDL and full PDL correspond to concrete classes of additive-weak parity automata; and (2) the continuous restriction of the μ-calculus corresponds to a concrete class of continuous-weak parity automata. These results are obtained via effective transformations from formulas to automata and vice-versa. In Chapter 7 we give automata characterizations for WMSO (weak monadic second-order logic) and WCL (weak chain logic), on the class of tree models. In this case, we use parity automata based on (extensions of) first-order logic (with equality). The main challenge of this chapter is to give simulation and projection theorems for the classes of continuous-weak and additive-weak parity automata. As a byproduct, we also obtain characterizations for the mentioned automata (and second-order logics) as fragments fixpoint logics. In Chapter 8 we use the tools developed in the previous chapters to prove novel bisimulation-invariance results. Namely, we prove that the bisimulation invariant fragment of WCL is PDL, and that the bisimulation-invariant fragment of WMSO is equivalent to the continuous restriction of the μ-calculus.