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"
64 lines
1.8 KiB
Markdown
64 lines
1.8 KiB
Markdown
---
|
|
id: 20250818132022
|
|
title: Temporal Logic
|
|
type: permanent
|
|
created: 2025-08-18T17:20:22Z
|
|
modified: 2025-08-21T16:42:25Z
|
|
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.
|
|
|
|
## Related Notes
|
|
[[strix]] - a reactive synthesis tool using temporal logic
|
|
specs
|