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

1k questions

1.2k answers

1.6k comments

498 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 ...