Lecture Notes for Concurrent Programming

12 June 2003 - Safety, Liveness, and Fairness


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.