Lecture Notes for Concurrent Programming

12 June 2003 - Safety, Liveness, and Fairness

Analogous, hell, it is a forall predicate. The claim that P is a safety property is identical to claiming that

forall si : si is a state instance : P(si)

is true. Similarly, the claim that P is a liveness property is identical to claiming that

forsome si : si is a state instance : P(si)

is true.

This page last modified on 25 June 2003.