Liveness Property

A property of a program or distributed system asserting that “something good eventually happens” (Lamport 1977; Alpern & Schneider 1985). Unlike a Safety Property, a liveness property cannot be falsified by any finite prefix — one must observe (or reason about) infinite behaviours.

Examples: eventual delivery (“every sent message is eventually received”), progress (“every enabled thread eventually runs”), termination (“every well-formed input produces output”). Proving liveness typically requires a well-founded ordering or a fairness assumption.

Alpern–Schneider’s decomposition theorem: every trace property is the intersection of a safety property and a liveness property. This factoring structures verification: safety is proved by invariants, liveness by well-founded descent or fairness-conditioned reasoning.

Tags

#verification #distributed-systems #safety-liveness

Safety Property

A property of a program or distributed system asserting that “nothing bad ever happens” (Lamport 1977). Formally, a safety property is one whose violation can be witnessed by a finite execution prefix: once the bad state is entered, no future behaviour can undo it.

Examples: mutual exclusion, partial correctness, absence of null-pointer dereference, “contract balance never drops below escrowed amount.” Dual: Liveness Property (“something good eventually happens”), whose violation requires an infinite trace.

Safety is semantically rich: on arbitrary programs, non-trivial safety properties are undecidable (Rice’s Theorem). This is why House on Rock - LangSec in Ethereum Classic argues that gas metering (a resource bound, decidable) cannot substitute for a safety guarantee (semantic, undecidable).

Liveness Property

Tags

Backlinks