TLA+ (Temporal Logic of Actions)

Origin. Leslie Lamport (1990s). Concurrent systems. Actions as formulas. Stuttering invariance. Foundation of distributed systems verification.

Models. States and actions. Temporal logic over behaviors. Stuttering equivalence. Refinement mapping. Specification of concurrent systems.

Formalism.

State and action: State: assignment to variables. Action: relation between states (primed/unprimed). x' = x + 1: action updating x. Enabled(A): action can occur.

Behavior: σ = s₀ → s₁ → s₂ → ... Infinite sequence of states. Behavior satisfies formula. Model of specification.

Temporal operators: □P: always P. ◇P: eventually P. P ⊢ Q: P leads to Q. □[A]_v: stuttering action.

Stuttering: □[A]_v ≡ □(A ∨ v' = v). Allow steps where v unchanged. Stuttering equivalence. Refinement basis.

Specification form: Init ∧ □[Next]_vars ∧ Fairness. Initial condition. Next-state relation. Fairness: liveness.

Fairness: WF_v(A): weak fairness (if enabled forever, occurs). SF_v(A): strong fairness (if enabled infinitely, occurs). Liveness constraints.

TLC model checker: Exhaustive state exploration. Finite-state abstraction. Error traces. Parallel checking.

Symbols.

Symbol	Unicode	Meaning
x'	—	next-state value
□	U+25A1	always
◇	U+25C7	eventually
[A]_v	—	stuttering action

Metatheory. Stuttering invariance. Refinement. Fairness. Compositionality.

Applies to. Distributed systems. Concurrent algorithms. Protocols. Amazon use.

Limitations. Finite-state checking. Proof complexity. Learning curve. Modeling decisions.