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.