I have a question regarding buchi automatons. The automata for the LTL formula, G(Xa->b) is as the attached picture. Why dosen't a have to be true in order to make the automaton correct?

enter image description here

My suggestion enter image description here

Best regards

  • $\begingroup$ The title you have chosen is not well suited to representing your question. Please take some time to improve it; we have collected some advice here. Thank you! $\endgroup$
    – Raphael
    Jul 19 '17 at 5:27

The formula states that for all $n$, if $a$ holds at time $n+1$ then $b$ holds at time $n$. If $a$ never holds then the formula is trivially true.

  • $\begingroup$ Thank you very much, @yuval-filmus. I still not quite sure that a get the formula. The 1, does that mean "every possible value"? $\endgroup$
    – Svendole
    Mar 20 '17 at 17:41
  • $\begingroup$ Here 1 is the formula that is always true. Similarly, 0 is the formula that is always false. $\endgroup$ Mar 20 '17 at 18:00
  • $\begingroup$ Yeah, so that would be the same as the buchi, i have drawn (see newly attached picture)? Thank you for your patience :-) @yuval-filmus $\endgroup$
    – Svendole
    Mar 20 '17 at 19:12
  • $\begingroup$ I'll let you figure that out on your own. $\endgroup$ Mar 20 '17 at 19:14

Your Answer

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

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