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.
Finding a finite model
reference request;lo.logic;computability;finite model theory
The first part of your question is answered by Trakhtenbrot's Theorem.The second part is quite a large question indeed.  Depending on the relational structure you're working on, multiple solutions can be given.  For instance, if you're interested in formal languages, MSO over word structures corresponds to regular languages, and the matching logic (see this) corresponds to CFL, and thus have their satisfiability problem decidable.You should have a look at Chapter 14 of Libkin, where nice segments of FO are proven to have a decidable satisfiability problem, according to the amount of quantifier alternations allowed.