New answers tagged


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^\...

Top 50 recent answers are included