# Tag Info

I'm not sure where the particular liveness definition you wrote comes from, but the definition given in Defining Liveness (Schneider, Alpern, 1985) is as follows. A property $P$ is a liveness property if and only if: $$\forall \alpha \in S^* : (\exists \beta \in S^\omega : \alpha\beta \vDash P)$$ where $S^*$ is the set of all partial executions and \$S^\...