Strong until
= Strong until
{title2=$\alpha\mathbin{\mathrm U}\beta$}
In <linear temporal logic>, $\alpha\mathbin{\mathrm U}\beta$ holds at position $i$ exactly when some $j\geq i$ satisfies $\beta$ and every position $k$ with $i\leq k<j$ satisfies $\alpha$. The witness $j$ must exist. The case $j=i$ imposes no condition on $\alpha$.