# Buchi Automaton G(Xa->b)

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?

My suggestion

Best regards

• 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! – 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.