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.
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.Sign up to join this community