I am looking for a short and precise explanation of B and U temporal operator in natural language..?

Question

Hello,

I am still struggling to comprehend formulas having B, SB, U or SU temporal operators. I understand mathematical definition of them but cannot use my knowledge to understand a more complicated formula. Can someone kindly make a short explanation of them in natural language that we can always refer to?

Thanks in advance.

Answer 1

Strong until, weak until, strong before, and weak before are temporal quantifiers in Linear Temporal Logic (LTL), and Computation Tree Logic (CTL, CTL*). But what are the differences?

Suppose we are looking at a path and we are evaluating it at time step t0. When do the following hold?

• [ a SU b ] (strong until): b does holds finitely many steps after t0. In the steps from t0 to the last step when b does not hold yet, a has to hold. If b already holds in t0, that's fine as well. Then a doesn't have to hold.
• [ a WU b ] (weak until): b may hold after finitely many steps after t0. In the steps from t0 to the last time step when b does not hold yet, a has to hold. If b never holds, then a has to hold in every step forever. If b already holds in t0, that's fine as well. Then a doesn't have to hold.
• [ a SU b ] (strong before): a does need to hold after finitely many steps after t0. On the way from t0 to (and including) this point where a holds first, b may never occur.
• [ a WU b ] (weak before): a may hold after finitely many steps after t0. On the way from t0 to (and including) this point where a holds first, b may never occur. If a never holds, then b may never hold too.

So in all four cases:

1. we are looking for the first occurrence good event (before: a happens, until: b happens)
2. on the way to the first satisfaction of the good event, we may not have a bad event (before: b happens at the same time or earlier than a, until: ¬a happens earlier than b)
3. the difference is that weak version allow an infinite search for the good event (while the bad event never happens), and the strong version require the search for the good event to be finite.

Comments

OK, very good. Thanks for your comprehensive explanations Martin. Just could you please fix the typos in the text to avoid misunderstanding.

---

Can you help me finding the typos that are left?

---

I think in 3rd and 4th bullet points the temporal operators inside brackets needs to be fixed (should be SB and B). The rest looks quite consistent.

Answer 2

Actually I just wanted to add a comment but images are not possible in comments, so I add another answer instead: I just want to point out the following slide that should be helpful here: to relate it with Martin's answer: the good event that is awaited for is the psi, and the other one that depends on psi's occurrence is the phi_i: