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

1.1k questions

1.2k answers

1.6k comments

529 users

0 votes

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?

in * TF "Emb. Sys. and Rob." by (1.1k points)

2 Answers

0 votes
 
Best answer

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)

by (166k points)
selected by
0 votes
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.
by (25.6k points)

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...