Two-Way Alternating Automata and Finite Models. ICALP, 2002 PDF
Vince Bárány, Mikołaj Bojańczyk
Finite satisfiability for guarded fixpoint logic. Inf. Process. Lett., 2012 PDF
The two-way modal μ-calculus is a logic which does not have the finite model property, i.e. some formulas are satisfiable but not satisfiable in any finite model. The same holds for guarded fixpoint logic, a logic introduced by Grädel and Walukiewicz. These two papers show that for both of these logics, one can decide if a given formula has a finite model. For the first paper, about the μ-calculus, the solution boils down to finding trees where certain patterns have bounded size. (Trying to understand this boundedness, I later introduced the logic MSO+U.) For the second paper, about guarded fixpoint logic, one needs to use the first paper plus results on cutting and pasting in models for guarded logics by Bárány, Gottlob and Otto.
The problem that is solved in paper  from the above list was supposed to be the topic of my Master’s thesis, under Igor Walukiewicz. I was unable to solve it, nor even the special case where the two-way μ-calculus is used instead of guarded fixpoint logic. I only managed to solve the special case of two-way μ-calculus which corresponded to two-way alternating automata with the Büchi condition. This special case is given in the following papers (conference and journal version), which are no longer of any use, as they are deprecated by  at the beginning of this page:
The finite graph problem for two-way alternating automata. Theor. Comput. Sci., 2003 PDF
The Finite Graph Problem for Two-Way Alternating Automata. FoSSaCS, 2001 PDF