Propositional Linear Temporal Logic

Propositional Linear Time Logic, or PLTL for short, extends Classical Propositional Logic with Modal operators that allow one to reason about time. As the name suggests, PLTL is a Temporal Logic.

The grammar of PLTL is given by

φ,ψ::=x∣⊤∣⊥∣φ∨ψ∣φ∧ψ∣φ⇒ψ∣○φ∣φ𝒰ψ∣φℛψ\varphi,\psi::=x\mid\top\mid\bot\mid\varphi\lor\psi\mid\varphi\land\psi\mid% \varphi\Rightarrow\psi\mid\bigcirc\varphi\mid\varphi\mathcal{U}\psi\mid\varphi% \mathcal{R}\psi

Textual Symbolic Explanation
X ⁢ φ 𝑋 𝜑 X\varphi ○ φ ○ absent 𝜑 \bigcirc\varphi φ 𝜑 \varphi has to hold in the next state
φ ⁢ U ⁢ ψ 𝜑 𝑈 𝜓 \varphi U\psi φ ⁢ 𝒰 ⁢ ψ 𝜑 𝒰 𝜓 \varphi\mathcal{U}\psi ψ 𝜓 \psi must hold at some point in the future, and φ 𝜑 \varphi must hold until that happens.
φ ⁢ R ⁢ ψ 𝜑 𝑅 𝜓 \varphi R\psi φ ⁢ ℛ ⁢ ψ 𝜑 ℛ 𝜓 \varphi\mathcal{R}\psi ψ 𝜓 \psi must be true until φ 𝜑 \varphi is true; if φ 𝜑 \varphi is never true, then ψ 𝜓 \psi must be true forever

We can construct additional modal operators ⋄ φ = ⊤ 𝒰 ⁢ φ ⋄ 𝜑 top 𝒰 𝜑 \diamond\varphi=\top\mathcal{U}\varphi and □ ⁢ φ = ⊥ ℛ ⁢ φ □ 𝜑 bottom ℛ 𝜑 \square\varphi=\bot\mathcal{R}\varphi that correspond to Eventuality Modality and the Necessity Modality, resp.

Semantics

References