Go backward to Simple Temporal Logic
Go up to Top
Go forward to Some Useful Temporal Formulas
Temporal Formulas
- Always (always )
- Elementary formulas
- not and always (not )
- always ( always ( or ))
- Semantics based on behaviors
- Infinite sequences of states.
- Behavior sigma = <, , ...>
- sigma[[]] in Bool.
- sigma satisfies iff sigma[[]] = true.
- Meaning of temporal formulas:
- <, , ...>[[]] [[]], if
elementary.
- sigma[[ and ]] sigma[[]] and sigma[[]]
- sigma[[not ]] not sigma[[]]
- <, , ...>[[always ]]
forall in Nat: <, , ...>[[]]
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine