Lasso path
= Lasso path
An infinite <path in a transition system> represented by a finite prefix followed by infinite repetition of a nonempty finite loop. If stored positions are $q_0,\ldots,q_k$ and $q_k\to q_\ell$, the represented <sequence> is $q_0\cdots q_{\ell-1}(q_\ell\cdots q_k)^\omega$. The <linear temporal logic> condition $GFp$ holds exactly when $p$ occurs on the repeated part, and $FGp$ holds exactly when $p$ holds everywhere on that part.