[go: up one dir, main page]
Scribd
Upload
9 views31 pages

FM-Lect11-Spring2025-Linear Temporal Logics

The document discusses Temporal Logics, specifically Linear Temporal Logic (LTL), including its syntax, semantics, and transition systems. It outlines various temporal operators, both for the past and future, and provides examples of their meanings. Additionally, it addresses the equivalence between LTL formulas and model satisfaction in temporal logic contexts.

Uploaded by

i200958 Sheir Muhammad
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
9 views31 pages

FM-Lect11-Spring2025-Linear Temporal Logics

The document discusses Temporal Logics, specifically Linear Temporal Logic (LTL), including its syntax, semantics, and transition systems. It outlines various temporal operators, both for the past and future, and provides examples of their meanings. Additionally, it addresses the equivalence between LTL formulas and model satisfaction in temporal logic contexts.

Uploaded by

i200958 Sheir Muhammad
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
You are on page 1/ 31

Temporal Logics

How would we express this system?

purify-primal-reverb-rise
Temporal Logic
Linear Temporal
Logic
Linear Temporal Logic (LTL)
Syntax of LTL
Semantics of LTL
A Transition System
A Path 𝚷
A Path 𝚷 (example)
LTL Semantics: Path Satisfaction
Example Path
Additional Temporal Operators
Model Satisfaction M, s |= 𝚿
$
Temporal Logics
Equivalence between LTL formulas
Equivalence between LTL formulas
Equivalence between LTL formulas
Equivalence between LTL formulas
Additional Temporal Operators
Past LTL Operators
Past Operator Future LTL Analogue Meaning Example
"ψ was true in YRain: "It rained in the
Yψ (Yesterday) Xψ (Next)
the previous state." last timestep."

"ψ has always been HSafe: "The system has


Hψ (Historically) Gψ (Globally)
true in the past." never been unsafe."

OError: "An error


"ψ was true at least
Oψ (Once) Fψ (Eventually) occurred sometime
once in the past."
before."

WarningSError: "An error


"ϕ happened in the
occurred, and a warning
ψSϕ (Since) ψUϕ (Until) past, and ψ has
has held continuously
held ever since."
since then."

You might also like