Resource for LTL formulae? I would like to practice on some problems for using LTL formulae but besides the foundations and theory there are only every few examples. I know that having understood theory is not enough. Where can I go looking for interesting applications, examples including discussions about it. Is it possible to open a thread with examples here?

E.g. 

$(P\to \Diamond Q)$ is intriguing. One would think "On a path $\pi$ starting at state $s$ when P holds, eventually Q will hold." But of course given LTL formula does also hold for any other path which does not satisfy $P$ but $\Diamond Q$ (def. $\rightarrow$ or $\neg P \vee  Q$).

Now, this is not covered in theory in general. It is experience knowledge. I want to practice LTL formulae, where can I go looking for them?
I am not sure what you are referring to when you say "this is not covered in theory in general." The specific example that you give has been studied and is called antecedent failure. 


  Formally verifying a microprocessor using a simulation methodology., D. L. Beatty and R. L. Bryant, 1994
  
  One of the principal dangers of formal verification is what we have called antecedent failure. Formally, implications have an extensional meaning: they are also true if the antecedent condition is not true. Antecedent failure means that we can speak nonsense and not realise it.


The problem of detecting more general forms of such logical pitfalls is called vacuity detection. The introduction of the paper below has an excellent overview. You will also find examples of formulae.


  Enhanced Vacuity Detection in Linear Temporal Logic, Roy Armoni, Limor Fix, Alon Flaisher, Orna Grumberg, Nir Piterman, Andreas Tiemeyer, and Moshe Y. Vardi, 2003


There are lots of courses where people teach temporal logic and those notes and exercises have lots of examples. I would also suggest Manna and Pnueli's book for examples.