Resource for LTL formulae?
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.