New answers tagged software-verification
2
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
