\betagin{document}

\mathitaketitle

\betagin{abstract}
We prove that the bisimulation-invariant fragment of weak monadic second-order logic (WMSO) is equivalent to the fragment of the modal $\mathitu$-calculus where the application of the least fixpoint operator $\mathitu p.\textsc{var}phi$ is restricted to formulas $\textsc{var}phi$ that are continuous in $p$. Our proof is automata-theoretic in nature; in particular, we introduce a class of automata characterizing the expressive power of WMSO over tree models of arbitrary branching degree. The transition map of these automata is defined in terms of a logic $\ensuremath{\lque_1}\xspace$ that is the extension of first-order logic with a generalized quantifier $au$, where $au x. \varphi$ means that there are infinitely many objects satisfying $\varphi$. An important part of our work consists of a model-theoretic analysis of $\ensuremath{\lque_1}\xspace$.
\end{abstract}

\section{Introduction}
\mathitathcal{L_\mathitu}lebel{sec:intro}

\paragraph{Expressiveness modulo bisimilarity.}

This paper concerns the relative expressive power of some languages used for
describing properties of pointed labelled transitions systems, or Kripke
models.
The interest in such expressiveness questions stems from applications where
these structures model computational processes, and bisimilar pointed
structures represent the \emph{same} process.
Seen from this perspective, properties of transition structures are relevant
only if they are invariant under bisimilarity.
This explains the importance of bisimulation invariance results of the form
\betagin{equation*}

M \equiv L / {b_{I}s} \text{ (over $K$)}
\end{equation*}
stating that,  if one restricts attention to a certain class $K$ of transition
structures, one language $M$ is expressively complete with respect to the
relevant (i.e., bisimulation-invariant) properties that can be formulated in
another language $L$.
In this setting, generally $L$ is some rich yardstick formalism such as
first-order or monadic second-order logic, and $M$ is some modal-style
fragment of $L$, usually displaying much better computational behavior
than the full language $L$.

A seminal result in the theory of modal logic is van Benthem's Characterization
Theorem~\cite{vanBenthemPhD}, stating that every bisimulation-invariant
first-order formula $\alphapha(x)$ is actually equivalent to (the standard
translation of) a modal formula:
\betagin{equation*}

\ensuremath{\mathitathrm{ML}} \equiv \mathit{FO}/{b_{I}s} \text{ (over the class of all LTSs)}.
\end{equation*}
Over the years, a wealth of variants of the Characterization Theorem have been
obtained.
For instance, Rosen proved that van Benthem's theorem is one of the few
preservation results that transfers to the setting of finite
models~\cite{rose:moda97}; for a recent, rich source of van Benthem-style
characterization results, see Dawar \& Otto~\cite{DawarO09}.
In this paper we are mainly interested is the work of Janin \&
Walukiewicz~\cite{Jan96}, who extended van Benthem's result to the setting
of fixpoint logics, by proving that the modal $\mathitu$-calculus ($\ensuremath{\mathitu\ML}\xspace$) is the
bisimulation-invariant fragment of monadic second-order
logic (\ensuremath{\mathitathrm{MSO}}):
\betagin{equation*}

\ensuremath{\mathitu\ML}\xspace \equiv \ensuremath{\mathitathrm{MSO}}/{b_{I}s} \text{ (over the class of all LTSs)}.
\end{equation*}

\paragraph{Bisimulation invariance for $\ensuremath{\mathitathrm{WMSO}}$.}
The yardstick logic that we consider in this paper is \emph{weak} monadic
second-order logic (\ensuremath{\mathitathrm{WMSO}}), a variant of monadic second-order logic where
the second-order quantifiers range over \emph{finite} subsets of the
transition structure rather than over arbitrary ones.
Our target will be to identify the bisimulation-invariant fragment of this
logic \ensuremath{\mathitathrm{WMSO}}.

