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

Can anyone give a model of the following LTL formula? $$\Box\Diamond p \land \Box\Diamond q \land \lnot \Diamond (p \land q).$$ That is, we want each of $$p$$ and $$q$$ to hold infinitely often, but $$p \land q$$ should never hold.

• What have you tried? Where did you get stuck? 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. 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\}$. 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?