Go backward to Some Useful Temporal FormulasGo up to TopGo forward to The Raw Logic |

- Validity of
*F*(|=*F*)- |=
*F**<=>**forall*`sigma`in**St**:^{infinity}`sigma`[[*F*]] set of all possible behaviors.^{infinity}

- |=
- Representation of algorithm:
- Temporal formula
*F*: `sigma`[[*F*]] =**true**iff`sigma`represents a possible execution of the algorithm.

- Temporal formula
- Property
*G*of algorithm:- |=
*F**=>**G*. - Algorithm represented by
*F*satisfies property*G*.

- |=
- Rules will be introduced for proving temporal formulas.
- Soundness: |-
*F**=>*|=*F*.

- Soundness: |-

Author: Wolfgang Schreiner

Last Modification: May 14, 1998