Before moving on, we should stress the role of the ambient class $K$ in
bisimulation-invariance results.
Of particular importance in the setting of weak monadic second-order logic is
the difference between structures of finite versus arbitrary branching degree.
In the case of finitely branching models, it is not very hard to show that
$\ensuremath{\mathitathrm{WMSO}}$ is a (proper) fragment of \ensuremath{\mathitathrm{MSO}}, and it seems to be folklore that
$\ensuremath{\mathitathrm{WMSO}}/{b_{I}s}$ corresponds to \ensuremath{\mathitathrm{AFMC}}\xspace, the alternation-free fragment of the
modal $\mathitu$-calculus.
For binary trees, this result was proved by Arnold \& Niwi{\'n}ski in
\cite{ArnoldN01}.
In the case of structures of arbitrary branching degree, however, $\ensuremath{\mathitathrm{WMSO}}$
and $\ensuremath{\mathitathrm{MSO}}$ have \emph{incomparable} expressive power.
The fact that, in particular, $\ensuremath{\mathitathrm{WMSO}}$ does not correspond to a fragment of
\ensuremath{\mathitathrm{MSO}}, is witnessed by the class of infinitely branching structures, which
is clearly \ensuremath{\mathitathrm{WMSO}}-definable, cannot be defined in \ensuremath{\mathitathrm{MSO}}, since every
\ensuremath{\mathitathrm{MSO}}-definable class of trees contains a finitely branching
tree.\ensuremath{\mathitathrm{FO}}\xspaceotnote{As remarked in \cite{CateF11}, this follows from the automata characterization of MSO given in \cite{Walukiewicz96}.} 
For this reason, the relative expressive power of $\ensuremath{\mathitathrm{WMSO}}/{b_{I}s}$ and
$\ensuremath{\mathitathrm{MSO}}/{b_{I}s}$ is not a priori clear.
However, it is reasonable to think that $\ensuremath{\mathitathrm{WMSO}}/{b_{I}s}$ is strictly \emph{weaker} than \ensuremath{\mathitathrm{AFMC}}\xspace: the class of well-founded trees, which is definable in \ensuremath{\mathitathrm{AFMC}}\xspace by
the simple formula $\mathitu p. \Box p$, is not definable in \ensuremath{\mathitathrm{WMSO}}.\ensuremath{\mathitathrm{FO}}\xspaceotnote{This follows from the fact that $\ensuremath{\mathitathrm{WMSO}}$ can only define properties of trees that, from a topological point of view, are Borel, which is not the case of the class of trees defined by $\mathitu p. \Box p$--- see e.g. \cite{CateF11}.}

Incidentally, the question whether, conversely, there is a natural logic of
which the
bisimulation-invariant fragment corresponds to \ensuremath{\mathitathrm{AFMC}}\xspace was answered positively
by three of the present authors in~\cite{DBLP:conf/lics/FacchiniVZ13}, where they introduced
another variant of \ensuremath{\mathitathrm{MSO}}, called well-founded $\ensuremath{\mathitathrm{MSO}}$ (\ensuremath{\mathitathrm{WFMSO}}), and proved
that $\ensuremath{\mathitathrm{WFMSO}}/{b_{I}s} \equiv \ensuremath{\mathitathrm{AFMC}}\xspace$ (over the class of all LTSs).

The main result that we shall prove in this paper states that the
bisimulation-invariant fragment of $\ensuremath{\mathitathrm{WMSO}}$ is equivalent to a certain,
fragment $\ensuremath{\mathitu_{c}\ML}\xspace$ of the modal $\mathitu$-calculus.
\betagin{equation}
\mathitathcal{L_\mathitu}lebel{eq-main}
\ensuremath{\mathitu_{c}\ML}\xspace \equiv \ensuremath{\mathitathrm{WMSO}}/{b_{I}s}  \text{ (over the class of all LTSs)}.
\end{equation}
This fragment $\ensuremath{\mathitu_{c}\ML}\xspace$, which is strictly weaker than the alternation-free fragment
of $\ensuremath{\mathitu\ML}$, is characterized by a certain restriction on the application of
fixpoint operators, which involves the notion of \emph{(Scott) continuity}.

Continuity, an interesting property that features naturally in the semantics
of many (fixpoint) logics, in fact plays a key role throughout this paper.
For its definition, we consider how the meaning $\haak{\varphi}^{\mathitathbb{T}} \subseteq T$
of a formula $\varphi$ in some structure $\mathitathbb{T}$ (with domain $T$) depends on the meaning of a fixed
proposition letter or monadic predicate symbol $p$.
This dependence can be formalized as a map $\varphi^{\mathitathbb{T}}_{p}: \wp(T) \to
\wp (T)$, and if this map satisfies the condition
\betagin{equation}
\mathitathcal{L_\mathitu}lebel{eq-Sc}
\varphi^{\mathitathbb{T}}_{p}(X) = b_{I}gcup \Big\{ \varphi^{\mathitathbb{T}}_{a}(X') \mathitid X'
\text{ is a finite subset of } X \Big\},
\end{equation}
we say that $\varphi$ is \emph{continuous in $p$}.
The topological terminology stems from the observation that \eqref{eq-Sc}
expresses the continuity of the map $\varphi^{\mathitathbb{T}}_{p}$ with respect to the Scott
topology on $\wp(T)$. 
If we look at concrete cases, this definition can be given a different reading:
if $\varphi$ is a formula of the
modal $\mathitu$-calculus, \eqref{eq-Sc} means that $\varphi$ holds at some state $s$
of $\mathitathbb{T}$ iff we can shrink the interpretation of the proposition letter $p$
to some finite subset of the original interpretation, in such a way that
$\varphi$ holds at $s$ in the modified version of $\mathitathbb{T}$.

A syntactic \emph{characterization} of this property for the modal $\mathitu$-calculus
was obtained by Fontaine~\cite{Fontaine08,FV12}, and the definition of our fragment $\ensuremath{\mathitu_{c}\ML}\xspace$
uses this characterization as follows:
whereas in the full language of $\ensuremath{\mathitu\ML}$ the only syntactic condition on the
formation of a formula $\mathitu p. \varphi$ is that $\varphi$ is \emph{positive} in $p$,
for the fragment $\ensuremath{\mathitu_{c}\ML}\xspace$ this condition is strengthened to the requirement that
$\varphi$ is (syntactically) \emph{continuous} in $p$.
More precisely, the fragment $\ensuremath{\mathitu_{c}\ML}\xspace$ is defined as follows:

\betagin{definition}
For each set $aprop$ of
proposition letters, the fragment $\cont{\ensuremath{\mathitu\ML}\xspace}{aprop}$ of $\ensuremath{\mathitu\ML}\xspace$ which is \emph{continuous in $aprop$}
is given by the simultaneous induction
\betagin{equation*}
   \textsc{var}phi ::= q
   \mathitid \psi
   \mathitid \textsc{var}phi \lor \textsc{var}phi
   \mathitid \textsc{var}phi \mathitathcal{L_\mathitu}lend \textsc{var}phi
   \mathitid \Diamond \textsc{var}phi
   \mathitid \mathitu p.\alphapha
\end{equation*}
where $p\in\mathitathsf{P}$, $q \in aprop$, $\psi$ is a $aprop$-free $\ensuremath{\mathitu\ML}\xspace$-formula, and
$\alphapha \in \cont{\ensuremath{\mathitu\ML}\xspace}{aprop\cup\{p\}}$.

The formulas of the fragment $\ensuremath{\mathitu_{c}\ML}\xspace$ are then given by the following induction:
\betagin{equation*}
   \textsc{var}phi ::= p \mathitid \lnot \textsc{var}phi
    \mathitid \textsc{var}phi \lor \textsc{var}phi
    \mathitid  \Diamond \textsc{var}phi
    \mathitid \mathitu p.\alphapha
\end{equation*}
where $p \in \mathitathsf{P}$, and $\alphapha \in \cont{\ensuremath{\mathitu\ML}\xspace}{p}$.
\end{definition}

In fact we will prove, analogous to the result by Janin \& Walukiewicz,
the following strong version of the characterization result~\eqref{eq-main},
which provides an explicit translation, mapping any
bisimulation-invariant formula $\varphi$ in $\ensuremath{\mathitathrm{WMSO}}$ to an equivalent formula
$\varphi^{\bullet}$ in $\ensuremath{\mathitu_{c}\ML}\xspace$.

\betagin{theorem}
\mathitathcal{L_\mathitu}lebel{t:m1}
There are effective translations $(-)^{\bullet}: \ensuremath{\mathitathrm{WMSO}} \to \ensuremath{\mathitu_{c}\ML}\xspace$ and
$(-)_{\bullet}: \ensuremath{\mathitu_{c}\ML}\xspace \to \ensuremath{\mathitathrm{WMSO}}$ such that 
\betagin{enumerate}
\item A formula $\varphi$ of $\ensuremath{\mathitathrm{WMSO}}$ is
bisimulation invariant if and only if $\varphi \equiv \varphi^{\bullet}$, and
\item $\psi \equiv \psi_{\bullet}$ for every formula $\psi \in \ensuremath{\mathitu_{c}\ML}\xspace$.
\end{enumerate}
\end{theorem}

To see how this theorem implies \eqref{eq-main}, observe that part (i)
shows that $\ensuremath{\mathitathrm{WMSO}}/{b_{I}s} \leq \ensuremath{\mathitu_{c}\ML}\xspace$.
Part (ii) states that $\ensuremath{\mathitu_{c}\ML}\xspace \leq \ensuremath{\mathitathrm{WMSO}}\xspace$, so combined with the fact that
every formula in $\ensuremath{\mathitu_{c}\ML}\xspace \subseteq \ensuremath{\mathitu\ML}\xspace$ is bisimulation invariant, this gives the
converse, $\ensuremath{\mathitu_{c}\ML}\xspace \leq \ensuremath{\mathitathrm{WMSO}}/{b_{I}s}$.

\paragraph{Automata for $\ensuremath{\mathitathrm{WMSO}}$.}

As usual in this research area, our proof will be automata-theoretic in
nature.
More specifically, as the second main contribution of this paper, we
introduce a new class of parity automata that exactly captures the expressive
power of $\ensuremath{\mathitathrm{WMSO}}$ over the class of tree models of arbitrary branching degree.

Before we turn to a description of these automata, we first have a look at the
automata, introduced by Walukiewicz~\cite{Walukiewicz96}, corresponding to $\ensuremath{\mathitathrm{MSO}}$
(over tree models).
Fixing the set of proposition letters of our models as $\ensuremath{\mathitathsf{P}}$, we think of
$\wp(\ensuremath{\mathitathsf{P}})$ as an \emph{alphabet} or set of \emph{colors}.
We can then define an \ensuremath{\mathitathrm{MSO}}-automaton as a tuple $\mathitathstr{A} = \tup{A, \Delta,
\Omega, \q_{I}}$, where $A$ is a finite set of states, $\q_{I}$ an initial state, and $\Omega:
A \to \mathitathstr{N}$ is a parity function.

The transition function $\Delta$ maps a pair $(a,c) \in A \times \p(\ensuremath{\mathitathsf{P}})$ to a
sentence in the first-order language (with equality) $\ensuremath{Fo_1}\xspacee(A)$, of which the
state space $A$ provides the set of (monadic) predicates.

For a more precise definition, let $\ensuremath{Fo_1}\xspacee^+(A)$ denote the set of
those sentences in $\ensuremath{Fo_1}\xspacee(A)$ where all predicates in $A$ occur only positively;

we require that $\Delta: A \times \wp(\ensuremath{\mathitathsf{P}}) \to \ensuremath{Fo_1}\xspacee^+(A)$.

We shall refer to $\ensuremath{Fo_1}\xspacee$ as the \emph{one-step language} of $\ensuremath{\mathitathrm{MSO}}$-automata,
and denote the class of $\ensuremath{\mathitathrm{MSO}}$-automata with $\mathitathit{Aut}(\ensuremath{Fo_1}\xspacee)$.

The automata that we consider in this article run on labelled transition systems
and decide wether to accept or reject them. To take such decision we associate
an acceptance game for an
$\ensuremath{\mathitathrm{MSO}}$-automaton $\mathitathstr{A}$ and a transition system $\mathitathbb{T}$.
A match of this game consists of two players, $\exists$ and $\ensuremath{\mathitathrm{FO}}\xspacerall$, moving a
token from one position to another.
When such a match arrives at a so-called \emph{basic} position, i.e., a
position of the form $(a,t) \in A \times T$, the players consider the
sentence $\Delta(a,c_{t}) \in \ensuremath{Fo_1}\xspacee^+(A)$, where $c_{t} \in \wp(\ensuremath{\mathitathsf{P}})$ is the color
of $t$ (that is, the set of proposition letters true at $t$).
At this position $\exists$ has to turn the set $R[t]$ of successors of
$s$ into a \emph{model} for the formula $\Delta(a,c_{t})$ by coming up with an
interpretation $I$ of the monadic predicates $a \in A$ as subsets of $R[s]$,
so that the resulting first-order structure $(R[s],I)$ makes the
formula $\Delta(a,c_{t})$ true.

Walukiewicz's key result linking $\ensuremath{\mathitathrm{MSO}}$ to $\mathitathit{Aut}(\ensuremath{Fo_1}\xspacee)$ states that
\betagin{equation}
\ensuremath{\mathitathrm{MSO}} \equiv \mathitathit{Aut}(\ensuremath{Fo_1}\xspacee)
 \text{ (over tree models)},
\end{equation}
and the proof of this result proceeds by inductively showing that every formula
$\varphi$ in $\ensuremath{\mathitathrm{MSO}}$ can be effectively transformed into an equivalent
automaton $\mathitathstr{A}_{\varphi} \in \mathitathit{Aut}(\ensuremath{Fo_1}\xspacee)$.
For the details of this construction, a fairly intricate analysis of the
one-step logic $\ensuremath{Fo_1}\xspacee$ is required, crucially involving various normal
forms of the sentences of $\ensuremath{Fo_1}\xspacee(A)$.

In order to adapt this approach to the setting of \ensuremath{\mathitathrm{WMSO}}\xspace, observe that by
K\"onig's lemma, a subset of a tree $\mathitathbb{T}$ is finite iff it is both a subset of
a finitely branching subtree of $\mathitathbb{T}$ and \emph{noetherian}, that is, a subset
of a subtree of $\mathitathbb{T}$ that has no infinite branches.
This suggests that we may change the definition of $\ensuremath{\mathitathrm{MSO}}$-automata into one
of $\ensuremath{\mathitathrm{WMSO}}$-automata via two kinds of modifications, roughly speaking
corresponding to a horizontal and a vertical `dimension' of trees.

For the `vertical modification' we may turn to the literature on weak automata~\cite{MullerSaoudiSchupp92}.
The acceptance condition $\Omega$ of a parity automaton $\mathitathstr{A} =
\tup{A, \Delta, \Omega, \q_{I}}$ is \emph{weak} if $\Omega(a) = \Omega(a')$ whenever
the states $a$ and $a'$ belong to the same strongly connected component
(SCC) of the automaton. To see that the notion of connected component is well-defined
observe that for $\mathitathstr{A}$ we can associate a directed graph on $A$
such that $a,b \in A$ are connected iff $b$ occurs in $\Deltalta(a,c)$ for some $c \in \wp(\mathitathsf{P})$.

Let $\mathitathit{Aut}_{w}(\ensuremath{Fo_1}\xspacee)$ denote the set of $\ensuremath{\mathitathrm{MSO}}$-automata with a weak parity
condition.
It was proved in \cite{Zanasi:Thesis:2012} (see also \cite{DBLP:conf/lics/FacchiniVZ13}) that
\betagin{equation*}

\ensuremath{\mathitathrm{WFMSO}} \equiv \mathitathit{Aut}_{w}(\ensuremath{Fo_1}\xspacee) \text{ (over the class of all trees)},
\end{equation*}
with $\ensuremath{\mathitathrm{WFMSO}}$ denoting the earlier mentioned variant of $\ensuremath{\mathitathrm{MSO}}$ 
where second-order quantification is restricted to noetherian subsets of trees.
From this it easily follows that
\betagin{equation*}

\ensuremath{\mathitathrm{WMSO}} \equiv \mathitathit{Aut}_{w}(\ensuremath{Fo_1}\xspacee) \text{ (over the class of finitely
branching trees)},
\end{equation*}
since the noetherian subsets of a finitely branching trees correspond to the
finite ones.
Over the class of all tree models, however, $\ensuremath{\mathitathrm{WMSO}}$ is \emph{not} equivalent
to $\mathitathit{Aut}_{w}(\ensuremath{Fo_1}\xspacee)$, 
as is witnessesed by the earlier mentioned
class of well-founded trees, which can be defined in $\ensuremath{\mathitathrm{AFMC}}\xspace \leq \ensuremath{\mathitathrm{WFMSO}}$,
but not in $\ensuremath{\mathitathrm{WMSO}}$.

The hurdle to take, in order to find automata for WMSO on trees of
\emph{arbitrary} branching degree, concerns the horizontal dimension; the
main problem lies in finding the right one-step language for
$\ensuremath{\mathitathrm{WMSO}}$-automata.
An obvious candidate for this language would be weak monadic second-order logic
itself, or more precisely, its variant $\ensuremath{\mathitathrm{WMSO}_1}\xspace$ over the signature of monadic
predicates (corresponding to the automata states).
A very helpful observation, made by V\"a\"an\"anen~\cite{vaananen77}, states that
\[
\ensuremath{\mathitathrm{WMSO}_1}\xspace \equiv \ensuremath{\lque_1}\xspace,
\]
where $\ensuremath{\lque_1}\xspace$ is the extension of $\ensuremath{Fo_1}\xspacee$ with the generalized quantifier
$au$, where $au x. \varphi$ meaning that there are \emph{infinitely} many
objects satisfying $\varphi$.
Taking the \emph{full} language of $\ensuremath{\mathitathrm{WMSO}_1}\xspace$ or $\ensuremath{\lque_1}\xspace$ as our one-step language
would give too much expressive power: since $\ensuremath{\lque_1}\xspace$ extends $\ensuremath{Fo_1}\xspacee$,
we would find that, over tree models, $\mathitathit{Aut}_{w}(\ensuremath{\lque_1}\xspace)$ extends
$\mathitathit{Aut}_{w}(\ensuremath{Fo_1}\xspacee)$, whereas we already saw that $\mathitathit{Aut}_{w}(\ensuremath{Fo_1}\xspacee) \equiv
\ensuremath{\mathitathrm{WFMSO}}$ is incomparable to $\ensuremath{\mathitathrm{WMSO}}$.

It is here that we will crucially involve the notion of \emph{continuity}.
The automata corresponding to $\ensuremath{\mathitathrm{WMSO}}$ will be of the form $\mathitathstr{A} = \tup{A, \Delta, \Omega, \q_{I}}$,
where the transition map $\Delta: A \times \wp(\ensuremath{\mathitathsf{P}}) \to
{\ensuremath{\lque_1}\xspace}^+(A)$ is subject to the following two constraints, for all $a,a' \in A$
belonging to the same strongly connected component of $A$:
\betagin{description}
\itemsep 0 pt
\item[(weakness)] $\Omega(a) = \Omega(a')$, and
\item[(continuity)]
if $\Omega(a)$ is odd (resp. even), then for each colour $c\in \wp(\ensuremath{\mathitathsf{P}})$,
   $\Delta(a,c)$ is continuous (resp. co-continuous) in $a'$,
\end{description}
where co-continuity is a dual notion to continuity.
The class of these automata is denoted by $\mathitathit{Aut}_{cw}(\ensuremath{\lque_1}\xspace)$.

Consequently, for a proper definition of these automata we need a
\emph{syntactic} characterization of the $\ensuremath{\lque_1}\xspace(A)$-sentences that are
(co-)continuous in one (or more) monadic predicates of $A$.

For this purpose, we conduct a fairly detailed model-theoretic study of the
logic $\ensuremath{\lque_1}\xspace$ which we consider to be the third main
contribution of our work.
Similar to the results for $\ensuremath{Fo_1}\xspacee$, we provide normal forms for the
sentences of $\ensuremath{\lque_1}\xspace(A)$, and syntactic characterizations of the fragments
whose sentences are monotone (respectively continuous) in some monadic predicate $a \in A$.

To finish, we give constructions transforming \ensuremath{\mathitathrm{WMSO}}-formulas to
\ensuremath{\mathitathrm{WMSO}}-automata and vice-versa, witnessing that

\betagin{equation}
\mathitathcal{L_\mathitu}lebel{eq:m3}
\ensuremath{\mathitathrm{WMSO}} \equiv \mathitathit{Aut}_{cw}(\ensuremath{\lque_1}\xspace) \text{ (over tree models)}.
\end{equation}

\paragraph{Proof of main result.}

To conclude our introduction we briefly sketch the proof of our main result, 
Theorem~\ref{t:m1}(1).
Roughly speaking, we follow the bisimulation-invariance proof by Janin \& 
Walukiewicz, which revolves around relating two distinct types of automata, 
which correspond, respectively, to the logics $\ensuremath{\mathitathrm{MSO}}$ and $\ensuremath{\mathitu\ML}\xspace$.
More precisely, these two automaton types are given as $\mathitathit{Aut}(\ensuremath{Fo_1}\xspacee)$ and
$\mathitathit{Aut}(\ensuremath{Fo_1}\xspace)$, where the one-step languages are first-order 
logic respectively with and without equality.
What we will add to their proof is the insight from~\cite{Venxx} that the
required relation between $\mathitathit{Aut}(\ensuremath{Fo_1}\xspacee)$ and $\mathitathit{Aut}(\ensuremath{Fo_1}\xspace)$ already follows
from results relating the respective one-step languages.

In our setting, we need to identify automata corresponding to the fragment
$\ensuremath{\mathitu_{c}\ML}\xspace$.
For this purpose we introduce the class $\mathitathit{Aut}_{cw}(\ensuremath{Fo_1}\xspace)$ consisting of those
automata in $\mathitathit{Aut}(\ensuremath{Fo_1}\xspace)$ that satisfy similar weakness and continuity 
conditions as the ones in $\mathitathit{Aut}_{cw}(\ensuremath{\lque_1}\xspace)$:
\betagin{equation}
\mathitathcal{L_\mathitu}lebel{eq:autF}
\ensuremath{\mathitu_{c}\ML}\xspace \equiv \mathitathit{Aut}_{cw}(\ensuremath{Fo_1}\xspace) \text{ (over the class of all LTSs)}.
\end{equation}

As the key step in our proof then, we will provide a translation 
$(-)^{\bullet}: \ensuremath{\lque_1}\xspace \to \ensuremath{Fo_1}\xspace$ which naturally induces a transformation 
$(-)^{\bullet}: \mathitathit{Aut}_{cw}(\ensuremath{\lque_1}\xspace) \to \mathitathit{Aut}_{cw}(\ensuremath{Fo_1}\xspace)$.
As a consequence of the nice model-theoretic properties of the translation at 
the one-step level, the automaton transformation satisfies, for all 
transition systems $\mathitathstr{T}$:
\betagin{equation}
\mathitathcal{L_\mathitu}lebel{eq:crux-i}
\mathitathstr{A}^{\bullet} \text{ accepts } \mathitathstr{T} \text{ iff } \mathitathstr{A} \text{ accepts 
} \omegaegaunrav{\mathitathstr{T}}
\end{equation}
where $\omegaegaunrav{\mathitathstr{T}}$ is the $\omega$-unravelling of $\mathitathstr{T}$.
It easily follows from \eqref{eq:crux-i} that a \ensuremath{\mathitathrm{WMSO}}-automaton $\mathitathstr{A}$
is bisimulation invariant iff $\mathitathstr{A}\equiv \mathitathstr{A}^{\bullet}$, and so 
Theorem~\ref{t:m1}(1) follows by \eqref{eq:m3} and \eqref{eq:autF}.

\paragraph{Overview of paper.}
In the next section we give a precise definition of the preliminaries required to understand this article. In Section~\ref{sec:onestep} we define the one-step logics that will be used through the paper and give normal forms and syntactic characterizations of their monotone and (co-)continuous fragments. In Section~\ref{sec:aut} we formally define \ensuremath{\mathitathrm{WMSO}}\xspace-automata and show that from every \ensuremath{\mathitathrm{WMSO}}\xspace-formula we can construct an equivalent \ensuremath{\mathitathrm{WMSO}}\xspace-automaton. In Section~\ref{sec:aut-to-formula_wmso} we prove the converse, that is, for every \ensuremath{\mathitathrm{WMSO}}\xspace-automaton we can construct an equivalent \ensuremath{\mathitathrm{WMSO}}\xspace-formula, this finishes the automata characterization of \ensuremath{\mathitathrm{WMSO}}\xspace over tree models. Finally, in Section~\ref{sec:char} we prove the main result of the paper, namely that the fragment $\ensuremath{\mathitu_{c}\ML}\xspace$ is the bisimulation-invariant fragment of \ensuremath{\mathitathrm{WMSO}}\xspace.

\section{Preliminaries}\mathitathcal{L_\mathitu}lebel{sec:prel}

\subsection{Transition systems and trees} \mathitathcal{L_\mathitu}lebel{ssec:prelim_trees}

Throughout this article we fix a set $\mathitathsf{P}$ of elements that will be called
\emph{proposition letters} and denoted with small Latin letters $p, q, \ldots$ .
We denote with $C$ the set $\wp (\mathitathsf{P})$ of \emph{labels} on $\mathitathsf{P}$; it will be
convenient to think of $C$ as an \emph{alphabet}.
Given a binary relation $R \subseteq X \times Y$, for any element $x \in X$,
we indicate with $R[x]$ the set $\compset{ y \in Y \mathitid (x,y) \in R}$ while $R^+$
and $R^{*}$ are defined respectively as the transitive closure of~$R$ and
the reflexive and transitive closure of~$R$. The set $\mathitathsf{Ran}(R)$ is defined as $b_{I}gcup_{x\in X}R[x]$.

A \emph{$C$-labeled transition system} (LTS) is a tuple $\mathitathbb{T} = \tup{T,R,\sigma,s_I}$ where
$T$ is the universe or domain of $\mathitathbb{T}$, $\sigma:T\to\wp(\mathitathsf{P})$ is a marking,
$R\subseteq T^2$ is the accessibility relation and $s_I \in T$ is a distinguished node.
We use $|\mathitathbb{T}|$ to denote the domain of $\mathitathbb{T}$.

Observe that the marking ${\sigma:T\to\wp(\mathitathsf{P})}$ can be seen as a valuation $\tscolors^Flat:\mathitathsf{P}\to\wp (T)$ given by $\tscolors^Flat(p) = \{s \in T \mathitid p\in \sigma(s)\}$.

A \emph{$C$-tree} is a LTS in which every node can
be reached from $s_I$, and every node except $s_I$ has a unique predecessor;
the distinguished node $s_I$ is called the \emph{root} of $\mathitathbb{T}$.
Each node $s \in T$ uniquely defines a subtree of $\mathitathbb{T}$ with carrier
$R^{*}[s]$ and root $s$. We denote this subtree by ${\mathitathbb{T}.s}$.
We use the term \emph{tree language} as a synonym of class of $C$-trees.

The tree unravelling of an LTS $\mathitathbb{T}$ is given by $\unravel{\mathitathbb{T}} := \tup{T_P,R_P,\sigma',s_I}$ where $T_P$ is the set of finite paths in $\mathitathbb{T}$ stemming from $s_I$, $R_P(t,t')$ iff $t'$ is an extension of $t$ and the color of a path $t\in T_P$ is given by the color of its last node in $T$. The $\omegaega$-unravelling $\omegaegaunrav{\mathitathbb{T}}$ of $\mathitathbb{T}$ is an unravelling which has $\omegaega$-many copies of each node different from the root.

A \emph{$p$-variant} of a transition system $\mathitathbb{T} = \tup{T,R,\sigma,s_I}$
is a $\p (\mathitathsf{P}\cup\{p\})$-transition system $\tup{T,R,\sigma',s_I}$
such that $\sigma'(s)\setminus\{p\} = \sigma(s)$ for all $s \in T$.
Given a set $S \subseteq T$, we let $\mathitathbb{T}[p\mathitapsto S]$ denote the $p$-variant

where $p \in \sigma'(s)$ iff $s \in S$.

Let $\textsc{var}phi \in \ensuremath{\mathitathcal{L}}\xspace$ be a formula of some logic $\ensuremath{\mathitathcal{L}}\xspace$,
we use $\ext{\textsc{var}phi} = \compset{\mathitathbb{T} \mathitid \mathitathbb{T} \mathitathbb{T}s \textsc{var}phi}$ to denote the class
of transition systems that make $\textsc{var}phi$ true.

A class $\mathitathcallass$ of transition systems is said to be \emph{$\ensuremath{\mathitathcal{L}}\xspace$-definable} if there
is a formula $\textsc{var}phi \in \ensuremath{\mathitathcal{L}}\xspace$ such that $\ext{\textsc{var}phi} = \mathitathcallass$.
We use the notation $\textsc{var}phi \equiv \psi$ to mean that $\ext{\textsc{var}phi} = \ext{\psi}$ and given two logics
$\ensuremath{\mathitathcal{L}}\xspace, \ensuremath{\mathitathcal{L}}\xspace'$ we use $\ensuremath{\mathitathcal{L}}\xspace \equiv \ensuremath{\mathitathcal{L}}\xspace'$ when the $\ensuremath{\mathitathcal{L}}\xspace$-definable and $\ensuremath{\mathitathcal{L}}\xspace'$-definable
classes of models coincide.

\textit{Convention.}
Throughout this paper, we will only consider transition systems $\mathitathbb{T}$
in which $R[s]$ is non-empty for every node $s \in T$.
In particular this means that every tree we consider is \emph{leafless}.
All our results, however, can easily be lifted to the general case.

\subsection{Games}

We introduce some terminology and background on infinite games.
All the games that we consider involve two players called \emph{\'Eloise}
($\exists$) and \emph{Abelard} ($\ensuremath{\mathitathrm{FO}}\xspacerall$).
In some contexts we refer to a player $\Pi$ to specify a
a generic player in $\{\exists,\ensuremath{\mathitathrm{FO}}\xspacerall\}$.

Given a set $A$, by $A^*$ and $A^\omegaega$ we denote respectively the set of
words (finite sequences) and streams (or infinite words) over $A$.

A \emph{board game} $\mathitathcal{G}$ is a tuple $(G_{\exists},G_{\ensuremath{\mathitathrm{FO}}\xspacerall},E,\text{\sl Win})$,
where $G_{\exists}$ and $G_{\ensuremath{\mathitathrm{FO}}\xspacerall}$ are disjoint sets whose union
$G=G_{\exists}\cup G_{\ensuremath{\mathitathrm{FO}}\xspacerall}$ is called the \emph{board} of $\mathitathcal{G}$,
$E\subseteq G \times G$ is a binary relation encoding the \emph{admissible
moves}, and $\text{\sl Win} \subseteq G^{\omegaega}$ is a \emph{winning condition}.
An \emph{initialized board game} $\mathitathcal{G}@u_I$ is a tuple
$(G_{\exists},G_{\ensuremath{\mathitathrm{FO}}\xspacerall},u_I, E,\text{\sl Win})$ where

$u_I \in G$ is the
\emph{initial position} of the game.
When $\text{\sl Win}$ is  given by a parity function
$\Omega: G \to \omegaega$ we say that $\mathitathcal{G}$ is a parity game and sometimes
simply write $\mathitathcal{G}=(G_{\exists},G_{\ensuremath{\mathitathrm{FO}}\xspacerall},E,\Omega)$.

Given a board game $\mathitathcal{G}$, a \emph{match} of $\mathitathcal{G}$ is simply a path
through the graph $(G,E)$; that is, a sequence $\pi = (u_i)_{i< \alphapha}$ of
elements of $G$, where $\alphapha$ is either $\omegaega$ or a natural number,
and $(u_i,u_{i+1}) \in E$ for all $i$ with $i+1 < \alphapha$.
A match of $\mathitathcal{G}@u_{I}$ is supposed to start at $u_{I}$.
Given a finite match $\pi = (u_i)_{i< k}$ for some $k<\omegaega$, we call
$\mathit{last}(\pi) := u_{k-1}$ the \emph{last position} of the match; the
player $\Pi$ such that $\mathit{last}(\pi) \in G_{\Pi}$ is supposed to move
at this position, and if $E[\mathit{last}(\pi)] = \emptyset$, we say that
$\Pi$ \emph{got stuck} in $\pi$.

A match $\pi$ is called \emph{total} if it is either finite, with one of the
two players getting stuck, or infinite. Matches that are not total are called
\emph{partial}.
Any total match $\pi$ is \emph{won} by one of the players:
If $\pi$ is finite, then it is won by the opponent of the player who gets stuck.
Otherwise, if $\pi$ is infinite, the winner is $\exists$ if $\pi \in
\text{\sl Win}$, and $\ensuremath{\mathitathrm{FO}}\xspacerall$ if $\pi \not\in \text{\sl Win}$.

Given a board game $\mathitathcal{G}$ and a player $\Pi$, let $\pmatches{G}{\Pi}$ denote
the set of partial matches of $\mathitathcal{G}$ whose last position belongs to player
$\Pi$.
A \emph{strategy for $\Pi$} is a function $f:\pmatches{G}{\Pi}\to G$.
A match $\pi  = (u_i)_{i< \alphapha}$ of $\mathitathcal{G}$ is
\emph{$f$-guided} if for each $i < \alphapha$ such that $u_i \in G_{\Pi}$ we
have that $u_{i+1} = f(u_0,\dots,u_i)$.

Let $u \in G$ and a $f$ be a strategy for $\Pi$.
We say that $f$ is a \emph{surviving strategy} for $\Pi$ in $\mathitathcal{G}@u$ if

\betagin{enumerate}
  \item[(i)] For each $f$-guided partial match $\pi$ of $\mathitathcal{G}@u$, if $\mathit{last}(\pi)$
  is in $G_{\Pi}$ then $f(\pi)$ is legitimate, that is,
  $(\mathit{last}(\pi),f(\pi)) \in E$.
\end{enumerate}

We say that $f$ is a \emph{winning strategy} for $\Pi$ in $\mathitathcal{G}@u$ if, additionally, 

\betagin{enumerate}
  \item[(ii)] $\Pi$ wins each $f$-guided total match of $\mathitathcal{G}@u$.
\end{enumerate}

If $\Pi$ has a winning winning strategy for $\mathitathcal{G}@u$ then $u$ is called a \emph{winning position} for $\Pi$ in $\mathitathcal{G}$.
The set of positions of $\mathitathcal{G}$ that are winning for $\Pi$ is denoted by $\text{\sl Win}_{\Pi}(\mathitathcal{G})$.
A strategy $f$ is called \emph{positional} if $f(\pi) = f(\pi^{\prime})$ for each $\pi,\pi^{\prime} \in \mathitathsf{Dom}(f)$ with $\mathit{last}(\pi) = \mathit{last}(\pi^{\prime})$.
A board game $\mathitathcal{G}$ with board $G$ is \emph{determined} if $G = \text{\sl Win}_{\exists}(\mathitathcal{G}) \cup \text{\sl Win}_{\ensuremath{\mathitathrm{FO}}\xspacerall}(\mathitathcal{G})$, that is, each $u \in G$ is a winning position for one of the two players.

\betagin{fact}[Positional Determinacy of Parity Games~\cite{EmersonJ91,Mostowski91Games}]
\mathitathcal{L_\mathitu}lebel{THM_posDet_ParityGames}
For each parity game $\mathitathcal{G}$, there are positional strategies $f_{\exists}$
and $f_{\ensuremath{\mathitathrm{FO}}\xspacerall}$ respectively for player $\exists$ and $\ensuremath{\mathitathrm{FO}}\xspacerall$, such that
for every position $u \in G$ there is a player $\Pi$ such that $f_{\Pi}$ is a
winning strategy for $\Pi$ in $\mathitathcal{G}@u$.
\end{fact}

From now on, we always assume that each strategy we work with in parity games
is positional. Moreover, we think of a positional strategy $f_\Pi$ for player $\Pi$
as a function $f_\Pi:G_\Pi\to G$.

\input{paraut}

\subsection{Weak monadic second-order logic}

\betagin{definition}
The \emph{weak monadic second-order logic} on a set of predicates $\mathitathsf{P}$ is given by
$$\textsc{var}phi ::= \here{p} \mathitid p \sqsubseteq q \mathitid R(p,q) \mathitid \lnot\textsc{var}phi \mathitid \textsc{var}phi\lor\textsc{var}phi \mathitid \exists p.\textsc{var}phi$$
where $p,q \in \mathitathsf{P}$. We denote this logic by $\ensuremath{\mathitathrm{WMSO}}\xspace(\mathitathsf{P})$ and omit $\mathitathsf{P}$ when the set of proposition letters is clear from context.
We  adopt the standard convention that no letter is both free and bound in $\textsc{var}phi$.
\end{definition}

\betagin{definition}\mathitathcal{L_\mathitu}lebel{def:wmso}
Let $\mathitathbb{T} = \tup{T,R,\sigma, s_I}$ be a LTS, the semantics of \ensuremath{\mathitathrm{WMSO}}\xspace is defined as follows

\betagin{align*}
\mathitathbb{T} \mathitathbb{T}s \here{p} & auad\text{ iff }auad  \tscolors^Flat(p) = \compset{s_I} \\
\mathitathbb{T} \mathitathbb{T}s p \sqsubseteq q & auad\text{ iff }auad  \tscolors^Flat(p) \subseteq \tscolors^Flat(q) \\
\mathitathbb{T} \mathitathbb{T}s R(p,q) & auad\text{ iff }auad  \text{for every $s\in \tscolors^Flat(p)$ there exists $t\in \tscolors^Flat(q)$ such that $sRt$} \\
\mathitathbb{T} \mathitathbb{T}s \lnot\textsc{var}phi & auad\text{ iff }auad  \mathitathbb{T} \not\mathitathbb{T}s \textsc{var}phi \\
\mathitathbb{T} \mathitathbb{T}s \textsc{var}phi\lor\psi & auad\text{ iff }auad  \mathitathbb{T} \mathitathbb{T}s \textsc{var}phi \text{ or } \mathitathbb{T} \mathitathbb{T}s \psi \\
\mathitathbb{T} \mathitathbb{T}s \exists p.\textsc{var}phi & auad\text{ iff }auad  \text{there is a \emph{finite} set $X \subseteq_\omegaega T$ such that $\mathitathbb{T}[p\mathitapsto X] \mathitathbb{T}s \textsc{var}phi$}
\end{align*}
\end{definition}

\betagin{remark}
The reader may have expected a more standard two-sorted language for second-order logic, for example given by

$$
\textsc{var}phi ::= p(x)

\mathitid R(x,y)
\mathitid x \ensuremath{\mathitathrm{FO}}\xspaceeq y
\mathitid \neg \textsc{var}phi
\mathitid \textsc{var}phi \lor \textsc{var}phi
\mathitid \exists x.\textsc{var}phi
\mathitid \exists p.\textsc{var}phi
$$
where $p \in \mathitathsf{P}$, $x,y \in \ensuremath{\mathitathrm{FO}}\xspacevar$ (individual variables), 
and $\ensuremath{\mathitathrm{FO}}\xspaceeq$ is the symbol for equality.
Both definitions can be proved to be equivalent, however, we choose to keep Definition~\ref{def:wmso} as it will be better suited to work with in the context of automata.
\end{remark}

\subsection{First-order logic with generalized quantifiers}
In this subsection we introduce an extension of first-order logic with so called generalized quantifiers. Our interest in this extension stems from the fact that it will allow us to define a variant of first-order logic that is expressively equivalent to weak monadic second order (see Section~\ref{sec:onestep}) and has nice technical features such as a normal form theorem.

Mostowski~\cite{Mostowski1957} defined (unary) generalized quantifiers as follows: a (unary) generalized quantifier ${\mathitathcal Q}$ is a collection of pairs $(J, X)$ with $X \subseteq J$, and satisfying the following condition

$$\text{If } b_{I}g( (J,X)\in {\mathitathcal Q}, \ |X|=|Y| \ \mathitathcal{L_\mathitu}lend \ | J \setminus X|=|K \setminus Y|b_{I}g) \text{ then } (K,Y)\in {\mathitathcal Q}.$$

\noindent The semantics of ${\mathitathcal Q}$ is defined by the following condition
$$
\mathitathbb{T}\mathitathbb{T}s {\mathitathcal Q}x. \varphi(x, \vlist{s}) \text{ iff } (T,\{t \mathitid \mathitathbb{T}\mathitathbb{T}s \varphi(t,\vlist{s}) \}) \in {\mathitathcal Q}.
$$

where we use $\vlist{s} := [s_1,\dots,s_n]$ to denote sequences or vectors of elements.

For the rest of this article we will focus on the generalized quantifier $au$ expressing that there exist infinitely many elements satisfying a certain condition. Formally, it is defined as

\[ au := \{(J,X) \mathitid |X| \geq \alphaeph_0\}.\]

The dual of $au$ is $\ensuremath{Forall^\infty}\xspace =\{(J,X) \mathitid |J\setminus X| < \alphaeph_0\}$. It is worth observing what is the intended meaning of this quantifier: $\ensuremath{Forall^\infty}\xspace x.\textsc{var}phi$ expresses that there are \emph{at most finitely many} elements \emph{falsifying} the formula $\textsc{var}phi$.

The extension of first-order logic with equality ($\ensuremath{\mathitathrm{FO}}\xspacee$) or without equality ($\ensuremath{\mathitathrm{FO}}\xspace$)
obtained by adding $au$ to the corresponding first-order language is denoted respectively by $\ensuremath{Fo^\infty}\xspace$ and $\ensuremath{Fo^\infty}\xspacee$.

\subsection{The Modal $\mathitu$-Calculus.}\mathitathcal{L_\mathitu}lebel{subsec:mu}
The language of the modal $\mathitu$-calculus ($\ensuremath{\mathitu\ML}\xspace$) on $\mathitathsf{P}$ is given by the following grammar:

\betagin{equation*}
    \textsc{var}phi\ ::= q \mathitid \neg q \mathitid \textsc{var}phi \mathitathcal{L_\mathitu}lend \textsc{var}phi \mathitid
    \textsc{var}phi \lor \textsc{var}phi \mathitid  \Diamond \textsc{var}phi \mathitid \Box \textsc{var}phi \mathitid
    \mathitu p.\textsc{var}phi \mathitid \nu p.\textsc{var}phi
\end{equation*}

where $p,q \in \mathitathsf{P}$ and $p$ is positive in $\textsc{var}phi$ (i.e., $p$ is not negated).
We use the standard convention that no variable is both free and bound in a formula and that every bound variable is fresh.

Let $p$ be a bound variable occuring in some formula $\textsc{var}phi \in \ensuremath{\mathitu\ML}\xspace$, we use $\deltalta_p$ to denote the binding definition of $p$, that is, the formula such that either $\mathitu p.\deltalta_p$ or $\nu p.\deltalta_p$ are subformulas of $\textsc{var}phi$.

The semantics of this language is completely standard. Let $\mathitathbb{T} = \tup{T,R,\sigma, s_I}$ be a transition system and $\textsc{var}phi \in \ensuremath{\mathitu\ML}\xspace$. We inductively define the \emph{meaning} $\ext{\textsc{var}phi}^{\mathitathbb{T}}$ which includes the following clauses for the least $(\mathitu)$ and greatest ($\nu$) fixpoint operators:

\betagin{align*}
  \ext{\mathitu x.\psi}^{\mathitathbb{T}}  & :=   b_{I}gcap \{S \subseteq T \mathitid S \supseteq \ext{\psi}^{\mathitathbb{T}[x\mathitapsto S]} \}  \\
  \ext{\nu x.\psi}^{\mathitathbb{T}}  & :=   b_{I}gcup \{S \subseteq T \mathitid S \subseteq \ext{\psi}^{\mathitathbb{T}[x\mathitapsto S]} \}
\end{align*}

We say that $\textsc{var}phi$ is \emph{true} in $\mathitathbb{T}$ (notation $\mathitathbb{T} \tscolorsdash \textsc{var}phi$) iff $s_I \in \ext{\textsc{var}phi}^{\mathitathbb{T}}$.

We will now describe the semantics defined above in game-theoretic terms. That is,
we will define the evaluation game $\mathitathcal{E}(\textsc{var}phi,\mathitathbb{T})$ associated with a formula $\textsc{var}phi \in \ensuremath{\mathitu\ML}\xspace$ and a transition system $\mathitathbb{T}$. This game is played by two players (\existsse and \ensuremath{\mathitathrm{FO}}\xspacerallard) moving through positions $(\xi,s)$ where $\xi$ is a subformula of $\textsc{var}phi$ and $s \in T$.

\betagin{table}[h]
\centering
\betagin{tabular}{|l|c|l|c|}
  \hline
  Position & Player & Admissible moves\\
  \hline
  $(\psi_1 \vee \psi_2,s)$ & $\exists$ & $\{(\psi_1,s),(\psi_2,s) \}$ \\
  $(\psi_1 \wedge \psi_2,s)$ & $\ensuremath{\mathitathrm{FO}}\xspacerall$ & $\{(\psi_1,s),(\psi_2,s) \}$ \\
  $(\Diamond\textsc{var}phi,s)$ & $\exists$ & $\{(\textsc{var}phi,t)\ |\ t \in R[s] \}$ \\
  $(\Box\textsc{var}phi,s)$ & $\ensuremath{\mathitathrm{FO}}\xspacerall$ & $\{(\textsc{var}phi,t)\ |\ t \in R[s] \}$ \\
  $(\mathitu p.\textsc{var}phi,s)$ & $-$ & $\{(\textsc{var}phi,s) \}$ \\
  $(\nu p.\textsc{var}phi,s)$ & $-$ & $\{(\textsc{var}phi,s) \}$ \\
  $(p,s)$ with $p$ bound in $\textsc{var}phi$ & $-$ & $\{(\deltalta_p,s) \}$ \\
  $(\lnot q,s) \in \mathitathsf{P} \times T$, $q$ free in $\textsc{var}phi$ and $q \notin \sigma(s)$ & $\ensuremath{\mathitathrm{FO}}\xspacerall$ & $\emptyset$\\
  $(\lnot q,s) \in \mathitathsf{P} \times T$, $q$ free in $\textsc{var}phi$ and $q \in \sigma(s)$ & $\exists$ & $\emptyset$\\
  $(q,s) \in \mathitathsf{P} \times T$, $q$ free in $\textsc{var}phi$ and $q \in \sigma(s)$ & $\ensuremath{\mathitathrm{FO}}\xspacerall$ & $\emptyset$\\
  $(q,s) \in \mathitathsf{P} \times T$, $q$ free in $\textsc{var}phi$ and $q \notin \sigma(s)$ & $\exists$ & $\emptyset$\\
  \hline
\end{tabular}
\caption{Evaluation game for the modal $\mathitu$-calculus}
\mathitathcal{L_\mathitu}lebel{egame_mucalc}
\end{table}

In an arbitrary position $(\xi,s)$ it is useful to think of
\existsse trying to show that $\xi$ is true at $s$, and of \ensuremath{\mathitathrm{FO}}\xspacerallard of trying to convince her that $\xi$ is false at $s$. The rules of the evaluation game are given in Table~\ref{egame_mucalc}.
Every finite match of this game is lost by the player that got stuck. To give a winning condition for an infinite match let $p$ be, of the bound variables of $\textsc{var}phi$ that get unravelled infinitely often, the one that is the highest in the syntactic tree of $\textsc{var}phi$. The winner of the match is \ensuremath{\mathitathrm{FO}}\xspacerallard if $p$ is a $\mathitu$-variable and \existsse if $p$ is a $\nu$-variable. We say that $\textsc{var}phi$ is true in $\mathitathbb{T}$ iff \existsse has a winning strategy in $\mathitathcal{E}(\textsc{var}phi,\mathitathbb{T})$.

b_{I}gskip
Formulas of the modal $\mathitu$-calculus are classified according to their
\emph{alternation depth}, which roughly is given as the maximal length of
a chain of nested alternating least and greatest fixpoint operators~\cite{Niwinski86}.
The \emph{alternation-free fragment} of the modal $\mathitu$-calculus~($\ensuremath{\mathitathrm{AFMC}}\xspace$) is the collection of
$\ensuremath{\mathitu\ML}\xspace$-formulas without nesting of least and greatest fixpoint operators.

\betagin{definition}
  Let $\textsc{var}phi$ be a formula of the modal $\mathitu$-calculus. We say that $\textsc{var}phi\in\ensuremath{\mathitathrm{AFMC}}\xspace$ iff for all subformulas $\mathitu p.\psi_1$ and $\nu q.\psi_2$ we have that $p$ is not free in $\psi_2$ and $q$ is not free in $\psi_1$.
\end{definition}

It is not difficult to see that, over arbitrary transition systems, this fragment is
less expressive than the whole $\ensuremath{\mathitu\ML}\xspace$. That is, there is a $\ensuremath{\mathitu\ML}\xspace$-formula
$\textsc{var}phi$ such that $\ext{\textsc{var}phi}$ is not $\ensuremath{\mathitathrm{AFMC}}\xspace$-definable~\cite{Park79}.

In order to properly define the fragment $\ensuremath{\mathitu_{c}\ML}\xspace \subseteq \ensuremath{\mathitathrm{AFMC}}\xspace$ which is of critical importance in this article, we are particularly interested in the \emph{continuous} fragment of the modal $\mathitu$-calculus. As observed in Section~\ref{sec:intro}, the abstract notion of continuity can be given a concrete interpretation in the context of $\mathitu$-calculus.

\betagin{definition}
Let $\textsc{var}phi \in \ensuremath{\mathitu\ML}\xspace$, and $q$ be a propositional variable. We say that \emph{$\textsc{var}phi$ is continuous in $q$} iff for every transition system $\mathitathbb{T}$ there exists some finite $S \subseteq_\omegaega \tscolors^Flat(q)$ such that
$$
\mathitathbb{T} \tscolorsdash \textsc{var}phi auad\text{iff}auad \mathitathbb{T}[q \mathitapsto S] \tscolorsdash \textsc{var}phi .
$$
\end{definition}

We can give a syntactic characterization of the fragment of $\ensuremath{\mathitu\ML}\xspace$ that captures this property. Given a set $aprop$ of propositional variables, we define the fragment of \ensuremath{\mathitu\ML}\xspace \emph{continuous} in $aprop$, denoted by $\cont{\ensuremath{\mathitu\ML}\xspace}{aprop}$, by induction in the following way
\betagin{equation*}
   \textsc{var}phi ::= q
   \mathitid \psi
   \mathitid \textsc{var}phi \lor \textsc{var}phi
   \mathitid \textsc{var}phi \mathitathcal{L_\mathitu}lend \textsc{var}phi
   \mathitid \Diamond \textsc{var}phi
   \mathitid \mathitu p.\alphapha
\end{equation*}

where $q \in aprop$, $p \in \mathitathsf{P} \setminus aprop$, $\alphapha \in \cont{\ensuremath{\mathitu\ML}\xspace}{aprop\cup\{p\}}$, and $\psi$ is a $aprop$-free $\ensuremath{\mathitu\ML}\xspace$-formula.

\betagin{proposition}[\cite{Fontaine08,FV12}]\mathitathcal{L_\mathitu}lebel{prop:FVcont}
A $\ensuremath{\mathitu\ML}\xspace$-formula is continuous in $q$ iff it is equivalent to a formula in the fragment $\cont{\ensuremath{\mathitu\ML}\xspace}{q}$.
\end{proposition}

Finally, we define $\ensuremath{\mathitu_{c}\ML}\xspace$ to be the fragment of $\ensuremath{\mathitu\ML}\xspace$ where the use of the least fixed point operator is restricted to the continuous fragment. Formally, it is defined as follows.

\betagin{definition}
Formulas of the fragment $\ensuremath{\mathitu_{c}\ML}\xspace$ are given by the following induction:
\betagin{equation*}
   \textsc{var}phi ::= q \mathitid \lnot \textsc{var}phi
    \mathitid \textsc{var}phi \lor \textsc{var}phi
    \mathitid \Diamond \textsc{var}phi
    \mathitid \mathitu p.\alphapha
\end{equation*}

where $p,q \in \mathitathsf{P}$, and $\alphapha \in \cont{\ensuremath{\mathitu\ML}\xspace}{p}$.
\end{definition}

\betagin{proposition}
Let $\textsc{var}phi \in \ensuremath{\mathitu_{c}\ML}\xspace$, the following hold
\betagin{enumerate}[(1)]
\itemsep 0pt
\item $\textsc{var}phi$ is an $\ensuremath{\mathitathrm{AFMC}}\xspace$-formula,
\item Every $\mathitu$-variable in $\textsc{var}phi$ is existential (i.e., is only in the scope of diamonds), and dually every $\nu$-variable in $\textsc{var}phi$ is universal (i.e., is only in the scope of boxes).
\end{enumerate}
\end{proposition}
\betagin{proof}
Both points are proved by an easy induction on the complexity of a formula. For the first one,  it is enough to notice that if $\textsc{var}phi \in \cont{\ensuremath{\mathitu\ML}\xspace}{q} \cap \ensuremath{\mathitathrm{AFMC}}\xspace$, then $\mathitu q. \textsc{var}phi \in \ensuremath{\mathitathrm{AFMC}}\xspace$ by definition of $\cont{\ensuremath{\mathitu\ML}\xspace}{q} $.
\end{proof}

As an immediate consequence of Proposition \ref{prop:FVcont} we have the following:

\betagin{corollary}\mathitathcal{L_\mathitu}lebel{cor:cont}
For every $\ensuremath{\mathitu_{c}\ML}\xspace$-formula $\mathitu p. \textsc{var}phi$, $\textsc{var}phi$ is continuous in $p$.
Fznote{can we say also that $\nu p. \textsc{var}phi$ is cocontinuous in $p$, on the base of the second part of Prop. 2.14(2)?}
\end{corollary}

\subsection{Bisimulation}
Bisimulation is a notion of behavioral equivalence between processes.
For the case of  transition systems, it is formally defined as follows.

\betagin{definition}
Let $\mathitathbb{T} = \tup{T, R, \sigma, s_I}$ and
$\mathitathbb{T}' = \tup{T', R', \sigma', s'_I}$ be transition systems.
A \emph{bisimulation} is a relation $Z \subseteq T \times T'$
such that for all $(t,t^{\prime}) \in Z$ the following holds:
\betagin{description}
  \itemsep 0 pt
  \item[(atom)] $p \in \sigma(t)$ iff $p \in \sigma^{\prime}(t')$ for all $p\in\mathitathsf{P}$;
  \item[(forth)] for all $s \in R[t]$ there is $s^{\prime} \in R^{\prime}[t^{\prime}]$ such that $(s,s^{\prime}) \in Z$;
  \item[(back)] for all $s^{\prime} \in R^{\prime}[t^{\prime}]$ there is $s \in R[t]$ such that $(s,s^{\prime}) \in Z$.
\end{description}

Two pointed transition systems $\mathitathbb{T}$ and $\mathitathbb{T}^{\prime}$ are
\emph{bisimilar} (denoted $\mathitathbb{T} b_{I}s \mathitathbb{T}^{\prime}$) if there is a
bisimulation $Z \subseteq T \times T^{\prime}$ containing $(s_I,s'_I)$.
\end{definition}

The following fact about tree unravellings will allow us to provide a proof of
Theorem~\ref{t:m1} by just proving it for tree languages.

\betagin{fact}\mathitathcal{L_\mathitu}lebel{prop:tree_unrav}
$\mathitathbb{T}$ and $\mathitathbb{T}^e$ are bisimilar, for every transition system $\mathitathbb{T}$.
\end{fact}

A class of transition systems $\mathitathcallass$ is \emph{bisimulation closed} if $\mathitathbb{T}
b_{I}s \mathitathbb{T}^{\prime}$ implies that $\mathitathbb{T} \in \mathitathcallass$ iff $\mathitathbb{T}^{\prime}
\in \mathitathcallass$, for all $\mathitathbb{T}$ and $\mathitathbb{T}^{\prime}$.
A formula $\textsc{var}phi \in \ensuremath{\mathitathcal{L}}\xspace$ is \emph{bisimulation-invariant} if $\mathitathbb{T} b_{I}s
\mathitathbb{T}^{\prime}$ implies that $\mathitathbb{T} \tscolorsdash \textsc{var}phi$ iff $\mathitathbb{T}^{\prime}
\tscolorsdash \textsc{var}phi$, for all $\mathitathbb{T}$ and $\mathitathbb{T}^{\prime}$.

\betagin{fact}
Each $\ensuremath{\mathitu\ML}\xspace$-definable class of transition systems is bisimulation closed.
\end{fact}

\section{One-step logics, normal forms and continuity}\mathitathcal{L_\mathitu}lebel{sec:onestep}

  Given a set of names $A$ we use $\ensuremath{\mathitathcal{L}}\xspace_1(A)$ to denote an arbitrary one-step language based on $A$.
  One-step formulas are interpreted over unary (or one-step) models $\mathitathbf{D} = (D,V:A\to\wp D)$.
  We use $\mathitathfrak{M}_1(A)$ to denote the class of all one-step models based on the set of names $A$.

In this section we define the one-steps logics that we use in the rest of the article, namely: one-step weak monadic second-order logic ($\ensuremath{\mathitathrm{WMSO}_1}\xspace$), one-step first-order logic with and without equality ($\ensuremath{Fo_1}\xspacee$, $\ensuremath{Fo_1}\xspace$) and one-step first-order logic with the $au$ quantifier ($\ensuremath{\lque_1}\xspace$). The main theorems of this section prove normal forms for these logics and give syntactical characterizations of the monotonic and continuous fragments that we use in later sections.

\betagin{definition}

Let $\ensuremath{\mathitathrm{FO}}\xspacevar$ be a set of (individual) variables. 
Given a set of names $A$ we define the set $\ensuremath{\mathitathrm{WMSO}_1}\xspace(A)$ of one-step weak monadic second-order formulas as the \emph{sentences} given by the following grammar

\betagin{align*}
\textsc{var}phi \ ::=  & \ a(x)

\mathitid x \ensuremath{\mathitathrm{FO}}\xspaceeq y

\mathitid \neg \textsc{var}phi
 \mathitid \textsc{var}phi \lor \textsc{var}phi

\mathitid \exists x.\textsc{var}phi

\mathitid \exists a.\textsc{var}phi 

\end{align*}

where $x,y \in \ensuremath{\mathitathrm{FO}}\xspacevar$, 
$a \in A$.
\end{definition}

\betagin{definition}
The set $\ensuremath{Fo_1}\xspacee(A)$ of one-step first-order sentences (with equality) is given by the sentences formed by
$$
\textsc{var}phi ::= a(x)

\mathitid x \ensuremath{\mathitathrm{FO}}\xspaceeq y

\mathitid \neg \textsc{var}phi
\mathitid \textsc{var}phi \lor \textsc{var}phi

\mathitid \exists x.\textsc{var}phi

$$
where $x,y\in \ensuremath{\mathitathrm{FO}}\xspacevar$, $a \in A$. The one-step logic $\ensuremath{Fo_1}\xspace(A)$ is as $\ensuremath{Fo_1}\xspacee(A)$ but without equality.
The set $\ensuremath{\lque_1}\xspace(A)$ of one-step first-order sentences with generalized quantifier $au$ (with equality)

is defined analogously by just adding the clauses $au x. \textsc{var}phi$ and $\ensuremath{Forall^\infty}\xspace x. \textsc{var}phi$.
\end{definition}

Without loss of generality, from now on we always assume that every bounded variable occurring in a sentence is bounded by an unique quantifier (generalized or not).

Recall that given a one-step logic $\ensuremath{\mathitathcal{L}}\xspace_1$ we write $\ensuremath{\mathitathcal{L}}\xspace_1^+(A)$ to denote the fragment
where every predicate $a\in A$ occurs only positively. The following observation will allow us to
work with the (one-sorted) language $\ensuremath{Fo_1}\xspacee$ instead of the (two-sorted) language $\ensuremath{\mathitathrm{WMSO}_1}\xspace$.

\betagin{fact}[\cite{vaananen77}]
$\ensuremath{\mathitathrm{WMSO}_1}\xspace(A) \equiv \ensuremath{\lque_1}\xspace(A)$.
\end{fact}

In the following subsections we provide a detailed model theoretic analysis of the one-step logics that we use in this article, specifically, we give

\betagin{itemize}
	\itemsep 0 pt
	\item Normal forms for arbitrary formulas of $\ensuremath{Fo_1}\xspace$, $\ensuremath{Fo_1}\xspacee$ and $\ensuremath{\lque_1}\xspace$.

	\item Strong forms of syntactic characterizations for the monotone and continuous fragments of several of the mentioned logics. Namely, for $\ensuremath{\mathitathcal{L}}\xspace_1 \in \{\ensuremath{Fo_1}\xspace,\ensuremath{Fo_1}\xspacee,\ensuremath{\lque_1}\xspace\}$ we provide
		\betagin{enumerate}[(a)]

			\item A fragment $\mathitonot{\ensuremath{\mathitathcal{L}}\xspace_1}{a}$ and a translation $(-)^\circ:\ensuremath{\mathitathcal{L}}\xspace_1(A)\to\mathitonot{\ensuremath{\mathitathcal{L}}\xspace_1}{a}(A)$ such that for every $\textsc{var}phi \in\ensuremath{\mathitathcal{L}}\xspace_1$ we have $\textsc{var}phi\equiv\textsc{var}phi^\circ$ iff $\textsc{var}phi$ is monotone in $a \in A$,

		\end{enumerate}

		for $\ensuremath{\mathitathcal{L}}\xspace_1 \in \{\ensuremath{Fo_1}\xspace,\ensuremath{\lque_1}\xspace\}$ we provide

		\betagin{enumerate}[(a)]
			\item[(b)] A fragment $\cont{\ensuremath{\mathitathcal{L}}\xspace_1}{a}$ and a translation $(-)^\vartriangle:\ensuremath{\mathitathcal{L}}\xspace_1(A)\to\cont{\ensuremath{\mathitathcal{L}}\xspace_1}{a}(A)$ such that for every $\textsc{var}phi \in\ensuremath{\mathitathcal{L}}\xspace_1$ we have $\textsc{var}phi\equiv\textsc{var}phi^\vartriangle$ iff $\textsc{var}phi$ is continuous in $a \in A$.Fcwarning{The real cont-translation is from $\mathitonot{\ensuremath{\mathitathcal{L}}\xspace_1}{a}(A)$}
		\end{enumerate}

		Moreover, we show that the latter translation also restricts to the fragment $\ensuremath{\mathitathcal{L}}\xspace^+_1$, i.e.,

		\betagin{enumerate}[(a)]
			\item[(c)] The restriction $(-)^\vartriangle_+:\ensuremath{\mathitathcal{L}}\xspace^+_1(A)\to\cont{\ensuremath{\mathitathcal{L}}\xspace^+_1}{a}(A)$ of $(-)^\vartriangle$ is such that for every $\textsc{var}phi \in\ensuremath{\mathitathcal{L}}\xspace^+_1$ we have $\textsc{var}phi\equiv\textsc{var}phi^\vartriangle_+$ iff $\textsc{var}phi$ is continuous in $a \in A$.
		\end{enumerate}

	\item Syntactic characterizations of the co-continuous fragments of $\ensuremath{Fo_1}\xspace$ and $\ensuremath{\lque_1}\xspace$.

	\item Normal forms for the monotone and continuous fragments.
\end{itemize}

\subsection{Normal forms}\mathitathcal{L_\mathitu}lebel{subsec:normalforms}
\input{normalforms.tex}

\subsection{One-step monotonicity}
\input{monotonicity.tex}

\subsection{One-step continuity}\mathitathcal{L_\mathitu}lebel{subsec:one-stepcont}
\input{continuity.tex}

\subsection{One-step co-continuity and Boolean duals}\mathitathcal{L_\mathitu}lebel{subsec:one-stepcocont}
\input{cocontinuity.tex}

\section{Automata for WMSO}\mathitathcal{L_\mathitu}lebel{sec:aut}

In this section we provide an automata-theoretic characterization of $\ensuremath{\mathitathrm{WMSO}}\xspace$.
As argued in the introduction, $\ensuremath{\mathitathrm{WMSO}}$-automata will be defined as the
automata in $\mathitathit{Aut}(\ensuremath{\lque_1}\xspace)$ that satisfy two additional properties: weakness
and continuity.
We now briefly discuss these properties in a slightly more general setting,
starting with weakness.

\betagin{definition}
\mathitathcal{L_\mathitu}lebel{def:weak}
Let $\mathitathcal{L}o$ be a one-step language, and let $\mathitathstr{A} = \tup{A,\Delta,\Omega,a_I}$
be in $\mathitathit{Aut}(\mathitathcal{L}o)$.
Given two states $a,b$ of $\mathitathstr{A}$,
we say that there is a transition from $a$ to $b$, notation: $a \leadsto b$,
if $b$ occurs in $\Delta(a,c)$ for some $c \in C$.
We let the \emph{reachability} relation $\preceq$ denote the reflexive-transitive
closure of the relation $\leadsto$.

A \emph{strongly connected $\preceq$-component} ($\preceq$-SCC) is a subset $M\subseteq A$ such that for every $a,b \in M$ we have $a \preceq b$ and $b \preceq c$. The SCC is called \emph{maximal} (MSCC) when $M\cup\{a\}$ ceases to be a SCC for any choice of $a \in A\setminus M$.

We say that $\Omega$ is a \emph{weak} parity condition, and $\mathitathstr{A}$ is a
\emph{weak} parity automaton if we have
\betagin{description}
\item[(weakness)] if $a \preceq b$ and $b \preceq a$ then $\Omega(a) = \Omega(b)$.

\end{description}
\end{definition}
\betagin{comment}
\betagin{tbs}
\item
story: weakness corresponds to noetherian projection
\item
Ex: \eqref{eq-wfmso} in introduction states that over the class of all
trees, the weak $\ensuremath{Fo_1}\xspacee$-automata correspond to the $\ensuremath{\mathitathrm{MSO}}$-variant
$\ensuremath{\mathitathrm{WFMSO}}$, where quantification is restricted to noetherian subsets.
\end{tbs}
\end{comment}

\betagin{remark}
Any weak parity automaton $\mathitathstr{A}$ is equivalent to a weak parity automaton

$\mathitathstr{A}'$ with $\Omega: A' \to \{0,1\}$. From now on we therefore consider only
weak parity automata with priorities $0$ and $1$.
\end{remark}

As explained in the introduction, the leading intuition is that weak parity automata are those unable to register non-trivial properties concerning the vertical `dimension' of input trees. Indeed on trees they characterize $\mathrm{WFMSO}$, that is, the fragment of $\mso$ where the quantification is restricted to \emph{well-founded} subsets of trees (corresponding to the notion of \emph{noetherian} subset if we consider arbitrary transition systems). We refer to the literature on weak automata \cite{MullerSaoudiSchupp92} and on $\mathrm{WFMSO}$ \cite{DBLP:conf/lics/FacchiniVZ13,Zanasi:Thesis:2012} for more details.

We now turn to the second condition that we will be interested in,
viz., continuity. Intuitively, this property expresses a constraint on how much of the horizontal `dimension' of an input tree the automaton is allowed to process. It will be instrumental in showing that the class of automata that we are going to shape characterizes $\ensuremath{\mathitathrm{WMSO}}\xspace$. The idea is that, as $\ensuremath{\mathitathrm{WMSO}}\xspace$-quantifiers range over finite sets, the weakeness condition corresponds to those sets being `vertically' finite (i.e. included in well-founded subtrees), whereas the continuity condition corresponds to them being `horizontally' finite (i.e. included in finitely branching subtrees).

\betagin{comment}
We now turn to the second property that we require of $\ensuremath{\mathitathrm{MSO}}$-automata,
viz., continuity.
Here the story is that requiring the transition map of our automata to meet
some continuity condition with respect to some states of the automaton, gives
us a grip on the `horizontal' dimension of quantification in $\ensuremath{\mathitathrm{WMSO}}$,
i.e., the dimension corresponding to the fact that finite subsets of a
tree $\mathitathstr{T}$ are subsets of a \emph{finitely} branching subtree of $\mathitathstr{T}$.

\betagin{tbs}
\item
Can we provide more insight here, or is it too technical?
\end{tbs}
\end{comment}

First we formulate our continuity condition abstractly in the setting of $\mathitathit{Aut}(\mathitathcal{L}o)$.
Given the semantics of the one-step language $\mathitathcal{L}o$, the (semantic) notion
of (co-)continuity applies to one-step formulas (see for instance
section~\ref{subsec:one-stepcont}). We can then formulate the following requirement on automata from $\mathitathit{Aut}(\mathitathcal{L}o)$:

\betagin{description}
\item[(continuity)] let $a,b$ be states such that both $a\preceq b$ and
$b \preceq a$, and let $c\in C$;

    if ${\Omega(b)}=1$ then $\Delta(b,c)$ is continuous in $a$.

    If $\Omega(b)=0$, then $\Delta(b,c)$ is co-continuous in $a$.

\end{description}

For the automata used in this article we need to combine the constraints for the horizontal and vertical dimensions, yielding automata with both the weakness and continuity constraints.

\betagin{definition}
A \emph{continuous-weak parity automaton} is an automaton $\ensuremath\mathitathbb{A}\xspace \in \mathitathit{Aut}(\mathitathcal{L}o)$ addittionally satisfying both the \textbf{(weakness)} and \textbf{(continuity)} conditions.
We let $\mathitathit{Aut}_{cw}(\ensuremath{\mathitathcal{L}}\xspace_1)$ denote the class of such automata.
\end{definition}

Observe that, so far, the continuity condition is given semantically.
However, given that the one-step languages that we are interested in have
a \emph{syntactic characterization} of continuity (see for example Theorem~\ref{thm:olquecont})
we will give concrete definitions of these automata that take advantage of the mentioned characterizations.

\betagin{definition}
A \emph{$\ensuremath{\mathitathrm{WMSO}}\xspace$-automaton} $\ensuremath\mathitathbb{A}\xspace = \tup{A,\Deltalta,\Omegaega,a_I}$ is an automaton $\ensuremath\mathitathbb{A}\xspace \in \mathitathit{Aut}(\ensuremath{\lque_1}\xspace)$ such that for all states $a,b \in A$ with $a \preceq b$ and $b\preceq a$ the following conditions hold:
\betagin{description}
	\itemsep 0 pt
	\item[(weakness)] $\Omega(a)=\Omega(b)$,
	\item[(continuity)] if $\Omega(a)$ is odd (resp. even) then, for each $c\in C$ we have
	   $\Delta(a,c) \in \cont{{\ensuremath{\lque_1}\xspace}^+}{b}(A)$ (resp. $\Delta(a,c) \in \cocont{{\ensuremath{\lque_1}\xspace}^+}{b}(A)$).
\end{description}
As the class of such automata coincides with $\mathitathit{Aut}_{cw}(\ensuremath{\lque_1}\xspace)$ we use the same notation for it.
\end{definition}

We have now arrived at the main theorem of this section, which takes care of
one direction of Theorem~\ref{t:m1}. The main theorem of this section states that

\betagin{theorem}
\mathitathcal{L_\mathitu}lebel{t:wmsoauto}
There is an effective construction transforming a $\ensuremath{\mathitathrm{WMSO}}$-formula $\varphi$
into a $\ensuremath{\mathitathrm{WMSO}}$-automaton $\mathitathstr{A}_{\varphi}$ that is equivalent
to $\varphi$ on the class of trees.
That is, for any tree $\mathitathstr{T}$,
\betagin{equation}
\mathitathstr{A}_{\varphi} \text{ accepts } \mathitathstr{T} \text{ iff } \mathitathstr{T} \mathitathbb{T}s {\varphi}.
\end{equation}
\end{theorem}

As usual, the proof of this theorem proceeds by induction on the complexity of
$\varphi$.
For the inductive steps of this proof, we need to verify that the class of
\ensuremath{\mathitathrm{WMSO}}\xspace-automata is closed under the boolean operations and finite projection.
Clearly, the latter closure property requires most of the work; we first
provide a simulation theorem that put $\ensuremath{\mathitathrm{WMSO}}\xspace$-automata in a suitable shape
for the projection construction.
The proofs in the next two sections are (nontrivial) modifications of the
analogous results proved in~\cite{DBLP:conf/lics/FacchiniVZ13}.

It will be convenient to use the following terminology.

\betagin{definition}
The \emph{tree language $\ensuremath{\mathitathcal{T}}(\ensuremath\mathitathbb{A}\xspace)$ recognized} by an automaton $\mathitathstr{A}$ is
defined as the collection of trees that are accepted by $\mathitathstr{A}$.
A class of trees is \emph{$\ensuremath{\mathitathrm{WMSO}}$-automaton recognizable} (or
\emph{recognizable}, if clear from context), if it is of the form
$\ensuremath{\mathitathcal{T}}(\ensuremath\mathitathbb{A}\xspace)$ for a $\ensuremath{\mathitathrm{WMSO}}$-automaton $\mathitathstr{A}$.
\end{definition}

\subsection{Simulation theorem}
\input{simulation.tex}

\subsection{Closure Properties}

In this subsection we prove that $\ensuremath{\mathitathrm{WMSO}}$-automata are closed under the 
operations corresponding to the connectives of $\ensuremath{\mathitathrm{MSO}}$, that is: union, 
complementation and projection with respect to finite sets.
We start with the latter.

\input{projection.tex}

\input{complementation.tex}

\subsection{Proof of Theorem \ref{t:wmsoauto}}

\betagin{proof} The proof is by induction on $\textsc{var}phi$.
\betagin{itemize}
  \item For the base case $\textsc{var}phi = p \sqsubseteq q$, the corresponding 
  $\ensuremath{\mathitathrm{WMSO}}\xspace$-automaton is provided in \cite[Ex. 2.6]{Zanasi:Thesis:2012}. 
  For the base case $\textsc{var}phi = R(p,q)$, we give the corresponding 
  $\ensuremath{\mathitathrm{WMSO}}\xspace$-automaton $\ensuremath\mathitathbb{A}\xspace_{R(p,q)} = \tup{A,\Deltalta,\Omegaega,a_I}$ below:
\betagin{eqnarray*}
        A &:=& \{a_0,a_1\}\\
        a_I &:=& a_0\\
  \Deltalta(a_0,c) &:=& \left\{
	\betagin{array}{ll}
           \exists x. a_1(x) \wedge \ensuremath{\mathitathrm{FO}}\xspacerall y. a_0(y) & \mathitbox{if }p \in c 
	\\ \ensuremath{\mathitathrm{FO}}\xspacerall x\ (a_0(x)) & \mathitbox{otherwise}
	\end{array}
\right. \\
  \Deltalta(a_1,c) &:=& \left\{
	\betagin{array}{ll}
        \top & \mathitbox{if }q \in c \\
        \bot & \mathitbox{otherwise}
	\end{array}
\right. \\
    \Omegaega(a_0) &:=& 0\\
    \Omegaega(a_1) &:=& 1.
\end{eqnarray*}
Note that the $\mathitathrm{MSO}$-automaton for $R(p,q)$ provided in 
\cite[Ex. 2.5]{Zanasi:Thesis:2012} is \emph{not} a $\ensuremath{\mathitathrm{WMSO}}\xspace$-automaton, as the 
continuity property does not hold.

\item
For the Boolean cases, where $\textsc{var}phi = \psi_1 \vee \psi_2$ or $\varphi = \neg\psi$
we refer to the closure properties of recognizable tree languages, see 
Theorem~\ref{t:cl-dis} and Theorem~\ref{t:cl-cmp}, 
respectivel.
  
\item 
For the case $\textsc{var}phi = \exists p. \psi$, consider the following chain of
equivalences, where $\ensuremath\mathitathbb{A}\xspace_{\psi}$ is given by the inductive hypothesis and 
${{\exists}_F p}.\ensuremath\mathitathbb{A}\xspace_{\psi}$ is constructed according to 
Definition \ref{DEF_fin_projection}:
\betagin{alignat*}{2}
{{\exists}_F p}.\ensuremath\mathitathbb{A}\xspace_{\psi} \text{ accepts }\mathitb{T} 
   & \text{ iff }
     \ensuremath\mathitathbb{A}\xspace_{\psi} \text{ accepts } \mathitb{T}[p \mathitapsto X], 
     \text{ for some } X \subseteq_{\omega} T
   & auad\text{(Lemma~\ref{PROP_fin_projection})}
\\ & \text{ iff }
     \mathitb{T}[p \mathitapsto X] \mathitathbb{T}s \psi,
     \text{ for some } X \subseteq_{\omega} T
   & auad\text{(induction hyp.)}
\\ & \text{ iff }
    \mathitb{T} \mathitathbb{T}s \exists p. \psi
   & auad\text{(semantics $\ensuremath{\mathitathrm{WMSO}}\xspace$)}
\end{alignat*}
\end{itemize}
\end{proof}

\section{From $\ensuremath{\mathitathrm{WMSO}}$-automata to $\ensuremath{\mathitathrm{WMSO}}$}\mathitathcal{L_\mathitu}lebel{sec:aut-to-formula_wmso}

In what follows, we verify that WMSO-automata capture exactly the expressive power of WMSO on the class of tree models. Since we already proved the direction from formulas into automata (Theorem~\ref{t:wmsoauto}), we just have to verify that there is a sound translation going in the other direction.

For this purpose, we first introduce a fixpoint extension of first-order logic.

\subsection{Fixpoint extension of  first-order logic}

Let our first-order signature be composed of a set $\mathitathsf{P}$ of monadic predicates (denoted with capital latin letters) and an unique binary predicate $R$.

Analogously to the modal $\mathitu$-calculus, the fixpoint extension of $\ensuremath{Fo^\infty}\xspacee(\mathitathsf{P})$ is defined by adding a fixpoint construction clause.

\betagin{definition}
The fixed point logic $\ensuremath{\mathitu\lque}\xspace(\mathitathsf{P})$ is given by:
$$
\textsc{var}phi ::= q(x) \mathitid R(x,y) \mathitid x \ensuremath{\mathitathrm{FO}}\xspaceeq y \mathitid \exists x.\textsc{var}phi \mathitid au x.\textsc{var}phi \mathitid \lnot\textsc{var}phi \mathitid \textsc{var}phi \mathitathcal{L_\mathitu}lend \textsc{var}phi \mathitid \mathitu p.\textsc{var}phi(p,x)
$$
where $p,q\in\mathitathsf{P}$, $x,y\in\ensuremath{\mathitathrm{FO}}\xspacevar$; moreover $p$ occurs only positively in $\textsc{var}phi(p,x)$ and $x$ is the only free variable in $\textsc{var}phi(p,x)$.
\end{definition}

The semantics of the fixpoint formula $\mathitu p. \varphi(p, x)$is the expected one. Given a model $\mathitathbb{T}$ and $s \in T$,  $\mathitathbb{T} \mathitathbb{T}s \mathitu p. \varphi(p, s)$ iff $s$ is in the least fixpoint of the  operator $F_\varphi:\wp(T)\to \wp(T)$ defined as $F_\varphi(S) := \{t \in T \mathitid \mathitathbb{T}[p \mathitapsto S] \mathitathbb{T}s \varphi(p, t) \}$.

Formulas of $\ensuremath{\mathitu\lque}\xspace$ may be also classified according to their alternation depth as it happens for the modal $\mathitu$-calculus.
The alternation-free fragment of $\ensuremath{\mathitu\lque}\xspace$ is thence defined as the collection of $\ensuremath{\mathitu\lque}\xspace$-formulas $\varphi$
without nesting of greatest and least fixpoint operators, i.e. such that, for any two subformulas $\mathitu p.\psi_1(p,y)$ and $\nu q. \psi_2(q,z)$, predicates $p$ and $q$ do not occur free respectively in $\psi_2(q,z)$ and $\psi_1(p,y)$.

\betagin{definition}
Given $p \in \mathitathsf{P}$, we say that $\textsc{var}phi \in \ensuremath{\mathitu\lque}\xspace(\mathitathsf{P})$ is
\betagin{itemize}
\item \emph{monotone in the predicate $p$} iff for every LTS $\mathitathbb{T}$ and assignment $g$, \[ \text{if }\mathitathbb{T}, g \mathitathbb{T}s \textsc{var}phi \text{ and $\tscolors^Flat(p) \subseteq E$, then }\mathitathbb{T}[p \mathitapsto E], g\mathitathbb{T}s \varphi\]

\item \emph{continuous in the predicate $p$} iff for every LTS $\mathitathbb{T}$ and assignment $g$ there exists some finite $S \subseteq_\omegaega \tscolors^Flat(p)$ such that
$$
\mathitathbb{T}, g \mathitathbb{T}s \textsc{var}phi auad\text{iff}auad \mathitathbb{T}[p \mathitapsto S], g \mathitathbb{T}s \textsc{var}phi .
$$
\end{itemize}
\end{definition}

In the next definition, we provide a definition of the continuous fragment of $\ensuremath{\mathitu\lque}\xspace$, reminiscent of the one defined in Theorem~\ref{thm:olquecont}.
\betagin{definition}
Let $\mathitathsf{Q}\subseteq \mathitathsf{P}$ be a set of monadic predicates. The fragment $\cont{\ensuremath{\mathitu\lque}\xspace}{\mathitathsf{Q}}(\mathitathsf{P})$ is defined by the following rules:
$$
\textsc{var}phi ::= \psi \mathitid q(x) \mathitid \exists x.\textsc{var}phi(x) \mathitid \textsc{var}phi \mathitathcal{L_\mathitu}lend \textsc{var}phi \mathitid \textsc{var}phi \lor \textsc{var}phi \mathitid \ensuremath{\mathitathbf{W}}\xspace x.(\textsc{var}phi,\psi) \mathitid \mathitu p. \varphi'(p, x)
$$
where $q \in \mathitathsf{Q}$, $\psi \in \ensuremath{\mathitu\lque}\xspace(\mathitathsf{P}\setminus \mathitathsf{Q})$, $p \in \mathitathsf{P} \setminus \mathitathsf{Q}$, $\ensuremath{\mathitathbf{W}}\xspace x.(\textsc{var}phi,\psi) := \ensuremath{\mathitathrm{FO}}\xspacerall x.(\textsc{var}phi(x) \lor \psi(x)) \mathitathcal{L_\mathitu}lend \ensuremath{Forall^\infty}\xspace x.\psi(x)$ and $\varphi'(p,x)$ is a formula with only $x$ free such that $\varphi'(p,x) \in \cont{\ensuremath{\mathitu\lque}\xspace}{\mathitathsf{Q} \cup\{p\}}(\mathitathsf{P})$.

\end{definition}

\betagin{lemma}\mathitathcal{L_\mathitu}lebel{lem:colqueiscont_mu}
If $\textsc{var}phi \in \cont{\ensuremath{\mathitu\lque}\xspace}{\mathitathsf{Q}}(\mathitathsf{P})$ then $\textsc{var}phi$ is continuous in (each predicate from) $\mathitathsf{Q}$.
\end{lemma}

\betagin{proof} First, notice that If $\textsc{var}phi \in \cont{\ensuremath{\mathitu\lque}\xspace}{\mathitathsf{Q}}(\mathitathsf{P})$ then $\textsc{var}phi$ is monotone  in (each predicate from) $\mathitathsf{Q}$. 
The proof goes then by induction on the complexity of $\textsc{var}phi$. For the all the cases except the fixpoint one, the proof is the same as the one for Lemma~\ref{lem:colqueiscont}. For $\varphi=\mathitu p. \varphi'(p, x)$, with $\varphi'(p,x) \in \cont{\ensuremath{\mathitu\lque}\xspace}{\mathitathsf{Q} \cup\{p\}}(\mathitathsf{P})$, the argument is the same as in~\cite[Lemma 1]{Fontaine08}.
\end{proof}

As for the modal $\mathitu$-calculus, we define the fragment $\ensuremath{\mathitu_{c}\lque}\xspace$ of $\ensuremath{\mathitu\lque}\xspace$ as the one where the use of the least fixed point operator is restricted to the continuous fragment. 

\betagin{definition}
The fragment $\ensuremath{\mathitu_{c}\lque}\xspace(\mathitathsf{P})$ of $\ensuremath{\mathitu\lque}\xspace(\mathitathsf{P})$ is given by the following restriction of the fixpoint operator to the contiuous fragment:
{\small
$$
\textsc{var}phi ::= q(x) \mathitid R(x,y) \mathitid x \ensuremath{\mathitathrm{FO}}\xspaceeq y \mathitid \exists x.\textsc{var}phi \mathitid au x.\textsc{var}phi \mathitid \lnot\textsc{var}phi \mathitid \textsc{var}phi \mathitathcal{L_\mathitu}lend \textsc{var}phi \mathitid \mathitu p.\textsc{var}phi'(p,x)
$$}
where $p,q\in\mathitathsf{P}$, $x,y\in\ensuremath{\mathitathrm{FO}}\xspacevar$; and $\textsc{var}phi'(p,x) \in \cont{\ensuremath{\mathitu\lque}\xspace}{\{p\}}(\mathitathsf{P})$ is such that $p$ occurs only positively in $\textsc{var}phi'$ and $x$ is the only free variable in $\textsc{var}phi'$.
\end{definition}

We now recall a useful property of fixpoint and continuity. Let $\varphi(p,x)$ a formula with only $x$ free.
Given a LTS $\mathitathbb{T}$, for every ordinal $\alphapha$, we define by induction the following sets:

\betagin{itemize}
	\itemsep 0 pt
	\item $\varphi^0(\emptyset):= \emptyset$,

	\item $\varphi^{\alphapha+1}(\emptyset):= \{ s \in T \mathitid \mathitathbb{T}[p \mathitapsto \varphi^\alphapha(\emptyset)] \mathitathbb{T}s \varphi(p, s)\}$,
	\item $\varphi^{\mathitathcal{L_\mathitu}lembda}(\emptyset):= b_{I}gcup_{\alphapha < \mathitathcal{L_\mathitu}lembda} \varphi^{\alphapha}(\emptyset)$, with $\mathitathcal{L_\mathitu}lembda$ limit.
\end{itemize}

If $\varphi$ is monotone in $p$, it is possible to show that $\varphi^{\betata+1}(\emptyset)= \varphi^{\betata}(\emptyset)$, for some ordinal $\betata$. Moreover, the set $\varphi^{\betata}(\emptyset)$ is the least fixpoint of $F_\varphi$ (cf. for instance \cite{ArnoldN01}).

A formula $\varphi(p, x)$ is said to be \emph{constructive} in $p$ if its least fixpoint is reached in at most $\omegaega$ steps, i.e., if for every model $\mathitathbb{T}$, the least fixpoint of $F_\varphi$ equals to $b_{I}gcup_{\alphapha < \omegaega} \varphi^{\alphapha}(\emptyset)$. From a local perspective, this means that a formula $\varphi(p, x)$ constructive in $p$ if for every model $\mathitathbb{T}$,  every node $s \in T$, whenever $\mathitu p. \varphi(p,x)$ is true at $s$, then $s$ belongs to some finite approximant $\varphi^{i+1}(\emptyset)$ of the least fixpoint of $F_\varphi$.
The next proposition is easily verified:

\betagin{proposition}\mathitathcal{L_\mathitu}lebel{prop:constructivity}
Let $\varphi(p,x)$ be a $\ensuremath{\mathitu\lque}\xspace$-formula with only $x$ free. If $\varphi(p,x)$ is continuous in $p$, then for every LTS $\mathitathbb{T}$, and every node $s \in T$, there is $i < \omegaega$ such that
\[\mathitathbb{T} \mathitathbb{T}s \mathitu p. \varphi(p,s) \text{ iff } s \in \varphi^{i+1}(\emptyset).\]
\end{proposition}

From the fact that sets $\varphi^{i+1}(\emptyset)$ are essentially defined as finite unfoldings and the previous Proposition~\ref{prop:constructivity}, we obtain the following.Fcwarning{More intuition on this?}

\betagin{proposition}\mathitathcal{L_\mathitu}lebel{prop:cor_constructivity}
Let $\varphi(p,x)$ be a $\ensuremath{\mathitu\lque}\xspace$-formula with only $x$ free and such that $\varphi(p,x)$ is continuous in $p$. Let $\mathitathbb{T}$ be a LTS, and $s \in T$. Then
$\mathitathbb{T} \mathitathbb{T}s \mathitu p. \varphi(p,s)$ iff there is a finite set $p^\mathitathbb{T} \subseteq_\omegaega T$ such that $s\in p^\mathitathbb{T}$ and $\mathitathbb{T}[p\mathitapsto p^\mathitathbb{T}] \mathitathbb{T}s \varphi(p,t)$  for every $t \in p^\mathitathbb{T}$.
\end{proposition}
 \betagin{proof}
 For the direction from left to right, assume that $\mathitathbb{T} \mathitathbb{T}s \mathitu p. \varphi(p,s)$. By Proposition~\ref{prop:constructivity}, we know that  there is $i< \omegaega$ such that $\mathitathbb{T}[p \mathitapsto \varphi^i(\emptyset)] \mathitathbb{T}s \varphi(p, s)$. The set $\varphi^i(\emptyset)$ need not to be finite. However,
 using this information, we are going construct a finite tree whose nodes $t$ are labelled by finite sets $X^m_j$, where $m$ is a node of $\mathitathbb{T}$ and $j \leq i$, satisfying the following condition:
 \betagin{enumerate}
\item  if $t$ is the root, then $t$ is labelled by $X_i^s$,
\item  if $t$ is labelled by $X_j^m=\{s_1, \dots, s_\ell\}$ and $j>0$, then $t$ has $\ell$  children and for every $s_i \in X_j^m$ there is an unique child $t'$ of $t$ labelled by $X_{j-1}^{n_i}$ where $m$ is a node,

\item for every node $t$ of the tree, if $t$ is labelled by $X_j^m$, then it holds that $X_j^m \subseteq \varphi^{j}(\emptyset)$.
\end{enumerate}
If we verify that $\mathitathbb{T}[p\mathitapsto p^\mathitathbb{T}] \mathitathbb{T}s \varphi(p,s)$ holds by taking as $p^\mathitathbb{T}$ the union of all labels of the nodes of the constructed tree, we can conclude for the proof of this direction.

As starting point of the inductive construction, we start by the empty tree.  Recall that we know that  $\mathitathbb{T}[p \mathitapsto \varphi^i(\emptyset)] \mathitathbb{T}s \varphi(p, s)$. Since $\varphi(p,x)$ is continuous in $p$, there is a finite set $X^s_i \subseteq \varphi^i(\emptyset)$ such that $\mathitathbb{T}[p \mathitapsto X^s_i] \mathitathbb{T}s \varphi(p, s)$. We then add a root to our tree and label it by $X^s_i$.
 Assume that at a leaf $s$ of our tree is labelled by $X^m_j$, for some $j < i$. If $X^m_j$ is empty, than we stop, else we proceed as follows. We know that $X^m_j\subseteq \varphi^{j}(\emptyset)$. This means that $\mathitathbb{T}[p \mathitapsto \varphi^{j-1}(\emptyset)] \mathitathbb{T}s \varphi(p, r)$, for every $r \in X_j^m$. By continuity, for each such $r$, there is a finite set $X^m_{j-1} \subseteq  \varphi^{j-1}(\emptyset)$ such that $\mathitathbb{T}[p \mathitapsto X^m_{j-1}(\emptyset)] \mathitathbb{T}s \varphi(p, r)$. For each $r \in X^m_j$ we thus add a child to $m$ and label it with $X^r_{j-1}$. By definition of $\varphi^{i+1}(\emptyset)$, the tree is finite. Let $X$ be the union of all labels of the constructed tree. $X$ is finite, and by monotonicity of $\varphi(p,x)$ we have that for every $m \in X \cup \{s\}$, $\mathitathbb{T}[p \mathitapsto X \cup \{s\}] \mathitathbb{T}s \varphi(p,m)$.

For the other direction, it's enough to notice that the smallest finite set $p^\mathitathbb{T} \subseteq T$ such that $\mathitathbb{T}[p\mathitapsto p^\mathitathbb{T}] \mathitathbb{T}s \varphi(p,s)$ and $\mathitathbb{T}[p\mathitapsto p^\mathitathbb{T}] \mathitathbb{T}s \varphi(p,m)$ for all $m \in p^\mathitathbb{T}$ is the least fixpoint $F_\textsc{var}phi$. 

 \end{proof}

\noindent Proposition~\ref{prop:cor_constructivity} naturally suggests the following translation $\mathitgFOETr{-}:\ensuremath{\mathitu\lque}\xspace(\mathitathsf{P})\to\ensuremath{\mathitathrm{WMSO}}\xspace(\mathitathsf{P})$,

\betagin{itemize}
	\itemsep 0 pt
	\item $\mathitgFOETr{p(x)}=p(x)$,
	\item $\mathitgFOETr{R(x,y)}=R(x,y)$
	\item $\mathitgFOETr{x\ensuremath{\mathitathrm{FO}}\xspaceeq y}= (x \ensuremath{\mathitathrm{FO}}\xspaceeq y)$
	\item $\mathitgFOETr{\textsc{var}phi \mathitathcal{L_\mathitu}lend \psi}=\mathitgFOETr{\textsc{var}phi} \mathitathcal{L_\mathitu}lend \mathitgFOETr{\psi}$,

	\item $\mathitgFOETr{\lnot \textsc{var}phi}= \lnot \mathitgFOETr{\textsc{var}phi}$,
	\item $\mathitgFOETr{\exists x. \textsc{var}phi}= \exists x. \mathitgFOETr{\textsc{var}phi}$,
	\item $\mathitgFOETr{au x. \textsc{var}phi}= \ensuremath{\mathitathrm{FO}}\xspacerall p.\exists x. (\lnot p(x) \mathitathcal{L_\mathitu}lend \mathitgFOETr{\textsc{var}phi})$,
	\item $\mathitgFOETr{\mathitu p. \textsc{var}phi(p,x)}= \exists p ( p(x) \mathitathcal{L_\mathitu}lend \ensuremath{\mathitathrm{FO}}\xspacerall y ( p(y) \to \mathitgFOETr{\textsc{var}phi(p,y) }))$.
\end{itemize}

The following theorem 
is then an immediate corollary of Proposition~\ref{prop:cor_constructivity}.

\betagin{theorem}\mathitathcal{L_\mathitu}lebel{thm:guard_wmso}
For every alternation-free formula $\varphi$ in the $\ensuremath{\mathitu_{c}\lque}\xspace$, every LTS $\mathitathbb{T}$, and assignment $g$, we have $\mathitathbb{T}, g \mathitathbb{T}s \textsc{var}phi$ iff $\mathitathbb{T}, g \mathitathbb{T}s \mathitgFOETr{\textsc{var}phi}$.

\end{theorem}
\betagin{proof}
The proof goes by induction on the complexity of $\textsc{var}phi$, the only critical step being the least fixpoint operator one. But this follows by applying Proposition \ref{prop:cor_constructivity} and the induction hypothesis.

\end{proof}

\subsection{Translating automata into formulas}
We are now ready to prove the second main result of the paper.

\betagin{theorem}\mathitathcal{L_\mathitu}lebel{thm:wmso_autofor}
There is an effective procedure that given an automaton in $\mathitathit{Aut}_{cw}({\ensuremath{\lque_1}\xspace})$, returns an equivalent WMSO-formula.
\end{theorem}
\betagin{proofsketch}
The argument   is
 essentially a refinement of the standard proof showing that any automaton in $\mathitathit{Aut}(\ensuremath{Fo_1}\xspace)$ can be translated into an equivalent $\mathitu$-formula
$\xi_\ensuremath\mathitathbb{A}\xspace$ (cf. e.g. \cite{Ven08}).
The idea is the following. We see a $\ensuremath{\mathitathrm{WMSO}}$-automaton as a system of equations expressed in terms of $\ensuremath{Fo^\infty}\xspacee$-formulas: each state corresponds to a monadic predicate variable and the parity of a state corresponds to the least and greatest fixpoint that we seek for the associated variable, etc. One then solves this system of equations via the same inductive procedure used to obtain the formula of the modal $\mathitu$-calculus from the system associated with a  $\mathitathit{Aut}(\ensuremath{Fo_1}\xspace)$-automaton (see e.g. \cite{ArnoldN01} for a description of the solution procedure). Because of the (weakness) and (continuity) conditions on the starting $\ensuremath{\mathitathrm{WMSO}}\xspace$-automaton $\ensuremath\mathitathbb{A}\xspace$, it is thence possible to verify that the resulting fixpoint formula $\xi_\ensuremath\mathitathbb{A}\xspace$ belongs to $\ensuremath{\mathitu_{c}\lque}\xspace$.
\end{proofsketch}

\betagin{remark}
As a corollary of the automata characterization on trees of \ensuremath{\mathitathrm{WMSO}}\xspace, we obtain the equivalence on this class of structures between \ensuremath{\mathitathrm{WMSO}}\xspace and $\ensuremath{\mathitu_{c}\lque}\xspace$. This consequence should be compared to the analogous result obtained by Walukiewicz in~\cite{Walukiewicz96} for FPL (fixpoint extension of $\ensuremath{\mathitathrm{FO}}\xspacee$) and MSO on trees.
\end{remark}

\section{Modal Characterization of WMSO}\mathitathcal{L_\mathitu}lebel{sec:char}

In this section we are going to prove Theorem \ref{t:m1}.
Our proof of the first item of the theorem crucially involves automata.
In the previous section we saw that on trees, $\ensuremath{\mathitathrm{WMSO}}$ effectively corresponds
to the automata class $\mathitathit{Aut}_{cw}(\ensuremath{\lque_1}\xspace)$.
 We will now relate this class to the one of
parity automata based on $\ensuremath{Fo_1}\xspace$ and satisfying similar weakness and continuity conditions.

\betagin{definition}
A \emph{$\ensuremath{\mathitu_{c}\ML}\xspace$-automaton} $\ensuremath\mathitathbb{A}\xspace = \tup{A,\Deltalta,\Omegaega,a_I}$ is an automaton $\ensuremath\mathitathbb{A}\xspace \in \mathitathit{Aut}(\ensuremath{Fo_1}\xspace)$ such that for all states $a,b \in A$ with $a \preceq b$ and $b\preceq a$ the following conditions hold:
\betagin{description}
	\itemsep 0 pt
	\item[(weakness)] $\Omega(a)=\Omega(b)$,
	\item[(continuity)] if $\Omega(a)$ is odd (resp. even) then, for each $c\in C$ we have
	   $\Delta(a,c) \in \cont{\ensuremath{Fo_1}\xspace^+}{b}(A)$ (resp. $\Delta(a,c) \in \cocont{\ensuremath{Fo_1}\xspace^+}{b}(A)$).
\end{description}
As the class of such automata coincides with $\mathitathit{Aut}_{cw}(\ensuremath{Fo_1}\xspace)$ we use the same name to denote it.
\end{definition}

As the key technical result of our paper, in subsection~\ref{pinvariant-fragment}
we will provide a construction $(-)^{\bullet}: \mathitathit{Aut}_{cw}(\ensuremath{\lque_1}\xspace) \to 
\mathitathit{Aut}_{cw}(\ensuremath{Fo_1}\xspace)$, such that for all $\mathitathstr{A}$ and $\mathitathstr{T}$ we have
\betagin{equation}
\mathitathcal{L_\mathitu}lebel{eq:crux}
\mathitathstr{A}^{\bullet} \text{ accepts } \mathitathstr{T} \text{ iff } \mathitathstr{A} \text{ accepts 
} \mathitathstr{T}^{\omega},
\end{equation}
where $\mathitathstr{T}^{\omega}$ is the $\omega$-unravelling of $\mathitathstr{T}$.
As we shall see, the map $(-)^{\bullet}$ is completely determined at the 
one-step level, that is, by some model-theoretic connection between 
$\ensuremath{\lque_1}\xspace$ and $\ensuremath{Fo_1}\xspace$.

The second fact, to be discussed in
subsection \ref{aut-to-formula}, is that for each $\ensuremath{\mathitu_{c}\ML}\xspace$-automaton $\mathitathstr{A}$  we can effectively construct an equivalent $\ensuremath{\mathitu_{c}\ML}\xspace$-formula $\xi_{\mathitathstr{A}}$.

On the basis of the above observations we show that those results are enough to prove Theorem~\ref{t:m1}(i) as follows:

\betagin{proofof}{Theorem~\ref{t:m1}}
\textbf{(1)} Given a \ensuremath{\mathitathrm{WMSO}}\xspace-formula $\varphi$, let $\varphi^{\bullet} \approxdef
\xi_{\ensuremath\mathitathbb{A}\xspace_{\varphi}^{\bullet}}$.
We verify that $\varphi$ is bisimulation invariant iff $\varphi$ and $\varphi^{\bullet}$
are equivalent.
The direction from right to left is immediate by the observation that
$\varphi^{\bullet}$ is a formula in $\ensuremath{\mathitu\ML}\xspace$.
The opposite direction follows from the following chain of equivalences:
\betagin{align*}
\mathitathbb{T} \mathitathbb{T}s \varphi
  & \text{ iff } \mathitathstr{T}^{\omega} \mathitathbb{T}s \varphi
  & \tag{$\varphi$ bisimulation invariant}
\\ & \text{ iff }  \mathitathstr{A}_{\varphi} \text{ accepts } \mathitathstr{T}^{\omega}
  & \tag{$ \varphi \equiv \ensuremath\mathitathbb{A}\xspace_{\varphi}$ on trees}
\\ & \text{ iff } \mathitathstr{A}_{\varphi}^{\bullet} \text{ accepts } \mathitathstr{T}
& \tag{\ref{eq:crux}}
\\ & \text{ iff }  \mathitathstr{T} \mathitathbb{T}s \xi_{ \ensuremath\mathitathbb{A}\xspace_{\varphi}^{\bullet}}
& \tag{$\ensuremath\mathitathbb{A}\xspace_{\varphi}^{\bullet}\equiv \xi_{ \ensuremath\mathitathbb{A}\xspace_{\varphi}^{\bullet}}$}
\end{align*}
\textbf{(2)} For the second part of Theorem \ref{t:m1},
We 

first define, for every first-order variable $x$, a translation $ST_x$ from
the $\mathitu$-calculus into the set of $\ensuremath{\mathitu\lque}\xspace$-formulas with only $x$ free:

\betagin{itemize}
\itemsep 0 pt
\item $ST_x(p)=p(x)$
\item $ST_x(\textsc{var}phi \mathitathcal{L_\mathitu}lend \psi)=ST_x(\textsc{var}phi) \mathitathcal{L_\mathitu}lend ST_x(\psi)$,
\item $ST_x(\textsc{var}phi \lor \psi)=ST_x(\textsc{var}phi) \lor ST_x(\psi)$,
\item $ST_x(\lnot \textsc{var}phi)= \lnot ST_x(\textsc{var}phi)$,
\item $ST_x(\Diamond \textsc{var}phi)=\exists y (R(x,y) \mathitathcal{L_\mathitu}lend ST_y(\textsc{var}phi)$),
\item $ST_x(\mathitu p. \textsc{var}phi)= \mathitu p. ST_x(\textsc{var}phi)$,
\end{itemize}
Clearly, every formula of the $\ensuremath{\mathitu_{c}\ML}\xspace$-fragment of the $\mathitu$-calclus is mapped to a logically equivalent formula of the $\ensuremath{\mathitu_{c}\ML}\xspace$-fragment of $\ensuremath{\mathitu\lque}\xspace$. Let
 $(-)_{\bullet}:\ensuremath{\mathitu_{c}\ML}\xspace\to\ensuremath{\mathitathrm{WMSO}}\xspace$ defined as the composite $\mathitgFOETr{-} \circ ST_x$. By Theorem \ref{thm:guard_wmso}
we obtain that $\psi \equiv \psi_{\bullet}$, for all $\psi \in
\ensuremath{\mathitu_{c}\ML}\xspace$.
\end{proofof}

\subsection{One-step translations}\mathitathcal{L_\mathitu}lebel{pinvariant-fragment}

In this subsection we will define a construction that transforms an arbitrary automaton
$\mathitathstr{A}$ in $\mathitathit{Aut}_{cw}(\ensuremath{\lque_1}\xspace)$ into an automaton $\mathitathstr{A}^{\bullet}$ in 
$\mathitathit{Aut}_{cw}(\ensuremath{Fo_1}\xspace)$, such that $\mathitathstr{A}$ and $\mathitathstr{A}^{\bullet}$ are related as 
in~\eqref{eq:crux}.
This construction is completely determined by the following translation at the
one-step level.

\betagin{definition}
Using the fact
that by Corollary~\ref{cor:olquepositivenf}, any formula in ${\ensuremath{\lque_1}\xspace}^+(A)$ is 
equivalent to a disjunction of formulas of the form 
$\posdbnfolque{\vlist{T}}{\Pi}{\Sigmagma}$, we define the translation 
$(-)^{\bullet} : {\ensuremath{\lque_1}\xspace}^+(A) \to \ensuremath{Fo_1}\xspace^+(A)$ as follows.
We set
\[
\Big( \posdbnfolque{\vlist{T}}{\Pi}{\Sigmagma} \Big)^{\bullet} \approxdef
b_{I}gwedge_{i} \exists x_i. \tau^+_{T_i}(x_i) \mathitathcal{L_\mathitu}lend \ensuremath{\mathitathrm{FO}}\xspacerall x. b_{I}gvee_{S\in\Sigmagma} \tau^+_S(x)

\]
and for $\alpha = b_{I}gvee_{i} \alpha_{i}$ we define $\alpha^{\bullet} \approxdef b_{I}gvee 
\alpha_{i}^{\bullet}$.
\end{definition}

The key property of this translation is the following.

\betagin{proposition}
\mathitathcal{L_\mathitu}lebel{p-1P}
For every one-step model $(D,V)$ and every $\alpha \in {\ensuremath{\lque_1}\xspace}^+(A)$ we have
\betagin{equation}
\mathitathcal{L_\mathitu}lebel{eq-1cr}
(D,V) \mathitathbb{T}s \alphapha^{\bullet} \text{ iff } (D\times \omega,V_\pi) \mathitathbb{T}s \alphapha,
\end{equation}
where $V_{\pi}$ 
 is the induced valuation given by 
$V_{\pi}(a) \approxdef \{ (d,k) \mathitid d \in V(a), k\in\omegaega\}$.
\end{proposition}

\betagin{proof}
Clearly it suffices to prove \eqref{eq-1cr} for formulas of the form
$\alpha = \posdbnfolque{\vlist{T}}{\Pi}{\Sigmagma}$.

\noindentFbox{$R_{I}ghtarrow$} 
Assume $(D,V) \mathitathbb{T}s \alphapha^{\bullet}$, we will show that 
$(D\times \omegaega,V_\pi) \mathitathbb{T}s \posdbnfolque{\vlist{T}}{\Pi}{\Sigmagma}$.
Let $d_i$ be such that $\tau_{T_i}^+(d_i)$ in $(D,V)$. 
It is clear that the $(d_i,i)$ provide \emph{distinct} elements satisfying 
$\tau_{T_i}^+((d_i,i))$ in $(D\times\omegaega,V_{\pi})$ and therefore the 
first-order existential part of $\alphapha$ is satisfied. 
With a similar but easier argument it is straightforward that the existential 
generalized quantifier part of $\alphapha$ is also satisfied.

For the universal parts of $\posdbnfolque{\vlist{T}}{\Pi}{\Sigmagma}$ it is enough to observe that, because of the universal part of $\alphapha^\bullet$, \emph{every} $d\in D$ realizes a positive type in $\Sigmagma$. By construction, the same applies to $(D\times\omegaega,V_{\pi})$, 
therefore this takes care of both universal quantifiers.
\mathitedskip
		
\noindentFbox{$\Leftarrow$} 
Assuming that $(D\times \omegaega,V_\pi) \mathitathbb{T}s 
\posdbnfolque{\vlist{T}}{\Pi}{\Sigmagma}$,
we will show that $(D,V) \mathitathbb{T}s \alphapha^\bullet$. 
The existential part of $\alphapha^{\bullet}$ is trivial. 
For the universal part we have to show that every element of $D$ realizes the 
positive part of a type in $\Sigmagma$. 
Suppose not, and let $d\in D$ be such that $\lnot\tau_S^+(d)$ for all $S\in 
\Sigmagma$. 
Then we have $(D\times\omegaega,V_\pi) \not\mathitathbb{T}s \tau_S^+((d,k))$ for all $k$.
That is, there are infinitely many elements not realizing the positive part of 
any type in $\Sigmagma$. 
Hence we have $(D\times\omegaega,V_\pi) \not\mathitathbb{T}s \ensuremath{Forall^\infty}\xspace y.b_{I}gvee_{S\in\Sigmagma} 
\tau_S^+(y)$. 
Absurd, because that is part of $\posdbnfolque{\vlist{T}}{\Pi}{\Sigmagma}$.
\end{proof}

As a consequence of Proposition~\ref{p-1P} we obtain the following.

\betagin{definition}
Given an automaton $\mathitathstr{A} = \tup{A,\Delta,\Omega,a_{I}}$ in $\mathitathit{Aut}(\ensuremath{\lque_1}\xspace)$, define 
the automaton $\mathitathstr{A}^{\bullet} \approxdef \tup{A,\Delta^{\bullet},\Omega,a_{I}}$ in 
$\mathitathit{Aut}(\ensuremath{Fo_1}\xspace)$ by putting, for each $(a,c) \in A \times C$:
\[
\Delta^{\bullet}(a,c) \approxdef (\Delta(a,c))^{\bullet}.
\]
\end{definition}

\betagin{proposition}
For any automaton $\mathitathstr{A} = \tup{A,\Delta,\Omega,a_{I}}$ in $\mathitathit{Aut}(\ensuremath{\lque_1}\xspace)$, and any
model $\mathitathstr{T}$, $\mathitathstr{A}$ and $\mathitathstr{T}$ satisfy \eqref{eq:crux}.
\end{proposition}

\betagin{proof}
The proof of this proposition is based on a fairly routine comparison of the 
acceptance games $\mathitathcal{A}(\mathitathstr{A}^{\bullet},\mathitathstr{T})$ and 
$\mathitathcal{A}(\mathitathstr{A},\mathitathstr{T}^{\omega})$.
In a slightly more general setting, the details of this proof can be found 
in~\cite{Venxx}.
\end{proof}
\mathitedskip

It remains to be checked that the construction $(-)^{\bullet}$, which has
been defined for arbitrary automata in $\mathitathit{Aut}(\ensuremath{\lque_1}\xspace)$, transforms 
$\ensuremath{\mathitathrm{WMSO}}$-automata into automata in the right class, viz., $\mathitathit{Aut}_{cw}(\ensuremath{Fo_1}\xspace)$.

\betagin{proposition}
Let $\mathitathstr{A} \in \mathitathit{Aut}(\ensuremath{\lque_1}\xspace)$.
If $\mathitathstr{A} \in \mathitathit{Aut}_{cw}(\ensuremath{\lque_1}\xspace)$, then $\mathitathstr{A}^{\bullet} \in \mathitathit{Aut}_{cw}(\ensuremath{Fo_1}\xspace)$.
\end{proposition}

\betagin{proof}
This proposition can be verified by a straightforward inspection, at the 
one-step level, that if a formula $\alpha \in {\ensuremath{\lque_1}\xspace}^+(A)$ belongs to the fragment 
$\cont{{\ensuremath{\lque_1}\xspace}^+}{a}(A)$, then its translation $\alpha^{\bullet}$ lands in 
the fragment $\cont{\ensuremath{Fo_1}\xspace^+}{a}(A)$.
\end{proof}

\betagin{remark}{\rm
As a corollary of the previous two propositions we find that 
\betagin{itemize}
	\itemsep 0 pt
	\item $\mathitathit{Aut}(\ensuremath{Fo_1}\xspace) \equiv \mathitathit{Aut}(\ensuremath{Fo_1}\xspace)/{b_{I}s}$, and
	\item $\mathitathit{Aut}_{cw}(\ensuremath{Fo_1}\xspace) \equiv \mathitathit{Aut}_{cw}(\ensuremath{Fo_1}\xspace)/{b_{I}s}$.
\end{itemize}
In fact, we are dealing here with an instantiation of a more general phenomenon 
that is essentially coalgebraic in nature.
In~\cite{Venxx} it is proved that if $\mathitathcal{L}o$ and $\mathitathcal{L}o'$ are two one-step
languages that are connected by a translation $(-)^{\bullet}: \mathitathcal{L}o' \to 
\mathitathcal{L}o$ satisfying a condition similar to \eqref{eq-1cr}, then we find that 
$\mathitathit{Aut}(\mathitathcal{L}o)$ corresponds to the bisimulation-invariant fragment of 
$\mathitathit{Aut}(\mathitathcal{L}o')$: $\mathitathit{Aut}(\mathitathcal{L}o) \equiv \mathitathit{Aut}(\mathitathcal{L}o')/{b_{I}s}$.
This subsection can be generalized to prove similar results relating
$\mathitathit{Aut}_{w}(\mathitathcal{L}o)$ to $\mathitathit{Aut}_{w}(\mathitathcal{L}o')$, and $\mathitathit{Aut}_{cw}(\mathitathcal{L}o)$ to 
$\mathitathit{Aut}_{cw}(\mathitathcal{L}o')$.
}\end{remark}

\subsection{From automata in $\mathitathit{Aut}_{cw}(\ensuremath{Fo_1}\xspace)$ to formulas in $\ensuremath{\mathitu_{c}\ML}\xspace$}\mathitathcal{L_\mathitu}lebel{aut-to-formula}

In this subsection we focus on the following theorem.

\betagin{theorem}\mathitathcal{L_\mathitu}lebel{t:autofor}
There is an effective procedure that, given an automaton $\mathitathstr{A}$ in
$\mathitathit{Aut}_{cw}(\ensuremath{Fo_1}\xspace)$, returns an equivalent formula $\xi_{\mathitathstr{A}}$ of the fragment 
$\ensuremath{\mathitu_{c}\ML}\xspace$ of the modal $\mathitu$-calculus.
\end{theorem}

\betagin{proof}
The argument  is a refinement of the standard proof showing that any automaton 
$\ensuremath\mathitathbb{A}\xspace$ from $\mathitathit{Aut}(\ensuremath{Fo_1}\xspace)$ can be translated into an equivalent $\mathitu$-formula 
$\xi_\ensuremath\mathitathbb{A}\xspace$ (cf. e.g. \cite{Ven08}), and it is essentially a special case of the argument proving Theorem \ref{thm:wmso_autofor}.

From now on, we always assume that a formula $\Delta(a,c)$ is in normal form. 
Following~\cite{Ven08}, we introduce another type of automata, called $(\mathitathsf{P},X)$-automata, which operate on $\p{(\mathitathsf{P} \cup X)}$-trees.
They differ from automata whose one-step language is defined over predicates in $(A \cup X)$ in that\ensuremath{\mathitathrm{FO}}\xspaceotnote{Parity automata based on $\ensuremath{Fo_1}\xspace$ are thus simply $(\mathitathsf{P},\emptyset)$-automata.}
\betagin{itemize}
\item Monadic predicate letters from $X$ can occur in the scope of a 
quantifier and only there, meaning that $(\mathitathsf{P},X)$-automata have transition $\Delta(a,c) \in \ensuremath{Fo_1}\xspace^+(A\cup X)$

\item The transition function is uniquely determined by the restriction of the coloring to $\mathitathsf{P}$, that is, for every $a \in A$, and $c_1, c_2 \in C$, if $c_1 \cap \mathitathsf{P} = c_2 \cap \mathitathsf{P}$ then $\Delta(a, c_1)= \Delta(a, c_2)$.
\end{itemize}
We also assume that
for every $x \in X$ there is a unique $a \in A$ and an unique $c \in C$ such that $x$ occurs in $\Delta(a,c)$.
The notion of acceptance is defined as expected, the only difference with being that during the acceptance game \'Eloise has to provide a valuation only for predicates in $A$ making formula given by the transition function true. 
It is then enough to prove the following claim.
\betagin{claimfirst}\mathitathcal{L_\mathitu}lebel{c:1}
There is an effective procedure that, given a $(\mathitathsf{P},X)$-automaton $\ensuremath\mathitathbb{A}\xspace$ gives an equivalent  formula $\xi_{\ensuremath\mathitathbb{A}\xspace} \in \ensuremath{\mathitu_{c}\ML}\xspace$ in which all occurrences of variables in $X$ are positive.
\end{claimfirst}
\betagin{pfclaim} 

Without loss of generality, we can assume that:
\betagin{itemize}
\itemsep 0 pt
\item Every (maximal) strongly connected component (SCC) in the graph of $\preceq$ has an unique entrance point,
\item The directed acyclic graph (DAG) of the SCCs of $\preceq$ is a tree, and more specifically,
\item 
$\{c \in A \mathitid a \leadsto c, c \prec a\}  \cap \{c \in A \mathitid b \leadsto c, c \prec b\}  = \emptyset$ whenever $a,b$ are in the same SCC, with $a\neq b$.
\end{itemize}

Given a $(\mathitathsf{P},X)$-automaton $\ensuremath\mathitathbb{A}\xspace$, we are now going to define a function $\deltalta_\ensuremath\mathitathbb{A}\xspace: A \to \ensuremath{\mathitathrm{ML}} (A \cup X \cup \mathitathsf{P})$

that assigns to each state $a$ of $\ensuremath\mathitathbb{A}\xspace$ a modal formula $\deltalta_\ensuremath\mathitathbb{A}\xspace(a)$ over  $A \cup X \cup \mathitathsf{P}$ representing all possible transitions from $a$ in the modal language with the property that if $b \in A$ is in the same $\preceq$-cycle of $a$ and $\Omega(a)=1$, then  $\deltalta_\ensuremath\mathitathbb{A}\xspace(a)$ is continuous in $b$. Dually for $\Omega(a)=0$.

Let $c \in C$, and assume $\Deltalta(a,c)$ is in positive basic form $b_{I}gvee \posdbnfofo{\Sigmagma}$. We define a first translation $TR_1$ taking as argument $\Deltalta(a,c)$ and giving as result a formula from the (guarded fragment of) first-order logic over $A \cup X \cup \mathitathsf{P}$ as follows. 
With every disjunct
$$
\posdbnfofo{\Sigmagma} = b_{I}gwedge_{S\in\Sigmagma} \exists x. \tau^+_{S}(x) \mathitathcal{L_\mathitu}lend \ensuremath{\mathitathrm{FO}}\xspacerall z.( b_{I}gvee_{S\in \Sigmagma} \tau^+_S(z)),
$$

we associate the formula

$$
TR_1(\posdbnfofo{\Sigmagma}) := b_{I}gwedge_{S\in\Sigmagma} \exists y. (R(x,y) \mathitathcal{L_\mathitu}lend \tau^+_{S}(y)) \mathitathcal{L_\mathitu}lend \ensuremath{\mathitathrm{FO}}\xspacerall z.( R(x,z) \to b_{I}gvee_{S\in \Sigmagma} \tau^+_S(z)).
$$
Fcwarning{Why do we need to go through this?}The formula $TR_1(\posdbnfofo{\Sigmagma})$ is bisimulation invariant, and it is equivalent to the modal formula

$$
TR_2(\posdbnfofo{\Sigmagma}) := b_{I}gwedge_{S\in\Sigmagma}  \Diamond(b_{I}gwedge S) \mathitathcal{L_\mathitu}lend \Box b_{I}gvee_{S\in \Sigmagma} (b_{I}gwedge S).
$$
Fcwarning{Maybe better to define this directly}
Let $TR_3(\Deltalta(a,c))= b_{I}gwedge (c \cap \mathitathsf{P}) \mathitathcal{L_\mathitu}lend b_{I}gwedge_{p \in \mathitathsf{P} \setminus c} \lnot p \mathitathcal{L_\mathitu}lend b_{I}gvee TR_2(\posdbnfofo{\Sigmagma})$.
 The modal formula $\deltalta_\ensuremath\mathitathbb{A}\xspace(a)$ is then defined as

 \[
 b_{I}gvee_{c \in C} TR_3(\Deltalta(a,c)).
 \]
By construction we have, for every $\mathitathbb{T}$,

    \betagin{eqnarray*}
    \mathitathbb{T}[x\mathitapsto s_I] \mathitathbb{T}s b_{I}gvee_{c \in C} b_{I}g (\tau_{(c \cap \mathitathsf{P})}(y) \mathitathcal{L_\mathitu}lend b_{I}gvee TR_1(\posdbnfofo{\Sigmagma})b_{I}g) & \text{iff} &\mathitathbb{T} \tscolorsdash \deltalta_\ensuremath\mathitathbb{A}\xspace(a).
    \end{eqnarray*}

A modal automaton over $\mathitathsf{P}$ is an automaton $ \tup{A, \deltalta, \Omega, a_I}$ such that $\deltalta : A \to \ensuremath{\mathitathrm{ML}}^+ (A)$, where $\ensuremath{\mathitathrm{ML}}^+ (A)$ is the set of all modal formulas over propositions $A \cup \mathitathsf{P}$ such that elements from $A$ appear only positively.
The acceptance game associated with such an automaton and a tree $\mathitathbb{T}$ is determined by the (symmetric) acceptance game defined according to the rules of Table~\ref{symmetric_modal_game}.
This means that we can equivalently see the automaton $\ensuremath\mathitathbb{A}\xspace$ as a modal automaton $\tup{A, \deltalta_\ensuremath\mathitathbb{A}\xspace, \Omega, a_I}$ whose transition function satisfies the weakness and continuity conditions. Thus, from now on we see $\ensuremath\mathitathbb{A}\xspace$ as the equivalent modal automaton we have just described.

\betagin{table}[h]
  \centering
\betagin{tabular}{|l|c|l|c|}
 \hline

  Position & Player & Admissible moves & Parity\\
   \hline
  $(a,s) \in A \times S$ & $\exists$ & $\{(\deltalta_\ensuremath\mathitathbb{A}\xspace(a),s)\}$ & $\Omega(a)$\\
  $(\psi_1 \vee \psi_2,s)$ & $\exists$ & $\{(\psi_1,s),(\psi_2,s) \}$ & $-$ \\
  $(\psi_1 \wedge \psi_2,s)$ & $\ensuremath{\mathitathrm{FO}}\xspacerall$ & $\{(\psi_1,s),(\psi_2,s) \}$ & $-$ \\
  $(\Diamond\textsc{var}phi,s)$ & $\exists$ & $\{(\textsc{var}phi,t)\ |\ t \in R[s] \}$ & $-$ \\
  $(\Box\textsc{var}phi,s)$ & $\ensuremath{\mathitathrm{FO}}\xspacerall$ & $\{(\textsc{var}phi,t)\ |\ t \in R[s] \}$ & $-$ \\

  $(\lnot p,s) \in \mathitathsf{P} \times S$ and $p \notin \sigma(s)$ & $\ensuremath{\mathitathrm{FO}}\xspacerall$ & $\emptyset$ & $-$\\
  $(\lnot p,s) \in \mathitathsf{P} \times S$ and $p \in \sigma(s)$ & $\exists$ & $\emptyset$ & $-$\\
  $(p,s) \in \mathitathsf{P} \times S$ and $p \in \sigma(s)$ & $\ensuremath{\mathitathrm{FO}}\xspacerall$ & $\emptyset$ & $-$\\
  $(p,s) \in \mathitathsf{P} \times S$ and $p \notin \sigma(s)$ & $\exists$ & $\emptyset$ & $-$\\

  \hline
\end{tabular}
 \caption{(Symmetric) acceptance game for modal automata}
 \mathitathcal{L_\mathitu}lebel{symmetric_modal_game}
\end{table}

For the construction of $\xi_\ensuremath\mathitathbb{A}\xspace$, we proceed by induction on the tree height of the DAG $t$ of SCC. If the height is 1, that is the DAG is a single point graph, we reason as follows.
 We have two cases to consider: either the SCC is trivial (i.e. it consists of a single non looping node), or not.
In the first case, $A=\{a_I\}$ and $\ensuremath\mathitathbb{A}\xspace$ is equivalent to $\xi_\ensuremath\mathitathbb{A}\xspace:=\deltalta_\ensuremath\mathitathbb{A}\xspace(a_I)$.

For the second case, let us assume that $\Omega(a_I)=1$, the case when it is $0$ being, mutatis mutandis, the same.
Let $A=\{a_0, \dots, a_\ell\}$, and $a_I=a_\ell$.
Since $\ensuremath\mathitathbb{A}\xspace$ is a weak modal automaton satisfying the continuity condition, given $a,b \in A$, if $b$ occurs in $\deltalta_\ensuremath\mathitathbb{A}\xspace(a)$, then $b$ is only in the scope of $\Diamond$ operator. 
We can now see the automaton $\mathitathstr{A}$
as a system of modal equations, and by applying the standard inductive procedure \emph{solves} this system of equations and
construct the least fixpoint formula $\xi_\ensuremath\mathitathbb{A}\xspace$ equivalent to $\ensuremath\mathitathbb{A}\xspace$, 

Here the key observation is that the weakness and continuity conditions on
strongly connected components of the automaton ensure that when we execute
a single step in solving the system of equations, we 
may work within the 
(syntactically) continuous fragment of the modal $\mathitu$-calculus.
From this, we can deduce that $\xi_\ensuremath\mathitathbb{A}\xspace \in \ensuremath{\mathitu_{c}\ML}\xspace$. Clearly the procedure preserves the polarity of each $x \in X$, meaning that all variables in $X$ are positive in $\xi_\ensuremath\mathitathbb{A}\xspace$.

For the induction step, assume the successors of the root of $t$ are $(n_1, \dots, n_\ell)$. For each $i \in \{1,\dots,\ell\}$, let $a_i$ be the entrance point of the SCC of $n_i$, and let $\ensuremath\mathitathbb{A}\xspace_{i}$ be the automaton $\ensuremath\mathitathbb{A}\xspace$ but having as an initial state $a_i$. If we do not consider the states that are not reachable by $a_i$, the DAG of the SCC of $\ensuremath\mathitathbb{A}\xspace_{i}$ is $t.{n_i}$ (the subtree of $t$ starting at $n_i$).
Let $Y=\{a_1, \dots, a_\ell\}$, and $M$ be the set of states of $\ensuremath\mathitathbb{A}\xspace$ that belong to the root of $t$. We assume $X \cap Y = \emptyset$. The structure
\[
\ensuremath\mathitathbb{A}\xspace_M := \tup{M, \deltalta_\ensuremath\mathitathbb{A}\xspace|_{M}, \Omega|_{M}, a_I}
\] is a $(\mathitathsf{P}, X \cup Y)$-automaton.

The inductive hypothesis applies to automata $\ensuremath\mathitathbb{A}\xspace_M, \ensuremath\mathitathbb{A}\xspace_{1}, \dots, \ensuremath\mathitathbb{A}\xspace_{\ell}$. Thus we obtain fixpoint formulas $\xi_M, \xi_1, \dots, \xi_\ell$, the former taking free variables in $\mathitathsf{P} \cup X \cup Y$, all the remaining in $\mathitathsf{P} \cup X$, equivalent to $\ensuremath\mathitathbb{A}\xspace_M, \ensuremath\mathitathbb{A}\xspace_1, \dots, \ensuremath\mathitathbb{A}\xspace_\ell$ respectively.
Notice that:
\betagin{itemize}
\item by induction hypothesis, $\xi_M, \xi_1, \dots, \xi_\ell \in \ensuremath{\mathitu_{c}\ML}\xspace$, every variable $x \in X \cup Y$ is positive in each of those formulas (if $x$ occurs in it),
\item by construction, if $x$ is free in $\xi_i$, then $x$ is not bounded in $\xi_{M}$.
\end{itemize}
 We can therefore deduce that
 $\xi_\ensuremath\mathitathbb{A}\xspace= \xi_{M}[a_1\mathitapsto\xi_{1}, \dots, a_\ell\mathitapsto\xi_{\ell}] \in \ensuremath{\mathitu_{c}\ML}\xspace$, and that each variable from $X$ occurs positively in $\xi_\ensuremath\mathitathbb{A}\xspace$.

 We verify that $\mathitathbb{T} \tscolorsdash \xi_{M}[a_1\mathitapsto\xi_{1}, \dots, a_\ell\mathitapsto\xi_{\ell}]$ iff $\mathitathbb{T} \in \ensuremath{\mathitathcal{T}}(\ensuremath\mathitathbb{A}\xspace)$, for every model $\mathitathbb{T}$.

But this follows by the following two facts:
\betagin{enumerate}
\item $\mathitathbb{T}\tscolorsdash \xi_{M}[a_1\mathitapsto\xi_{1}, \dots, a_\ell\mathitapsto\xi_{\ell}]$ iff $\mathitathbb{T}[a_1\mathitapsto \ext{\xi_1}^{\mathitathbb{T}}, \dots, a_\ell\mathitapsto \ext{\xi_\ell}^{\mathitathbb{T}}  ] \tscolorsdash \xi_M$,
\item $\mathitathbb{T} \in \ensuremath{\mathitathcal{T}}(\ensuremath\mathitathbb{A}\xspace)$  iff $\mathitathbb{T}[a_1\mathitapsto \ext{\ensuremath\mathitathbb{A}\xspace_1}^{\mathitathbb{T}}, \dots, a_\ell\mathitapsto \ext{\ensuremath\mathitathbb{A}\xspace_\ell}^{\mathitathbb{T}}  ] \in \ensuremath{\mathitathcal{T}}(\ensuremath\mathitathbb{A}\xspace_M)$
\end{enumerate}
where 
$\ext{\ensuremath\mathitathbb{A}\xspace_i}^{\mathitathbb{T}} := \{ s \in \mathitathbb{T} \mathitid \mathitathbb{T}.s \in \ensuremath{\mathitathcal{T}}(\ensuremath\mathitathbb{A}\xspace_i) \}$. 
\end{pfclaim}

This finishes the proof of Theorem. 
\end{proof}

In this section we verify that every  $\ensuremath{\mathitu_{c}\ML}\xspace$-formula is equivalent to a $\ensuremath{\mathitathrm{WMSO}}\xspace$-formula.

Firstly, let us define, for every first-order variable $x$, a translation $ST_x$ from $\ensuremath{\mathitu_{c}\ML}\xspace$-formulas into $\ensuremath{\mathitathrm{WMSO}}\xspace$-formulas with only $x$ free as follows:

\betagin{itemize}
\itemsep 0 pt
\item $ST_x(p)=p(x)$
\item $ST_x(\textsc{var}phi \mathitathcal{L_\mathitu}lend \psi)=ST_x(\textsc{var}phi) \mathitathcal{L_\mathitu}lend ST_x(\psi)$,
\item $ST_x(\textsc{var}phi \lor \psi)=ST_x(\textsc{var}phi) \lor ST_x(\psi)$,
\item $ST_x(\lnot \textsc{var}phi)= \lnot ST_x(\textsc{var}phi)$,
\item $ST_x(\Diamond \textsc{var}phi)=\exists y (R(x,y) \mathitathcal{L_\mathitu}lend ST_y(\textsc{var}phi)$),
\item $ST_x(\mathitu p. \textsc{var}phi)= \exists p ( p(x) \mathitathcal{L_\mathitu}lend \ensuremath{\mathitathrm{FO}}\xspacerall y ( p(y) \to ST_y(\textsc{var}phi) ))$.
\end{itemize}
Note that in $ST_x(\mathitu p. \textsc{var}phi)$, the predicate $p$ which occurs in $ST_y(\textsc{var}phi) $ is bounded by the outermost second order existential quantifier.

Let $(-)_\bullet$ be simply $ST_x$, for a given first-order variable $x$. Then, we prove the following theorem.

\betagin{theorem}\mathitathcal{L_\mathitu}lebel{thm:contransweak}
For every LTS $\mathitathbb{T} = \tup{T,R,\sigma,s_I}$, the following two conditions are equivalent:

\betagin{enumerate}
\itemsep 0pt
\item $\mathitathbb{T} \tscolorsdash \textsc{var}phi$,
\item $\mathitathbb{T}[x \mathitapsto s_I] \mathitathbb{T}s \textsc{var}phi_\bullet$.
\end{enumerate}

\end{theorem}
\betagin{proof}
The proof goes by induction on the complexity of $\textsc{var}phi$, the only critical step being the least fixpoint operator one.
Let therefore consider $\mathitu p. \textsc{var}phi$. Recall that we assume, without loss of generality, that bounded and free variables are distinct in $\mathitu p. \textsc{var}phi$.
We first show that $(1)$ implies $(2)$. Since $\mathitathbb{T} \tscolorsdash \textsc{var}phi$, \'Eloise has a winning strategy $f$ in $\mathitathcal{E}(\mathitu p.\textsc{var}phi,\mathitathbb{T})@(\mathitu p.\textsc{var}phi,s_I)$.
Define $p^\mathitathbb{T} \subseteq T$ to be the set of nodes $s \in T$ such that there is a (partial) match $\pi'$ satisfying

\betagin{enumerate}[(1)]
\itemsep 0pt
\item $\pi'$ is $f$-guided,
\item every position of $\pi'$ is of the form $(\gammamma,m)$, with $p$ occurring in $\gammamma$, and
\item the last position of $\pi'$ is of the form $(\mathitu p. \textsc{var}phi, s)$.
\end{enumerate}

The key observation is that since $f$ is a winning strategy, all $f$-guided matches are finite, and that because $p$ is existential in $\textsc{var}phi$, \existsse is the only player who picks successors in $\pi'$. As a consequence of K\"onig's Lemma, $p^\mathitathbb{T}$ is finite.

Using the induction hypothesis, it is easy to check that $\mathitathbb{T}[x \mathitapsto s_I] \mathitathbb{T}s \exists p ( p(x) \mathitathcal{L_\mathitu}lend \ensuremath{\mathitathrm{FO}}\xspacerall y ( p(y) \to ST_y(\textsc{var}phi) ))$ with $p \mathitapsto p^\mathitathbb{T}$ as a witness.

For the other direction, the idea is the following. Because $\mathitathbb{T}[x \mathitapsto s_I] \mathitathbb{T}s ST_x(\textsc{var}phi)$,
there is a finite set $p^\mathitathbb{T}$ such that $\mathitathbb{T}[x \mathitapsto s_I, p \mathitapsto p^\mathitathbb{T}] \mathitathbb{T}s p(x) \mathitathcal{L_\mathitu}lend \ensuremath{\mathitathrm{FO}}\xspacerall y ( p(y) \to ST_y(\textsc{var}phi) )$. The winning strategy for \'Eloise  in $\mathitathcal{E}(\mathitu p.\textsc{var}phi,\mathitathbb{T})@(\mathitu p.\textsc{var}phi,s_I)$ is thus defined as the composition of all winning strategies in $\mathitathcal{E}(\textsc{var}phi,\mathitathbb{T}[p \mathitapsto p^\mathitathbb{T}])@(\textsc{var}phi,s)$ for $s \in p^\mathitathbb{T}$.
\end{proof}

\noindent This concludes the proof of Theorem~\ref{t:m1}, and in particular of the fact that
$\ensuremath{\mathitu_{c}\ML}\xspace = \ensuremath{\mathitathrm{WMSO}}\xspace/{b_{I}s}$.

\newcommand{\mathit{CF}(q)}{\mathitathit{CF}(q)}
\newcommand{\ST}[1]{\mathitathit{ST}_{#1}}

\betagin{convention}
We assume familiarity with the syntax and (game) semantics of the modal 
$\mathitu$-calculus $\mathitu\ensuremath{\mathitathrm{ML}}$ and of weak monadic second-order logic (WMSO).

We will only interpret these languages on tree models $(\mathitathstr{T},r)$, with $r$
being the root of the tree; for convenience we assume that $r$ is part of
the signature of WMSO.

We let $\unlhd$ denote the subformula relation, and let $\Sfor{\alpha}$ denote
the set of subformulas of a formula $\alpha$.
The first-order standard translation (with free variable $x$) of a modal formula
$\psi$ is denoted as $\ST{x}(\psi)$.
\end{convention}

\betagin{definition}
Given a proposition letter $q$, we define the set $\mathit{CF}(q)$ by the following 
grammar:
\[
\alphapha \mathitathrel{::=} q \mathitathrel{|} \psi
   \mathitathrel{|} \alpha \mathitathcal{L_\mathitu}lend \alpha \mathitathrel{|} \alpha \lor \alpha \mathitathrel{|} \Diamond\alpha,
\]
where $\psi$ denotes an arbitrary modal formula in which $q$ does not 
occur.
\end{definition}

It follows from results by Fontaine \& Venema that a modal formula is 
continuous in $q$ iff it is equivalent to a formula in the fragment $\mathit{CF}(q)$.

\betagin{theorem}
For any $\alpha \in \mathit{CF}(q)$ that is guarded in $q$, the formula $\mathitu q. \alpha$ can
be expressed in WMSO.
\end{theorem}

From now on we fix a proposition letter $q$ and a formula $\alpha \in \mathit{CF}(q)$
that is guarded in $q$.
In addition, we assume that $q$ does occur in $\alpha$.

\betagin{definition}
Let $H$ denote the least subset of $\Sfor{\alpha}$

such that $\alpha \in H$,
and if $q$ occurs in $\beta \in H$, then all immediate subformulas of $\beta$
also belong to $H$.
\end{definition}

It is not hard to show that $H \subseteq \mathit{CF}(q)$.
More in particular, $H$ consists of those subformulas $\beta$ of $\alpha$ 
such that either $q$ occurs in $\betata$, or $\alpha$ has a subformula of the form 
$\beta\lor\beta'$ or $\beta\mathitathcal{L_\mathitu}lend\beta'$ such that $q$ occurs in $\beta'$ but not in 
$\beta$.

As a consequence of the definition, any full match $\pi$ of an evaluation 
game $\mathitathcal{E}(\alpha,\mathitathstr{S})$ has an initial part $\pi'$ in which only formulas in 
$H$ are under consideration, and which, unless $\pi' = \pi$ and $\exists$
gets stuck in a position of the form $(\Diamond\beta,s)$ with $\Diamond\beta \in H$, 
ends at a position either of the form $(q,s)$ (in which case the match is 
over), or of the form $(\beta,s)$ with $q$ not occurring in $\beta$.

Similarly a full match $\pi$ of an evaluation game $\mathitathcal{E}(\mathitu 
q.\alpha,\mathitathstr{S})@(\mathitu q.\alpha,r)$ will have one of the following shapes:
\betagin{enumerate}
\item 
$\pi$ is infinite and $\exists$ looses since this means that $q$ is unfolded
infinitely often;
\item
$\pi$ is finite and has an initial $H$-part $\pi'$ which satisfies 
one of the following:
    \betagin{enumerate}
    \item $\pi = \pi'$ and $\exists$ looses in getting stuck at a diamond formula;
    \item $\pi'$ ends in a position of the form $(\beta,s)$ with $q$ not 
    occurring in $\beta$; in this case $(\beta,s)$ is preceded by a position of the
    form $(\gamma,s)$ with $q \unlhd \gamma \in H$ and $\beta$ being either a conjunct 
    or a disjunct of $\gamma$.
    \end{enumerate}
\end{enumerate}

\betagin{definition}
Let $\varphi$ the WMSO-formula $\{ \exists Y_{\beta} \mathitid \beta \in H \}.\varphi'$,
where $\varphi'$ is the conjunction of the following formulas:
\betagin{description}
\item[$\mathitathbf{(\chi_{r})}$] $Y_{\alpha}(r)$
\item[$\mathitathbf{(\chi_{\lor})}$] 
   $b_{I}gwedge_{\beta\lor\gamma \in H}\ensuremath{\mathitathrm{FO}}\xspacerall x. (Y_{\beta\lor\gamma}x \to
      (Y_{\beta}x \lor Y_{\gamma}x))$
\item[$\mathitathbf{(\chi_{\mathitathcal{L_\mathitu}lend})}$] 
   $b_{I}gwedge_{\beta\mathitathcal{L_\mathitu}lend\gamma \in H}\ensuremath{\mathitathrm{FO}}\xspacerall x. (Y_{\beta\mathitathcal{L_\mathitu}lend\gamma}x \to 
      (Y_{\beta}x \mathitathcal{L_\mathitu}lend Y_{\gamma}x))$
\item[$\mathitathbf{(\chi_{\Diamond})}$] 
   $b_{I}gwedge_{\Diamond\beta \in H}\ensuremath{\mathitathrm{FO}}\xspacerall x. (Y_{\Diamond\beta}x \to 
      \exists y. (Rxy \mathitathcal{L_\mathitu}lend Y_{\beta}y))$
\item[$\mathitathbf{(\chi_{\mathitu})}$] 
   $\ensuremath{\mathitathrm{FO}}\xspacerall x. (Y_{q}x \to Y_{\alpha}x)$
\item[$\mathitathbf{(\chi_{\ensuremath{\mathitathrm{ML}}})}$] 
   $b_{I}gwedge_{q \not\unlhd \psi \in H}\ensuremath{\mathitathrm{FO}}\xspacerall x. (Y_{\psi}x \to 
      \ST{x}(\psi))$
\end{description}
\end{definition}

\betagin{proposition}
Let $\mathitathstr{T}$ be a tree with root $r$. 
Then
\[
\mathitathstr{T},r \tscolorsdash \mathitu q.\alpha \iff \mathitathstr{T}, r \mathitathbb{T}s \varphi.
\]
\end{proposition}

\betagin{proof}
Fbox{$R_{I}ghtarrow$} 
If $\mathitathstr{T},r \tscolorsdash \mathitu q.\alpha$ then $\exists$ has a winning strategy $f$ in the 
game $\mathitathcal{E}(\mathitu q.\alpha,\mathitathstr{T})@(\mathitu q.\alpha,r)$.
For $\beta\in H$, define $Y_{\beta}$ to be the set of states $t \in T$ such that 
there is a (partial) match $\pi'$ that (i) is consistent with $f$, and such 
that (ii) every position of $\pi'$ is of the form $(\gamma,t)$ with $\gamma\in H$,
and (iii) the last position of $\pi'$ is of the form $(\beta,t)$.

The two key observations are that since $f$ is a winning strategy, all 
$f$-consistent matches are finite, and that because of the shape of formulas
in $H$, the only player who picks successors during the initial $H$-part of
a match is $\exists$.
As a consequence of K\"onig's Lemma, each set $Y_{\beta}$ is finite.

This means that these sets can interpret the second-order variables 
of the WMSO-formula $\varphi$.
The details as to why the collection $\{ Y_{\beta} \mathitid \beta \in H \}$ 
satisfies the $\chi$-formulas, will be given later.

Fbox{$R_{I}ghtarrow$}
Assume that $\mathitathstr{T}, r \mathitathbb{T}s \varphi$.
By a slight abuse of notation we will let $\{ Y_{\beta} \mathitid \beta \in H \}$
denote a finite set of finite subsets of $T$ such that $\mathitathstr{T}[Y_{\beta} 
\mathitid \beta \in H],r \mathitathbb{T}s \varphi'$.

In order to show that $\mathitathstr{T},r \tscolorsdash \mathitu q.\alpha$, let $\exists$ use the 
following strategy in the game $\mathitathcal{E}(\mathitu q.\alpha,\mathitathstr{T})@(\mathitu q.\alpha,r)$:
\betagin{itemize}
\item
at a position of the form $(\beta,t)$ with $q \unlhd \beta$ and $t \in Y_{\beta}$,
distinguish cases:
   \betagin{itemize}
   \item if $\beta = \beta_{0} \lor \beta_{0}$, pick $i \in \{ 0,1 \}$ such 
   that $t \in Y_{\beta_{i}}$; such an $i$ exists because of 
   ($\chi_{\lor}$);
   \item if $\beta = \Diamond\gamma$, pick a $u \in T$ such that $Rtu$ and $u 
   \in Y_{\gamma}$; such a $u$ exists because of ($\chi_{\Diamond}$);
   \end{itemize}
\item
at a position of the form $(\psi,t)$ with $q \not\unlhd \psi$, if $\mathitathstr{T},t 
\tscolorsdash \psi$ then $\exists$ uses her canonical strategy;
\item
at all other positions, $\exists$ moves randomly.
\end{itemize}

\betagin{claim}
For all positions $(\beta,t)$ that are consistent with the above strategy,
either $q \unlhd \beta$ and $t \in Y_{\beta}$, or $q \not\unlhd \beta$ and 
$\mathitathstr{T},t \tscolorsdash \beta$.
\end{claim}

\betagin{pfclaim}
By a straightforward induction on the length of partial matches.
\end{pfclaim}

Consider an arbitrary full match $\pi$ that is consistent with this 
strategy.
It easily follows by the above claim that $\exists$ will not get stuck
(some details to be supplied).

Suppose for contradiction that $\pi$ is infinite, i.e., the variable $q$
is unfolded infinitely often during $\pi$.
Because $\mathitathstr{T}$ is a tree and $\alpha$ is guarded in $q$, this means that $\pi$ 
passes through infinitely many \emph{distinct} positions of the form 
$(q,t)$.
Then by the claim the set $Y_{q}$ must be infinite, which contradicts the
fact that $Y_{q}$ interprets a WMSO-variable.

It follows that $\pi$ is finite. 
Then by the earlier classification of matches, $\pi$ has an initial 
$H$-part $\pi'$ which ends 
in a position of the form $(\psi,s)$ with $q$ not occurring in $\psi$.
By the above claim, this means that $\mathitathstr{T},t \tscolorsdash \psi$, and so $\exists$'s
canonical strategy, which she uses in the remainder of the match, guarantees
that she wins the match.

In other words, we have provided $\exists$ with a winning strategy in the 
game $\mathitathcal{E}(\mathitu q.\alpha,\mathitathstr{T})@(\mathitu q.\alpha,r)$, as required.
\end{proof}

\section{Conclusions}

\paragraph{Overview.} In this work we have presented three main contributions.
First, we proved that the bisimulation-invariant fragment of \ensuremath{\mathitathrm{WMSO}}\xspace is the
fragment $\ensuremath{\mathitu_{c}\ML}\xspace$ of $\ensuremath{\mathitu\ML}\xspace$ 
where the application of the fixpoint operator $\mathitu p$ is restricted to
formulas that are continuous in $p$.
Our result sheds light on the relationship between $\mso$, \ensuremath{\mathitathrm{WMSO}}\xspace and $\ensuremath{\mathitu\ML}\xspace$.
In particular, it provides a positive answer to the question whether
$\ensuremath{\mathitathrm{WMSO}}\xspace / {b_{I}s} \leq \ensuremath{\mathitathrm{AFMC}}\xspace$ on trees of arbitrary branching degree, left open
in~\cite{DBLP:conf/lics/FacchiniVZ13}.
This may also be read as the statement that the formulas that separate
$\ensuremath{\mathitathrm{WMSO}}\xspace$ from $\mathitathrm{MSO}$ are not bisimulation invariant (and hence, irrelevant in
the sense mentioned in the introduction).

To achieve this result, we shaped $\ensuremath{\mathitathrm{WMSO}}\xspace$-automata, a special kind of parity automata satisfying additional \emph{continuity} and \emph{weakness} conditions, with transition map given by the monadic logic $\ensuremath{\lque_1}\xspace$. Our second main contribution was to show that they characterize \ensuremath{\mathitathrm{WMSO}}\xspace on tree models.

As our third main contribution we gave a detailed model-theoretic analysis of the monotone and continuous fragments of $\ensuremath{\lque_1}\xspace$. We provide strong normal forms and syntactic characterizations that, besides being of independent interest, are critical for the development of the aforementioned results.

\paragraph{Future work.}  
A first line of research is directly inspired by the methods employed in this work. $\ensuremath{\mathitathrm{WMSO}}$-automata and $\ensuremath{\mathitu_{c}\ML}\xspace$-automata are essentially obtained by imposing conditions on the appropriate one-step logic $\ensuremath{\mathitathcal{L}}\xspace_1$ and transition structure of automata belonging to $\mathitathit{Aut}(\ensuremath{\mathitathcal{L}}\xspace_1)$. 
Following this approach, one could take aim at the automata-theoretic counterpart of other fragments of the modal $\mathitu$-calculus, like PDL, CTL or CTL$^*$. 

Another direction of investigation is based on the observation that, from a
topological point of view, all $\ensuremath{\mathitathrm{WMSO}}$-definable properties are Borel.
Since we do not have examples of  Borel $\ensuremath{\mathitathrm{MSO}}$-definable properties that
are not $\ensuremath{\mathitathrm{WMSO}}$-definable, is tempting to conjecture that $\ensuremath{\mathitathrm{WMSO}}$ is the
Borel fragment of $\ensuremath{\mathitathrm{MSO}}$ and analogously for $\ensuremath{\mathitu_{c}\ML}\xspace$ and $\ensuremath{\mathitu\ML}\xspace$.

\paragraph{Acknowledgements.}
The second author is supported by the \emph{Expressiveness of Modal Fixpoint Logics} project realized within the 5/2012 Homing Plus programme of the Foundation for Polish Science, co-financed by the European Union from the Regional Development Fund within the Operational Programme Innovative Economy (``Grants for Innovation''). The fourth author is supported by the project ANR 12IS02001 PACE.

b_{I}bliographystyle{plain}
b_{I}bliography{main-wmso}

\end{document}