# LTL Validity checking

Could you explain how you derived the formula here (Problem 7a. September 6, 2022 exams). The formula in the lecture slide seems different from this.

For G[a WU b], we may simply apply the standard translation to LTL (pages 83-83), but we may also skip the GF-constraints for positive occurrences of weak and negative occurrences of strong temporal operators (page 94). In our case, both operators are weak and have positive occurrences, so that no GF-constraints are generated.

```    G[a WU b]
= AE({p},true,p<->b|a&Xp,Gp)
= AE({p,q},true,(p<->b|a&Xp)&(q<->p&Xq),q)
= AE({p,q},q,(p<->b|a&Xp)&(q<->p&Xq),true)
```

What is different to the lecture slides? Maybe I don't get what you mean?

Remark: It has already been pointed out that we may already take AE({p},true,p<->b|a&Xp,Gp) as a two-state safety automaton as the result.

by (166k points)
My confusion is this part &(q<->p&Xq),q
What is wrong with it? As explained on slides 95-99, we apply the abbreviations step by step which generates a conjunction of transition equations and a conjunction of fairness constraints, right?
Got it. Thank you