- 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.
- Mutual exclusion: safety
- Bounded overtaking: safety
- Starvation freedom: liveness
- Deadlock freedom: liveness