I have been looking at the Until operator and the release operator and when introduced to the release operator it was suggested that it is equivalent to:

$\phi R \psi \equiv \neg(\neg\phi U \neg \psi)$

But when trying to get from the semantic definition of the Until operator to the semantic definition of the Release operator by negation I get stuck part way. Specifically, I get stuck trying to negate a $\forall j < i$ expression as I will show below.

So the semantic definition of Until:

$\pi \models \phi U \psi \iff \exists i \geq0, \pi[i] \models \psi \land \forall j\leq i-1, \pi[j]\models \phi$

Putting the negations in:

$\pi \models \neg(\neg\phi U \neg\psi) \iff \neg(\exists i \geq0, \pi[i] \models \neg\psi \land \forall j< i, \pi[j]\models \neg\phi)$

$\iff \forall i \geq 0, \neg(\pi[i]\models\neg\psi)\lor \neg(\forall j < i,\pi[j]\models\neg\phi)$

$\iff \forall i \geq 0, (\pi[i]\models\psi)\lor (\exists j < i,\pi[j]\models\phi)$

In words, I am ending up with globally $\psi$ or globally there always exists some predecessor that satisfies $\phi$. Which cannot be correct as $\pi[j]$ is not defined when $i=0$.

The semantic definition for the release operator that I was aiming for is:

$\pi \models \phi R\psi \iff (\exists i\geq 0, \pi[i]\models\phi \land \forall j\leq i, \pi[j]\models\psi)\lor (\forall k \geq 0, \pi[k] \models \psi)$

So I have part of the expression correct ($\forall k \geq 0, \pi[k] \models \psi \equiv \forall i \geq 0, (\pi[i]\models\psi)$), but I am really stumped about how to get the second part or where I went wrong.

Any help enlightening me is greatly appreciated!


  • $\begingroup$ Well the first issue is you made a typo in the semantics for $R$ as it doesn't mention $\phi$ at all. Also, it would seem to be notationally simpler and conceptually cleaner to write $\forall j < i$ rather than $\forall j \leq i - 1$. $\endgroup$ Mar 10, 2019 at 5:30
  • $\begingroup$ Thanks for pointing out the typo in the R semantics, I have fixed it and simplified the $j < i $ expressions. $\endgroup$
    – Jack
    Mar 10, 2019 at 7:05

2 Answers 2


First, note that you did not really get the "first part the the expression correct". The first formula is, roughly, of the form

$$ \forall i, (p(i) \lor q(i)) $$ while the second one is of the form $$ r \lor (\forall k, p(k)) $$ Note the different bracketing.

That being said, you have two definitions for the semantics of the release operator, and you want to prove them equivalent. So far, you tried to manipulate those formulae according to standard logical rules (a correct approach), but failed to do so. Indeed, as far as I can see, that approach can not succeed. The nice news is that you do not need to use that approach: in order to prove that definition $A$ and $B$ are equivalent, you can also write two distinct proofs, one for $A \implies B$ and one for $B \implies A$. In writing such proofs, you can leverage all the known results from mathematics, not just those allowing formula manipulation.

In your specific case, you will need to use the well-ordering property of natural numbers, stating that any non-empty set of naturals must have a least element. Let me sketch a part of the proof.

Assume your first definition, and let's prove the second one. We consider two cases.

  1. If $\pi[k] \models \psi$ for all $k$, then the second definition is trivially true.

  2. Otherwise, $\pi[k] \not\models \psi$ for some $k$. This means that the set of natural numbers $\{k|\pi[k] \not\models \psi\}$ is not empty, hence has a least element -- let $m$ be that element. This means that $m$ satisfies $\pi[m] \not\models \psi$, and that (minimality) $\forall n<m, \pi[n] \models \psi$. Now, using the hypothesis, we can obtain that $\exists j<m, \pi[j]\models\phi$. From this and minimality we obtain the thesis.

Note that you still need to prove the other direction.

  • $\begingroup$ Thanks, this is great. I needed to think about the problem differently. There is one point I am a bit confused about. How do we get $\exists j < m, \pi[j] \models \phi$? Are we just saying that m is some value $\geq 0$ and since the statement on the left of the disjunction is not true, then the one on the right must hold? Basically, why have we replaced the i in our hypothesis with our minimal element? $\endgroup$
    – Jack
    Mar 11, 2019 at 2:10
  • $\begingroup$ Also I was wondering if you could comment on the case in the hypothesis where we have: $\forall i \geq 0, \exists j < i, \pi[j] \models \phi$. We are stating that j must exist for all i. Yet when $i=0$ it cannot exist. Is this a case of vacuous truth? or is it just a total contradiction? $\endgroup$
    – Jack
    Mar 11, 2019 at 4:04
  • $\begingroup$ @Jack By hp we have $\forall i \geq 0, (\pi[i]\models\psi)\lor (\exists j < i,\pi[j]\models\phi)$, hence $(\pi[m]\models\psi)\lor (\exists j < m,\pi[j]\models\phi)$ but the first part is false (I have a typo above where I used $k$ instead of $m$, I'll fix that). So, yes, we chose $i$ to be our least element. $\endgroup$
    – chi
    Mar 11, 2019 at 10:45
  • $\begingroup$ @Jack No, that's not a vacuous truth. The full property is of the form $\forall i\geq 0, p(i) \lor (\exists j<i, \ldots)$. Assuming that and choosing $i=0$, we get that $p(0)$ must be true since $\exists j<0, \ldots$ is false. In your case, $\pi[0]\models \psi$ must hold. $\endgroup$
    – chi
    Mar 11, 2019 at 10:50

Not sure whether its correct but I think that the until operator for LTL requires at least one instance of the pre condition to hold so


should really be


since you can't have without πœ“ first having πœ™ so the reason you get the undefined behaviour at i = 0 is because your original definition is wrong. There is not an i = 0 where πœ‹[𝑖]βŠ¨πœ“


Your Answer

By clicking β€œPost Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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