III.5 Satisfiable and valid
Satisfiable and valid [Slide 101]
- A propositional ITL formula f is satisfiable if and only if there exists
an interval σ such that M⟦f⟧(σ) = tt.
- A propositional ITL formula f is valid if and only if for all intervals σ,
M⟦
f⟧(σ) = tt.
Example 29.
- (f ; empty) ≡ (empty ; f) is a valid formula.
- Formula (P ∧ empty) ; skip ; (P ∧ empty) is satisfiable because
M⟦
(P ∧empty) ; skip ; (P ∧empty)
⟧
(σ) = tt where interval σ is σ0σ1
and σ0(P) = tt and σ1(P) = tt.