Go backward to Temporal Formulas
Go up to Top
Go forward to Validity and Provability
Some Useful Temporal Formulas
- Eventually (eventually )
- is eventually true.
- eventually not always not .
- <, , ...>[[eventually ]]
exists in Nat: <, , ...>[[]]
- Infinitely Often (always eventually )
- <, , ...>[[always eventually ]]
forall in Nat: exists in Nat:
<, , ...>[[]]
- Eventually Always (eventually always )
- <, , ...>[[eventually always ]]
exists in Nat: forall in Nat:
<, , ...>[[]]
- Leads to ()
- always ( eventually )
- Any time is true, is true then or at some later time.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine