 Path in a transition system

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.