Go backward to Some Useful Temporal Formulas
Go up to Top
Go forward to The Raw Logic
Validity and Provability
- Validity of (|= )
- |= forall sigma in St: sigma[[]]
- set of all possible behaviors.
- Representation of algorithm:
- Temporal formula :
- sigma[[]] = true iff sigma represents a possible
execution of the algorithm.
- Property of algorithm:
- |= .
- Algorithm represented by satisfies property .
- Rules will be introduced for proving temporal formulas.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine