A logic for properties of executions over time: “always”, “eventually”, “until”. Pnueli brought it to program verification in 1977 (see his paper). Robot specifications, monitors and planners use it.
Mentioned in
7 papers:
- 3DSG survey (2026)
- LLM-guided scene graph planning (2023)
- ROSMonitoring (2020)
- Shielded RL (2018)
- Shield synthesis (2015)
- LTL3 (2011)
- Temporal logic of programs (1977)