The semantics of until operator in linear temporal logic

71 Views Asked by At

According to the definition of until operator from Wiki:

$w \models \varphi~\text{U}~\psi$ if there exists $i \geq 0$ such that $w^i \models \psi$ and for all $0 \leq k < i, w^k \models \varphi$.

If the first state $w^0$ is $\neg \varphi \wedge \psi$ or $\varphi \wedge \psi$, does we have $w \models \varphi~\text{U}~\psi$ ? It is the case $i = 0$ for above defintion, thus it should be true. But i am not sure, because $\varphi \wedge \psi$ seems to not be proper with the semantics of until operator.