How can I prove that LTL formula is valid?

Question

I do not know with which technique i can prove if a LTL forumula is valid.

Let's say we have for example this one: ¬q U(¬p ∧ ¬q) → ¬Gp. How can prove if this valid or not? (should be true in any state of any model).

Answer 1

There are two main technique in order to prove validity (or more in general, to solve the problem of satisfiability over a definite model) for a LTL formula.

The first one is based on semantic tableau, analogous to the case of modal logic, here you can find some explanations.

The other one is based on automata, in particular it is possible to translate a formula in a Buchi automaton, and then one can check satisfiability paths on the automaton. In the case of the validity, you have to translate the negation of your formula and verify that the automaton you get is the empty one. This can be performed algorithmically, this is a useful tool (by the way, you formula is actually valid, try inserting this string: NOT(((NOT q)U(NOT p && NOT q))->NOT G(p))), at the same page you can find reference about the implementation of the translation algorithm.