The fourth rung · what holds over time
Temporal Arithmetic
The first three rungs judge a single state — is it safe, is it good, is it permitted. But an agent produces a trajectory, and the properties that matter most range over the whole run: nothing bad ever happens, the goal is eventually reached, progress is made infinitely often. This is Linear Temporal Logic, made executable: an algebra of safety and liveness, evaluated by formula progression — the same step-at-a-time derivative that drives runtime monitoring.
1 · alethic — necessity / safety → Invariant Arithmetic · refuses
2 · axiological — value / preference → Heuristic Arithmetic · ranks
3 · deontic — obligation / permission → Deontic Arithmetic · obliges & escalates
4 · temporal — liveness over trajectories → this page · shields & sustains
5 · reflexive — self-revising norms → later
IThe algebra
A Spec is an LTL formula over atomic predicates on states. Four temporal operators, the standard ones, plus the Boolean connectives:
| operator | reads | fixpoint identity (what progression implements) |
|---|---|---|
| X φ next | φ holds at the next step | progress(Xφ, s) = φ |
| G φ always | φ holds at every step | Gφ ≡ φ ∧ X Gφ |
| F φ eventually | φ holds at some step | Fφ ≡ φ ∨ X Fφ |
| φ U ψ until | φ holds until ψ does | φUψ ≡ ψ ∨ (φ ∧ X(φUψ)) |
Derived: GF φ (always-eventually — infinitely often), FG φ (eventually-always — stabilizes), and request/response p ⟹ ◇q. The one operation that makes this run online is progression:
τ ⊨ φ iff τ¹ ⊨ progress(φ, τ₀)
progress(φ, s) rewrites a formula into the residual obligation on the rest of the trajectory after seeing state s — the LTL derivative. Monitoring is just a fold of progress over the states; the residual collapses to ⊤ (satisfied) or ⊥ (violated) the moment the outcome is forced. This is the temporal analogue of the invariant layer's chain.
Safety and liveness
Every linear-time property is the conjunction of a safety property and a liveness property (Alpern & Schneider). The split is exactly the seam between rungs 1–3 and this one:
SAFETY — G ¬bad
"nothing bad ever happens." A violation has a finite witness — you can point to the step where it breaks. So safety can be enforced as a runtime shield: one step of lookahead prunes any action whose successor state would drive the residual to ⊥.
extends the alethic floor across time.
LIVENESS — F good
"something good eventually happens." No finite prefix can falsify it — there is always still a chance later. It can only fail by running out of horizon. So liveness behaves as a temporal obligation with a deadline; unmet, it escalates.
extends the deontic ought across time.
That second observation is the unification: a one-step deontic obligation and a liveness goal are the same thing at different horizons, and they share the same contrary-to-duty escalation when they cannot be met.
IIThe laws
Eight for the temporal algebra, three for the interaction with the bridge. The keystone is T4 — progression agrees with the semantics — which the harness checks by running the monitor against an independent recursive evaluator on random formulas.
| T1 | G and F are idempotent (GGφ ≡ Gφ) |
| T2 | duality: ¬Gφ ≡ F¬φ, ¬Fφ ≡ G¬φ |
| T3 | ∧, ∨ over specs are commutative and idempotent (a lattice) |
| T4 | progression is faithful: monitor(φ, τ) ≡ evalDirect(φ, τ) |
| T5 | safety has a finite witness; liveness never commits to false before the horizon |
| T6 | G(φ∧ψ) ≡ Gφ∧Gψ, F(φ∨ψ) ≡ Fφ∨Fψ |
| T7 | the until fixpoint: φUψ ≡ ψ ∨ (φ ∧ X(φUψ)) |
| T8 | on a lasso ⟨stem⟩⟨loop⟩ω: GF p ⇔ p somewhere in loop; FG p ⇔ p everywhere in loop |
| TB1 | the safety shield prunes a step whose successor would violate |
| TB2 | an unmet liveness obligation escalates (contrary-to-duty) at the horizon |
| TB3 | a safety violation yields an unsafe verdict with the witness step |
IIIThe laws, checked
Same harness as the other rungs — each law against random inputs, in your browser, on the engine that ships in box-and-box. T4 in particular runs random formulas through both the progression monitor and the reference evaluator and checks they agree.
IVType sketch
// an LTL spec over predicates on states type Spec = | { t:"atom"; pred:(s:State)=>boolean } | { t:"not"|"next"|"always"|"eventually"; a:Spec } | { t:"and"|"or"|"until"; a:Spec; b:Spec }; // the LTL derivative — residual obligation on the suffix function progress(f: Spec, s: State): Spec; // fold progress; verdict collapses to satisfied / violated, else pending function monitor(f: Spec, τ: State[]): { verdict:"satisfied"|"violated"; online: Verdict[]; residual: Spec }; // safety → shield (one-step lookahead) · liveness → obligation (escalates at horizon) function guard(residual: Spec, next: State): boolean; // would `next` violate? function supervise(τ: State[], specs: TemporalSpec[]): { safe: boolean; escalation: { required:true; specs:{ id; repair; reason }[] } | null; };
VWorked example
An agent runs a multi-step task. States carry the invariant Value's fields, so the atoms are predicates over the real substrate: a safety spec G(β ≥ 0.8) — confidence never drops — and a liveness spec F(done) — the task eventually completes, with a contrary-to-duty repair escalate-replan. Watch the verdicts, and the shield one step ahead. Runs live.
VIStanding on
Linear Temporal Logic is Pnueli's (1977); the safety/liveness decomposition is Alpern & Schneider's (1985); the three-valued online verdict (satisfied / violated / pending) is the runtime-verification tradition (Bauer, Leucker & Schallhart, 2011); and formula progression — evaluating a temporal formula one state at a time by rewriting it — is Bacchus & Kabanza's (2000). The safety shield is the same shielding idea the invariant bridge uses, lifted from a single action to a trajectory. None of it is new; the contribution is the executable synthesis and the wiring onto the rest of the ladder.
Alpern, B. & Schneider, F. (1985). Defining Liveness. Information Processing Letters 21.
Bacchus, F. & Kabanza, F. (2000). Using Temporal Logic to Express Search Control Knowledge. Artificial Intelligence 116.
Bauer, A., Leucker, M. & Schallhart, C. (2011). Runtime Verification for LTL and TLTL. ACM TOSEM 20.