Safety & Liveness

  • Safety: nothing bad will ever happen
  • Liveness: something good will happen eventually

For sequential programs (correctness of program):

  • Safety: partial correctness
  • Liveness: termination

Foe state-transition graphs:

  • Safety: properties whose violation always has a finite witness (i.e. if something bad happens on an infinite run, then it happens already on some finite prefix)
    • For any run \( R \), \( R \) satisfies \( P \) if and only if every prefix of \( R \) satisfies \( P \).
    • For any run \( R \), \( R \) does not satisfy \( P \) if and only if there exists a prefix of \( R \) that does not satisfy \( P \).
  • Liveness: properties whose violation never has a finite witness (i.e. no matter what happens along a finite run, something good could still happen later)
    • For any finite run \( R \), there exists \( R_1 \) such that \( R_1 \) is an extension of \( R \) and \( R_1 \) staisfies \( P \).

Safety are properties that can be checked on finite executions, while liveness are properties that cannot be checked on finite executions.

Examples:

  • Mutual exclusion: safety
  • Bounded overtaking: safety
  • Starvation freedom: liveness
  • Deadlock freedom: liveness