Show that the following formula is a law of LTL, i. e. the formula is satisfied on all paths in all models

 G(p → X q) ∧ G(q → F p) ∧ p → G F p

I dont know how to go about that. Whats the standard procedure to go about checking the satisfiability of all paths in all models for a given LTL formulae?

  • 3
    $\begingroup$ First, please put parenthesis in your formula. It seems the last "implies" should be outside the parenthesis. Secondly, try to show that this formula holds for every path, regardless of the model. $\endgroup$ – Shaull Oct 14 '17 at 17:45
  • 2
    $\begingroup$ What have you tried? Where did you get stuck? We do not want to just hand you the solution; we want you to gain understanding. However, as it is we do not know what your underlying problem is, so we can not begin to help. See here for tips on asking questions about exercise problems. If you are uncertain how to improve your question, why not ask around in Computer Science Chat? $\endgroup$ – Raphael Oct 14 '17 at 17:46
  • $\begingroup$ Seems to be a modus ponens thing, roughly speaking. $\endgroup$ – Raphael Oct 14 '17 at 17:47
  • $\begingroup$ Hint: rather than thinking about all possible models & paths, think about the definitions of G, F, X. Your proof should assume the left hand side and use these definitions to prove the right hand side, thus proving the implication independently of the model & path.. $\endgroup$ – cardobard_box Oct 14 '17 at 17:55
  • $\begingroup$ @cardobard_box Can you give me an example or point me to some materials regarding this? $\endgroup$ – Zeist Oct 15 '17 at 10:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.