Obsidian/Zettelkasten/Permanent Notes/20250818132022-temporal-logic.md

id	title	type	created	modified	tags
20250818132022	Temporal Logic	permanent	2025-08-18T17:20:22Z	2025-08-18T20:49:51Z

Temporal Logic

What is Temporal Logic?

An extension of predicate logic that allows reasoning about how statements evolve over time.

• Used heavily in formal verification, model checking, and control systems safety.
• Reasoning is over infinite traces (sequences of states).

---

Core Temporal Operators

Symbol	LaTeX	Name	Meaning
X φ	X \varphi	Next	φ holds in the next state
F φ	\Diamond \varphi	Eventually	φ will hold at some time in the future
G φ	\Box \varphi	Globally (Always)	φ holds at all future times
φ U ψ	\varphi \, U \, \psi	Until	φ must hold until ψ holds

---

Example Specifications

1. Safety:
   “The reactor temperature never exceeds 600°C.”
   G\,(temp < 600)

2. Liveness:
   “The pump will eventually turn on.”

   F(PumpOn)

3. Response:
   “Whenever a request occurs, it will eventually be granted.”
   G\,(request \rightarrow F\,grant)

4. Stability:
   “If the valve opens, it stays open until pressure is safe.”
   G\,(ValveOpen\rightarrow (ValveOpen\;U\;PressureSafe))

Why It Matters

• Formal Methods: Express constraints on system behaviors over time.
• Model Checking: Tools like SPIN, NuSMV, Spot verify LTL specs.
• Engineering Applications:
  • Ensure control systems obey safety invariants.
  • Specify liveness goals for controllers (e.g., “eventually stabilize temperature”).
  • Used in TLA+, runtime monitoring, and shield synthesis.