Well, it is just looking at the semantics of the temporal operators.
If you have trouble with these kind of exercises, maybe the following hints help.
You can copy 0s and 1s from the givne input traces, and other already computed traces due to the following laws that tell us some cases when subformulas starting with temporal operators are 0 or 1 due to the current time conditions:
b -> Fb
!a -> !Ga
b -> [a SU b]
!a&!b -> ![a SU b]
a&!b -> [a SB b]
b -> ![a SB b]
Once that is done, you can fill out the gaps between 0s and 1s within such an incomplete trace. These are done by the following rules:
!b -> Fb = XFb
a -> Ga = XGa
a&!b -> [a SU b] = X[a SU b]
!a&!b -> [a SB b] = X[a SB b]
What may be still left are open intervals at the end. That is the part where weak and strong operators differ.
In the mentioned example, it would work as follows:
step 1:
a : 011 011 ...
b : 100 100 ...
c : 001 001 ...
q0 = [a SU b] : 1 1
q1 = [q0 SU c] : 1 1 ...
step 2: fill gaps:
a : 011 011 ...
b : 100 100 ...
c : 001 001 ...
q0 = [a SU b] : 111 1
q1 = [q0 SU c] : 111 1 ... For the rest, you should understand that the second part of the traces were meant to repeat forever, you you may simply unroll that once more. Then you will see the following:
a : 011 011 011 ...
b : 100 100 100 ...
c : 001 001 001 ...
q0 = [a SU b] : 111 111 1
q1 = [q0 SU c] : 111 111 1 ...
