# Translation to CTL

Sept 2022

9b. E([a U b] ^ ¬ [c U d])

= E([a U b] ^ [¬c B d])

= E([a U b] ^ [¬d U ¬c ^ ¬d])

Can you please help me understand this formula conversion highlighted in bold?

It can help if you can help me find out the formula in the lecture slide too.

Pulling the negation inwards is explained on page 25 of chapter 7. From a logical point you can also reason that: Not having c until d means that !c must have happened at least once before d. If d never holds (violating the "strong until" definition) then of course the weak definition of "before" is sufficient to describe that behavior (and the other way round).

On the other side, you can also use page 29 of chapter 7 to first rewrite the "strong until" as a "strong before" and then applying the negation to that "strong before" which gives you:

¬ [c U d] = ¬ [d B (¬c ∧ ¬d)] = [¬d U (¬c ∧ ¬d)]

so the second conversion is also correct. You can also reason that conversion from the "before" directly:

Either !d holds infinitely (then both the "weak before" and "weak until" are true) or there is some point where !c holds before the first appearance of d, which thus must be a point where !c & !d holds (which also "solves" the weak until).

As page 28 and 29 show, every temporal operator (beside X) can be written as "strong until" while "strong until" itself can be rewritten as any of the other binary temporal operators, so there is effectively a conversion from every temporal operator to every other temporal operator (by going over "strong until") except the two unary ones (i.e. "G" and "F") which can of course not solely represent the binary operators (but can be represented by them). However not all combinations of those conversions are described explicitely in the script, so you may need to do this yourself (for example by going over the "strong until" as just explained).

by (3.4k points)