Go backward to
Quantification over Flexible Variables
Go up to
Top
Go forward to
Quantification in TLA
Quantification over Flexible Variables
"Obvious" definition:
sigma
[[
exists
x
:
F
]]
<=>
exists
tau
in
St
infinity
: (
sigma
=
x
tau
)
and
tau
[[F]]
Not correct since not necessarily invaraint under stuttering!
Remove stuttering steps:
#<
s
0
,
s
1
, ...>
<=>
if
forall
n
in
Nat
:
s
n
=
s
0
then
<
s
0
,
s
0
, ...>
else if
s
1
=
s
0
then
#<
s
1
,
s
2
, ...>
else
<
s
0
> o #<
s
1
, ...>
TLA = STLA + quantification.
Existential quantifier over flexible and rigid variables.
All TLA formulas are invariant under stuttering:
#
sigma
= #
tau
=>
sigma
[[
F
]] =
tau
[[
F
]]
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998