Dane Sabo
64f1617e9d
M "Zettelkasten/Permanent Notes/20250818132022-temporal-logic.md" M "Zettelkasten/Permanent Notes/20250819103208-strix.md" A "Zettelkasten/Permanent Notes/20250821123741-syntcomp.md" M "Zettelkasten/Permanent Notes/Literature Notes/LIT-20250819112550-strix-explicit-reactive-synthesis-strikes-back.md"
1.8 KiB
1.8 KiB
| id | title | type | created | modified | tags |
|---|---|---|---|---|---|
| 20250818132022 | Temporal Logic | permanent | 2025-08-18T17:20:22Z | 2025-08-21T16:42:25Z |
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
-
Safety:
“The reactor temperature never exceeds 600°C.”
G\,(temp < 600) -
Liveness:
“The pump will eventually turn on.”F(PumpOn) -
Response:
“Whenever a request occurs, it will eventually be granted.”
G\,(request \rightarrow F\,grant) -
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.
Related Notes
strix - a reactive synthesis tool using temporal logic specs