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

660 questions

773 answers

1.1k comments

383 users

Hi,

In the figure given below, Can you explain why does NOT c & [(Fb) SU (¬a ∧ Xa)] hold in s0 ? We are getting (!a & X a) in s1 so the strong until would hold in s1.

Look at the following trace:

s0 s1 s2 ... a : 0 0 1 ... b : 0 0 0 ... c : 1 0 0 ... !a & X a : 0 1 0 ... F b : 0 0 0 ... [F b SU !a & X a] : 0 1 0 ... [b SU !a & X a] : 0 1 0 ... F[b SU !a & X a] : 1 1 0 ...