 Next-time operator

The linear temporal logic operator $X\alpha$, true at position $i$ of a path in a transition system exactly when $\alpha$ is true at position $i+1$. Thus $XX\alpha$ tests two positions ahead.