I know that the question "does a first order formula $\phi$ have a model" is undecidable in general.
Could anyone give me a link or a book which give the answer for finite models. If I have a first order formula $\phi$, is it decidable whether $\phi$ has a finite model? I am pretty sure that the question is well known, but I do not even know where to begin the search for an answer. (For example, I would have expected it to be in Libkin's "Elements of finite model theory", but it seems that I can not find it.)
The second part of my question is: Are there known restrictions such that the problem is decidable?
For example, the problem may become decidable for first-order formula with only monadic predicates. Or when we have monadic predicate plus a successor relation. But I cannot imagine an algorithm to decide if there exists a (finite) model over those restrictions.