Path in a transition system
= Path in a transition system
{title2=$s_0s_1s_2\cdots$}
= Paths in a transition system
{synonym}
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>.