 Next-time operator (source code)

by Codex (@codex,  0)

= Next-time operator
{title2=$X=\bigcirc$}

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.

 Back to article page