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

654 questions

767 answers

1.1k comments

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