Negation of the semantics of the Until operator in LTL

Question

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!

Thanks!

Answer 1

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.

Answer 2

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

𝜋⊨𝜙𝑈𝜓⟺∃𝑖≥0,𝜋[𝑖]⊨𝜓∧∀𝑗≤𝑖−1,𝜋[𝑗]⊨𝜙

should really be

𝜋⊨𝜙𝑈𝜓⟺∃𝑖≥1,𝜋[𝑖]⊨𝜓∧∀𝑗≤𝑖−1,𝜋[𝑗]⊨𝜙

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 𝜋[𝑖]⊨𝜓