omega automata

Question

For (a SU b) - for formula to be correct,

suppose 'b' becomes True first time at T5 (and forever) then 'a' can only be true till T4, it can neither be True at T5 nor any time after T5.

and the same holds for (a WU b) also.

But for (a SB b) and (a WB b) - 'a' can also hold when 'b' becomes True for the first time

Is my understanding correct?

Thank you in advance.

Answer 1

No, it is rather like this:

           b : 00000111
           a : 11111***
    [a SU b] : 11111111

           b : 00000111
           a : 10111***
    [a SU b] : 00111111

           b : 00000111
           a : 11110***
    [a SU b] : 00000111

Note where I have written * for a; the value of a does not matter there. For WU, it is the same in the above diagrams.

For [a SB b] and [a WB b], a must hold before b holds (not at the same time). 

           b : 00000
           a : 00001
    [a SB b] : 11111

           b : 10001
           a : 00111
    [a SB b] : 01110

You may also remember the following laws (weak or strong does not matter here):

    !a & !b -> ([a SB b] <-> X[a SB b])
     a & !b ->  [a SB b]
          b -> ![a SB b]

     a & !b -> ([a SU b] <-> X[a SU b])
    !a & !b -> ![a SU b]
          b ->  [a SU b]

Comments

Ok. I understand now. Thank you so much.

---

Is it correct for WU?

            b : 00000111
            a : 10111***
 [a SU b] : 00111111
[a WU b] : 10111111

In WB we consider out of two arguments none is true but in SB we don't consider it. Am I wrong? Sorry, I am getting confused again.

            b : 10001
            a : 00111
 [a SB b] : 01110
[a WB b] : ?????

           b : 00000
           a : 00001
[a SB b] : 11111
[a WB b] :?????

---

If b holds at some time, then weak and strong until are same. Your WU-example is wrong; at the first point of time, it is not the case that [a WU b] holds, since a becomes false at t=1 and b is not yet there and also not there at t=2.

Also for the cases with the before operator weak and strong don't matter there (but in general they do, of course).