# LTL Model of (infinitely often p) ∧ ( infinitely often q) ∧ (¬ Eventually (p ∧ q))?

Can anyone give a model (pi) of the ltl formula above?

• What have you tried? Where did you get stuck? – Shaull May 20 '20 at 10:50
• @Shaull The invariant is confusing me but I think a formula such as π = {p}{q}{p}{q}{p}{q}.... but i'm really not sure. – Jim May 20 '20 at 11:16
• Not sure what invariant you're talking about, but $\pi$ as you suggest indeed satisfies the formula. – Shaull May 20 '20 at 11:40
• @Shaull i mean im confused with this part of the formula (¬ Eventually (p ∧ q)). Does it mean that p and q can never be together like {p}{q} or does it mean {p,q}? – Jim May 20 '20 at 12:37
• The latter. It means that the current letter never satisfies both $p$ and $q$, i.e. it is not $\{p,q\}$. – Shaull May 20 '20 at 13:27

Hint: Take $$p$$ to mean even number, $$q = \neg p$$ meaning odd number.
Can you come up with a model where you have infinitely often $$p$$ and infinitely often $$q$$ but never both at the same time?