Go backward to
Some Useful Temporal Formulas
Go up to
Top
Go forward to
The Raw Logic
Validity and Provability
Validity
of
F
(|=
F
)
|=
F
<=>
forall
sigma
in
St
infinity
:
sigma
[[
F
]]
infinity
set of all possible behaviors.
Representation of algorithm:
Temporal formula
F
:
sigma
[[
F
]] =
true
iff
sigma
represents a possible execution of the algorithm.
Property
G
of algorithm:
|=
F
=>
G
.
Algorithm represented by
F
satisfies property
G
.
Rules will be introduced for proving temporal formulas.
Soundness: |-
F
=>
|=
F
.
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998