Go backward to Temporal Formulas Go up to Top Go forward to Validity and Provability

Some Useful Temporal Formulas

• Eventually (eventually )
  • F is eventually true.
  • eventually F <=> not always not F.
  • <s₀, s₁, ...>[[eventually F]] <=>
       exists n in Nat: <s_n, s_n+1, ...>[[F]]
• Infinitely Often (always eventually )
  • <s₀, s₁, ...>[[always eventually F]] <=>
       forall n in Nat: exists m in Nat:
       <s_n+m, s_n+m+1, ...>[[F]]
• Eventually Always (eventually always )
  • <s₀, s₁, ...>[[eventually always F]] <=>
       exists n in Nat: forall m in Nat:
       <s_n+m, s_n+m+1, ...>[[F]]
• Leads to (|->)
  • F |-> G <=> always (F => eventually G)
  • Any time F is true, G is true then or at some later time.