0
$\begingroup$

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).

$\endgroup$

1 Answer 1

1
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ wow thank you. This helps me a lot. Very usefull tool!! $\endgroup$
    – 40er
    Jun 8, 2022 at 17:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.