This question is specifically about the paper "Guarded Fixed Point Logic" by Gradel and Walukiewicz. Among other things they prove the decidability of the satisfiability problem for Fixpoint Loosely Guarded Fragment of First-Order Logic.

They see tableaux as input trees for alternating two-way automata.

Their proof follows these steps:

1) For any given sentence $\psi$, one can algorithmically build an alternating two-way automaton $\mathcal{A}_\psi$ such that $\mathcal{A}_\psi$ accepts $T$ iff $T$ is a tableau for $\psi$.

2) For any given sentence $\psi$, one can algorithmically build an alternating two-way automaton $\mathcal{A}_\psi$ such that $\mathcal{A}_\psi$ accepts $T$ iff $T$ is a tableau that represents a model for $\psi$.

3) Their alternating two-way automata are closed under intersection and have decidable emptiness problem.

They don’t talk about accepting conditions for their alternating two-way automata. Rather, they directly define acceptance in terms of games and winning strategies. I would like to:

1) See the accepting conditions for their alternating two-way automata explicitly stated without talking about games.

2) Know why the number of constants that we need to build the tableaux is bound by $2\cdot$ (width of $\psi$). Does this mean that if the initial sentence is satisfiable, then it has a model of size $\leq 2\cdot$ (width of $\psi$)?

3) Know what could be dropped or modified if one in interested only in the Loosely Guarded Fragment of First-Order Logic WITHOUT FIXPOINTS.

Hope someone is interested too.