Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

769 questions

886 answers

1.3k comments

424 users

0 votes

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!

in * TF "Emb. Sys. and Rob." by (440 points)
retagged by

1 Answer

+2 votes

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] 
by (117k points)
Imprint | Privacy Policy
...