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
$\begingroup$
$\endgroup$
-
$\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
$\begingroup$
$\endgroup$
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.
answered Mar 20 '17 at 17:27
-
$\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$ – Yuval Filmus 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$ – Yuval Filmus Mar 20 '17 at 19:14
