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

Hello,

I wanted to ask in the below solution, why s1 is not satisfied?. For WU even if phi alone is satisfied, the formula would satisfy and "a" is being satisfied at initial state itself.
 

Thanks!.

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

1 Answer

0 votes
in s0, a and thus also Fa are satisfied. From s1 on, we never see a again. Hence, Fa is not satisfied in s1. The weak until is satisfied if either the left side holds forever or at least to the point before the point when the right side is satisfied. Since b is nowhere satisfied, we'd have the left side forever but it is only satisfied in the first step. Thus, S1 isn't satisfied.
by (25.6k points)
Thank You. So, for SU, formula will be satisfied even if once also the right side becomes true but doesn't have to necessarily hold forever? But for WU, the left side has to hold forever irrespective of, if its 'a' or 'Fa' (in the above case) or till the point when the right side becomes true. Have I understood it correctly?.
Both for SU and WU, the formula is satisfied once the right side is (provided that the left side had been satisfied so far). The difference is that WU also additionally allows the right side to never be satisfied if the left side is always satisfied.


Edit (one year later): I've been asked what's the intuition about SB and WB.
Both are satisfied if the left hand side is satisfied at some point and the right hand side has so far not been satisfied up (and including) that step.
If neither side is ever satisfied, then WB is satisfied, SB is not.

Related questions

0 votes
1 answer
asked Aug 24, 2020 in * TF "Emb. Sys. and Rob." by nikita (300 points)
0 votes
1 answer
asked Aug 23, 2020 in * TF "Emb. Sys. and Rob." by ssripa (550 points)
0 votes
1 answer
asked Aug 20, 2020 in * TF "Emb. Sys. and Rob." by maherin (370 points)
0 votes
1 answer
0 votes
1 answer
asked Aug 9, 2021 in * TF "Intelligent Systems" by RS (770 points)
Imprint | Privacy Policy
...