Dane Sabo
ae0ab17291
R "Zettelkasten/Hub Notes/NNFM Ontology.canvas" -> "NNFM Ontology.canvas" R "Zettelkasten/Hub Notes/Permanent Notes/Programming/Assembly/Assembly Canvas.canvas" -> "Programming/Assembly/Assembly Canvas.canvas" R "Zettelkasten/Hub Notes/Permanent Notes/Programming/Assembly/Untitled.md" -> Programming/Assembly/Untitled.md R "Zettelkasten/Hub Notes/Permanent Notes/Programming/Formal Methods/LEAN/Learning Plan.md" -> "Programming/Formal Methods/LEAN/Learning Plan.md" R "Zettelkasten/Hub Notes/Permanent Notes/Programming/Formal Methods/LEAN/Tutorial World.md" -> "Programming/Formal Methods/LEAN/Tutorial World.md" R "Zettelkasten/Hub Notes/Permanent Notes/Programming/Formal Methods/TLA/TLA Canvas.canvas" -> "Programming/Formal Methods/TLA/TLA Canvas.canvas" R "Zettelkasten/Hub Notes/Permanent Notes/Programming/Formal Methods/TLA/TLA+ Learning Plan.md" -> "Programming/Formal Methods/TLA/TLA+ Learning Plan.md" R "Zettelkasten/Hub Notes/Permanent Notes/Programming/Formal Methods/TLA/What is TLA?.md" -> "Programming/Formal Methods/TLA/What is TLA?.md"
61 lines
1.7 KiB
Markdown
61 lines
1.7 KiB
Markdown
---
|
|
id: 20250818132022
|
|
title: Temporal Logic
|
|
type: permanent
|
|
created: 2025-08-18T17:20:22Z
|
|
modified: 2025-08-18T20:49:51Z
|
|
tags: []
|
|
---
|
|
|
|
# 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.
|
|
|