Question about the before operator

Question

Hello everyone,

While learning for VRS using the online tool, a question came up.
The following kripke structure is given:

And I was evaluating the formula: E [a SB b]

According to the tool the following state set satisfies this: {s0;s1;s4;s5;s6;s8}.

My Question is why s1, s4, s5 and s6 are part of this set, if I had asked for WB, it would make sense to me, but why is SB satisfied?

Thanks in advance!

Answer 1

Note that [a SB b] demands that a holds before b holds, and that a must eventually occur, but b may not occur. 

• s0 is there because the path s0->s8->... satisfies [a SB b].
• s1 is there because the path s1->s2->s2 satisfies [a SB b] 
• s4 is there because the path s4->s5->s6->... satisfies [a SB b] 
• s5 is there because the path s5->s6->... satisfies [a SB b] 
• s6 is there because the path s6->... satisfies [a SB b] 
• s8 is there because the path s8->... satisfies [a SB b]