How to prove that a formula can not be expressed in LTL, but can be in Buchi automata? I am looking for a general technique which can help me to prove not just that Buchi automata is more expressive model than LTL, but that the specific formula can/can't be expressed in LTL.

For example, "$p$ occurs at least on even positions" can be described by the following Buchi automata: $({q_0, q_1}, \Sigma, \delta, q_0, \{q_0\})$ where $\delta(q_1, *) = q_0$ and $\delta(q_0, p) = q_1$. 

I've read that that automata can't be expressed in LTL, but I don't understand how to formally prove it.

Thanks.
First you need to know what you want to express and how you are going to express it. For instance, you can represent a property as a set of infinite traces. 

The properties definable by Buechi automata are the $\omega$-regular languages. The properties definable by LTL formulae are the star-free regular languages. The star-free languages are a strict subset of the $\omega$-regular languages.

Section 5.1 of Principles of Model Checking by Baier and Katoen is a good, elementary starting point. If you want general proof techniques there are a variety of ways to proceed. One general technique that appeals to me is to use games. The first player is trying to show two structures can be distinguished with an LTL formula. The second shows they are the same. Two structures are LTL equivalent if the second player has a winning strategy. So, if you take two structures which are not isomorphic but the second player has a winning strategy, then, there is no LTL formula to distinguish between the two.


  An Until Hierarchy and Other Applications of an Ehrenfeucht-Fraisse Game for Temporal Logic, K. Etessami and Th. Wilke.


There are algorithms for checking if a given $\omega$-regular language is star-free. Unfortunately these are usually couched inside the proofs of theorems.


  Logical definability on infinite traces, Werner Ebinger and Anca Muscholl


I'll dig around a bit more and try to find a more algorithmic presentation.