1. Mikołaj Bojańczyk
   Two-Way Alternating Automata and Finite Models. ICALP, 2002   PDF

2. 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 [2] 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 [1] at the beginning of this page:

• Mikołaj Bojańczyk
  The finite graph problem for two-way alternating automata. Theor. Comput. Sci., 2003   PDF

• Mikołaj Bojańczyk
  The Finite Graph Problem for Two-Way Alternating Automata. FoSSaCS, 2001   PDF