The relation between liveness and saftey properties is based on their
definitions as forall and foreach predicates. The foreach
predicate
foreach x : P(x) : Q(x)
is identical to the forsome predicate
not (forsome x : P(x) : not Q(x))
In the other direction, the forsome predicate
forsome x : P(x) : Q(x)
is identical to the foreach predicate
not (forall x : P(x) : not Q(x))
The slippery bit in these identities is the double negative.
This page last modified on 25 June 2003.