Temporal Logics

Question

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?

Answer 1

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

Comments

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