# 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