The finite graph problem for two-way alternating automata

Two-way alternating automata on infinite trees were introduced by Vardi (Reasoning about the part with two way automata, Lecture Notes in Computer Science, vol. 11, Springer, Berlin, 1998, pp. 628-641). Here we consider alternating two-way automata on graphs and show the decidability of the following problem: "does a given automaton with the Biichi condition accept any finite graph?" Using this result we demonstrate the decidability of the finite model problem for a certain fragment of the modal mu-calculus with backward modalities. (C) 2002 Elsevier Science B.V. All rights reserved.