Exam Paper: 2018.02.14 Question 9a

Question

In the below question-

how is E([1 U a] ∧ [1 U b]) (line 3) being solved as E[1 U ((a ∧ [1 U b]) ∨ (b ∧ [1 U a]))] (line 4)?

Can we not leave it till E(Fa ∧ Fb) or EFa ∧ EFb?

Answer 1

The idea of the construction that Martin already pointed out can be applied to the formula E(Fa ∧ Fb) directly; there is no real need to switch to the Until formulas. The reason for the latter was that those formulas were mentioned in the slides while corresponding ones for F would have to be derived first and would be:

E(Fa ∧ Fb) = EF(a ∧ Fb) ∨ EF(b ∧ Fa) = EF(a ∧ EFb) ∨ EF(b ∧ EFa)

Answer 2

If I remember that correctly, that's from an example discussed in the lecture. But the argument is as follows:

The conjunction enforces that both a and b occur at arbitrary moments in the future. We just a case distinction. Either we have a first and b at some point later or vice versa. These two cases are then connected with a disjunction which makes it equal to the previous formula.