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

Here, in the path from s0 Fa is valid and a is valid only in s0. Also since the formula S1 is weak until, b does not necessarily have to be true. Hence, it will satisfy formula S1 also, right? 

Since a is not satisfied in s1, a and Gb both are false in s1, hence it does not hold for formula S2 right?

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

1 Answer

+1 vote
You are wrong with this: On the path s0->s1^omega, "a" holds at t=0, but not for any t>0, and therefore Fa also holds at t=0, but not for any t>0. Variable b does never hold on that path, so S1 becomes equivalent to GFa, which is false on that path. Therefore, S1 does not hold on the path (not for any position t). Note that the weak until demands that the formula (in this case Fa) holds for any t, but it does only hold at t=0 in the example.

S2 holds on the path at t=0 since [(G b) SU a] is equivalent to a|b&X[(G b) SU a] and since "a" holds at t=0, also S2 holds there. S2 does however not hold for any t>0 on the path.

It is however enough that S1 and S2 differ at time t=0 on the path.
by (170k points)

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
...