Expressiveness of Monadic Second Order Logics on Infinite Trees of Arbitrary Branching Degree
Fabio Zanasi
Abstract:
In this thesis we study the expressive power of variants of monadic
second-order logic (MSO) on infinite trees by means of automata. In
particular we are interested in weak MSO and well-founded MSO, where
the second-order quantifiers range respectively over finite sets and
over subsets of well-founded trees. On finitely branching trees, weak
and well-founded MSO have the same expressive power and are both
strictly weaker than MSO. The associated class of automata (called
weak MSO-automata) is a restriction of the class characterizing
MSO-expressivity.
We show that, on trees with arbitrary branching degree, weak
MSO-automata characterize the expressive power of well-founded MSO,
which turns out to be incomparable with weak MSO. Indeed, in this
generalized setting, weak MSO gives an account of properties of the
‘horizontal dimension’ of trees, which cannot be described by means of
MSO or well-founded MSO formulae.
In analogy with the result of Janin and Walukiewicz for MSO and the
modal μ-calculus, this raises the issue of which modal logic captures
the bisimulation-invariant fragment of well-founded MSO and weak
MSO. We show that the alternation-free fragment of the modal
μ-calculus and the bisimulation-invariant fragment of well-founded MSO
have the same expressive power on trees of arbitrary branching
degree. We motivate the conjecture that weak MSO modulo bisimulation
collapses inside MSO and well-founded MSO.