1
$\begingroup$

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.

$\endgroup$
6
  • 2
    $\begingroup$ What have you tried? Where did you get stuck? $\endgroup$
    – Shaull
    May 20 '20 at 10:50
  • $\begingroup$ @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. $\endgroup$
    – Jim
    May 20 '20 at 11:16
  • $\begingroup$ Not sure what invariant you're talking about, but $\pi$ as you suggest indeed satisfies the formula. $\endgroup$
    – Shaull
    May 20 '20 at 11:40
  • $\begingroup$ @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}? $\endgroup$
    – Jim
    May 20 '20 at 12:37
  • $\begingroup$ The latter. It means that the current letter never satisfies both $p$ and $q$, i.e. it is not $\{p,q\}$. $\endgroup$
    – Shaull
    May 20 '20 at 13:27
1
$\begingroup$

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?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.