Go backward to
Simple Temporal Logic
Go up to
Top
Go forward to
Some Useful Temporal Formulas
Temporal Formulas
Always
(
always
)
Elementary formulas
E
1
, E
2
not
E
1
and
always
(
not
E
2
)
always
(
E
1
=>
always
(
E
1
or
E
2
))
Semantics based on
behaviors
Infinite sequences of states.
Behavior
sigma
= <
s
0
,
s
1
, ...>
sigma
[[
F
]] in
Bool
.
sigma
satisfies
F
iff
sigma
[[
F
]] =
true
.
Meaning of temporal formulas:
<
s
0
,
s
1
, ...>[[
F
]]
<=>
s
0
[[
F
]], if
F
elementary.
sigma
[[
F
and
G
]]
<=>
sigma
[[
F
]]
and
sigma
[[
G
]]
sigma
[[
not
F
]]
<=>
not
sigma
[[
F
]]
<
s
0
,
s
1
, ...>[[
always
F
]]
<=>
forall
n
in
Nat
: <
s
n
,
s
n+1
, ...>[[
F
]]
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998