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

915 questions

1k answers

1.4k comments

441 users

0 votes
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.
in * TF "Vis. and Sci. Comp." by (870 points)
edited by

1 Answer

+1 vote

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]
by (142k points)
edited by
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).

Related questions

0 votes
1 answer
asked Aug 12, 2020 in * TF "Vis. and Sci. Comp." by Anshu (870 points)
0 votes
1 answer
asked Aug 12, 2020 in * TF "Vis. and Sci. Comp." by Anshu (870 points)
0 votes
1 answer
asked Aug 11, 2020 in * TF "Vis. and Sci. Comp." by Anshu (870 points)
0 votes
1 answer
Imprint | Privacy Policy
...