ITL
© 1996-2018







III.5 Satisfiable and valid

Satisfiable and valid [Slide 99]

  • A propositional ITL formula f is satisfiable if and only if there exists an interval σ such that Mf(σ) = tt.
  • A propositional ITL formula f is valid if and only if for all intervals σ, Mf(σ) = 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.







2018-02-25
Contact | Home | ITL home | Course | Proofs | Algebra | FL