Path in a transition system ($s_0{s}_1{s}_2\cdots$)

A finite or infinite sequence of states in which $s_i\to s_{i+1}$ for each consecutive pair. In infinite-path linear temporal logic semantics, paths are infinite; an initial path must also start in the specified initial set. Repeated states are allowed, unlike conventions for a simple path in a graph.

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,\dots ,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.