Safety and Liveness

Ask an engineer what their concurrent system must do and you will hear two very different kinds of wish. One kind sounds like a fear: "two threads must never be in the critical section at the same time"; "the array index must never run off the end"; "the plane must never report itself on the ground while airborne." The other kind sounds like a hope: "every request will eventually be answered"; "the download will eventually finish"; "no thread waits for the lock forever." Fears and hopes. Nothing-bad, and something-good.

This is not a loose metaphor — it is a precise and complete classification. Every property you could ever state about the infinite behaviours of a system is, in a sense we will make exact, a mixture of a safety property ("nothing bad ever happens") and a liveness property ("something good eventually happens"). Knowing which kind you are dealing with tells you how a counterexample can look, what a model checker must search for, and even what kind of proof you owe.

Behaviours as infinite traces

Fix the vocabulary first. A reactive system — a server, a lock, a controller — is not a function that runs and halts; it is a machine that goes on responding. So we model a run as an infinite trace: a sequence of states (or of observations) \sigma = s_0\, s_1\, s_2\, \ldots The system's behaviour is the set of all traces it can produce. A property is just a set of traces too — the ones we deem acceptable — and the system satisfies the property when every trace it can produce is in that set.

With that lens, "does the system violate the property?" becomes "does it have a trace outside the accepted set?" — and the whole safety/liveness distinction is a statement about what such an outside trace can look like. That is what the figure below dramatises: a safety violation is spotted at a finite moment, a liveness violation only in the limit.

Safety: nothing bad ever happens

Informally: some "bad thing" never occurs along the run.
Formally: a set of traces S is a safety property if every trace not in S has a finite bad prefix — a finite initial segment such that no infinite continuation of it lies in S.
Slogan: a safety property, once broken, stays broken.

The finite-prefix clause is the whole content. It says a safety violation is observable at a finite time: there is a specific step at which you can point and say "there — it is already too late." Mutual exclusion is the canonical example. The bad thing is "both processes in their critical section at once." If a run ever reaches such a state, the prefix up to that state is a witness — it does not matter what happens afterwards, the run has already failed. Likewise "the index never exceeds the array bound": the first out-of-range access is a finite witness.

Because the witness is finite, you refute a safety property with a finite counterexample — a concrete, replayable trace ending at the bad state. That is exactly the object a debugger hands you, and exactly what makes safety violations so satisfying to fix.

Liveness: something good eventually happens

Informally: some "good thing" eventually occurs — sooner or later, but with no deadline fixed in advance.
Formally: a set of traces L is a liveness property if every finite prefix — no matter how bad it looks — can still be extended to some infinite trace in L.
Slogan: it is never too late; only an infinite run can fail.

Contrast this with safety exactly. For a liveness property, no finite prefix is ever a witness of failure, because any prefix can still be completed successfully — the good thing could always happen on the very next step. It follows that the only way to violate liveness is to go on forever and never deliver: an infinite counterexample, typically a loop that cycles endlessly while starving the awaited event.

The great examples are all about "eventually": termination ("the program eventually halts"), no starvation ("a waiting thread is eventually scheduled"), eventual response ("every request is eventually acknowledged"), guaranteed progress. Each is refuted only by an execution that runs forever behaving badly — a non-terminating loop, a thread passed over again and again, a request left hanging for eternity.

The decomposition theorem

Safety and liveness are not just two handy buckets; together they are exhaustive. A beautiful result of Alpern and Schneider (1985) says that the two classes span everything.

For any property P (any set of infinite traces) there exist a safety property S and a liveness property L with P = S \cap L.
Topologically, over the space of infinite traces, safety properties are the closed sets and liveness properties are the dense sets; every set is the intersection of its closure (a safety property) with a dense set (a liveness property).

The practical payoff is a design discipline: when you write a specification, split it into its safety part and its liveness part and treat each with the right tool. The safety part you attack by hunting for a finite bad prefix (an invariant that must never be broken); the liveness part you attack by ruling out bad infinite loops (a well-founded measure, or fairness assumptions). A single everyday requirement usually contains both: "every request gets exactly one response" bundles a safety clause ("never more than one response" — finite witness if a second one appears) with a liveness clause ("at least one response, eventually" — infinite witness if none ever comes).

How you refute each kind — side by side

	Safety	Liveness
Slogan	nothing bad ever happens	something good eventually happens
Violated by	a finite bad prefix	an infinite run only
Counterexample	finite trace to a bad state	infinite trace / a bad cycle (lasso)
Once broken…	stays broken	can always still be fixed
Examples	mutual exclusion, no overflow, no deadlock-state	termination, no starvation, eventual response
Typical proof	an invariant that holds at every step	a well-founded rank that must decrease

Notice the crisp asymmetry in the counterexamples. A model checker refuting safety returns a finite path; refuting liveness it returns a lasso — a finite stem leading into a cycle that repeats forever, standing in for the infinite bad run. That difference in the shape of the counterexample is exactly what drives the two different search algorithms you will meet in model checking.

It feels like liveness — deadlock is a failure of progress, after all — but the standard formulation "the system is never in a deadlocked state" is squarely a safety property. A deadlocked state (every process blocked, waiting on another) is a bad state reached at a finite moment; the prefix that arrives there is a finite witness, and nothing afterwards matters. The genuinely live cousin is "no starvation" — "every waiting process is eventually served" — which really is liveness, refuted only by an infinite schedule that passes one process over forever. The lesson: the words "progress" and "stuck" don't decide the class; ask instead whether a finite prefix can already seal the verdict.

A tempting misreading is to treat a liveness property as if it carried a hidden deadline — "the reply comes within, say, 100 steps." It does not. Plain liveness promises the good thing happens at some finite time, but the bound can depend on the run and is not fixed in advance. This is precisely why liveness cannot be refuted by any finite prefix: for every deadline you might guess, a run can honestly exceed it and still satisfy the property by delivering later. If you truly need "within k steps", that is a bounded requirement — and a bounded "eventually" collapses back into a safety property (the bad thing is now "step k passed with no reply", a finite witness). Confusing unbounded eventuality with a bounded deadline is the classic error, and it silently turns a liveness question into a safety one.