Temporal Property Specification¶

Why It Matters¶

Many critical properties are inherently temporal and can't be captured in static specifications. "The system never deadlocks" (safety), "every request eventually receives a response" (liveness), "if A happens, then B happens before C" (ordering). Temporal specification catches bugs that single-state checks miss.

The Key Move¶

When specifying system behavior, distinguish temporal modalities. Does this property hold in every state (always) or just eventually (finally)? Must it hold starting now (globally) or from some future point (eventually-always)? Express complex properties as combinations: "always (if request then eventually response)."

Classic Application¶

Protocol verification. A mutual exclusion protocol must satisfy: "always (at most one process in critical section)" (safety) and "always (if process requests critical section, eventually it enters)" (liveness). Both are essential; testing might catch safety violations but often misses liveness failures (starvation).

Surprising Application¶

Relationship commitment. "We'll never fight" (safety) is unrealistic and unnecessary. Better: "Always (if conflict arises, eventually we address it constructively)" (liveness with safety). This admits conflict (realistic) while guaranteeing resolution (essential). The temporal structure clarifies what commitment means.

Failure Modes¶

Vacuous satisfaction - a liveness property "eventually X" is satisfied if the system terminates (eventually nothing happens). Conflating safety and liveness - confusing "never bad" with "always good." Untestable properties - temporal properties over infinite time can't be tested, only verified formally. Specification complexity - complex temporal properties become unreadable.

Go Deeper¶

Lamport, "Proving the Correctness of Multiprocess Programs" (1977); Pnueli, "The Temporal Logic of Programs" (1977)