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

1.1k questions

1.3k answers

1.7k comments

556 users

0 votes

Would my solution work too?

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

1 Answer

+1 vote
No, it does not work. [a WU b] is not satisfied, since b never holds, but a does also not hold always. Also, [b SB !a] does not hold since b never holds (and it should even hold before !a).
by (170k points)
I am a bit confused, since [a WU b] & F!a is given, does it mean that it is enough if [a WU b] is satisfied in t=0? like the initial state s0?

since WU is given, it means in [a WU b], b may or may not be true but a has to be true right? so, at t=0, a is true, so it would make [a WU b] true or since it is not true in next state it will be false? How does that work?
[a WU b] is a path formula so we have to find a path where it holds at some position (like t=0) and where the other formula does not hold. Note that [a WU b] = b | a &X[a WU b], so that [a WU b] holds at t=0 if b holds there (which is not the case) or if a holds there (which is the case) AND [a WU b] holds at t=1 (which is not the case).

Related questions

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