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

Exam : 17.02.2021 : Q 8 d : 2021.02.17.vrs.solutions.pdf (uni-kl.de)

Q. How XX is removed in first step ?

I came up with below solution :

Could you please explain this ?

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

1 Answer

+1 vote
 
Best answer
Your solution is also correct. The LTL formula X X G F[a SU b] is equivalent to the LTL formula  G F b, so that the X-operators are not that meaningful here. You may also add further ones, since X ... X G F phi is equivalent to G F phi, since if phi holds infinitely often, it will do so also after some finite time. The other thing that you used and the example solution used as well is that F[a SU b] is equivalent to F b: If F[a SU b]  holds at some time t, then there is a point of time t+delta where b holds, and therefore also F b holds. Conversely, if F b holds, then there is a point of time t where b holds, and at that time also [a SU b] holds, since b implies [a SU b].

Still confused?
by (166k points)
selected by
Thank you for the detailed explanation.

The first part regarding X X G F[a SU b] is clear, just one question is it same for .. X F G phi as eventually globally phi holds, so at some point of time phi will hold infinitely ?

For second part F[a SU b] :
So it means that, as this is SU hence when b holds eventually, F [a SU b] holds, so in future time t if b holds then it is same as F b both results in same.
Because if b never holds then both F [a SU b] and Fb doesn't hold. So in short as you have said b implies [a SU b].
Yes, also (F G a) <=> (X F G a) is valid. And no comment to the second part, that is fine.
Thanks a lot :)
It is clear now.

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
asked Aug 30, 2022 in * TF "Emb. Sys. and Rob." by ss (160 points)
0 votes
1 answer
asked Aug 24, 2022 in * TF "Emb. Sys. and Rob." by CS_E (2.9k points)
Imprint | Privacy Policy
...