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

915 questions

1k answers

1.4k comments

441 users

0 votes
1) In chapter 7 - Temporal Logics, slide 82 what is the meaning of positive and negative occurrence of weak until and strong until operator?

And on slide 84, why haven't we considered fairness constraint for Ga?
in * TF "Vis. and Sci. Comp." by (870 points)

1 Answer

0 votes
If we are just using negation, conjunction and disjunction, then a positive occurrence of a subformula is one that occurs behind an even number of negations while a negative occurrence is one that occurs behind an odd number of negations.

Ga on slide 84 has a positive occurrence, and as slide 82 explained, we can neglect fairness constraints for [phi WU psi] (means for all weak temporal operators since all of them can be reduced to WU, and since we have G(a) = [a WU false], it also applies to G).
by (142k points)
ok got it. Since, F(a) = -(-a WU false), thus we considered fairness constraint in slide 83. Thank you so much.
Right! Alternatively, you could say F(a) = [true SU a] which is then a positive occurrence of a strong until.
ok. Got it. thank you :D

Related questions

0 votes
1 answer
asked Feb 13, 2021 in * TF "Emb. Sys. and Rob." by dn (1.4k points)
0 votes
1 answer
asked Aug 14, 2020 in * TF "Vis. and Sci. Comp." by Anshu (870 points)
0 votes
1 answer
0 votes
1 answer
asked Aug 13, 2020 in * TF "Vis. and Sci. Comp." by Anshu (870 points)
Imprint | Privacy Policy
...