0
$\begingroup$

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

$\endgroup$
  • 2
    $\begingroup$ What have you tried? Where did you get stuck? $\endgroup$ – Shaull May 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 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 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 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 at 13:27
0
$\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?

| cite | improve this answer | |
$\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.