Go backward to
Rigid Variables and Quantifiers
Go up to
Top
Go forward to
Simple Temporal Logic
The Enabled Predicate
Enabled
A
True for
s
iff it is possible to take an
A
step starting in
s
.
s
[[
Enabled
A
]]
<=>
exists
t
in
St
:
s
[[
A
]]
t
Syntactic definition
v
i
all (flexible) variables in
A
.
Enabled
A
<=>
exists
c
1
, ...,
c
n
:
A
(
c
1
/
v'
1
, ...,
c
n
/
v'
n
).
Enabled
(
y
= (
x'
)
2
+
n
) =
exists
c
:
y
=
c
2
+
n
If
A
represents actomic operation,
Enabled
A
is true for those states in which it is possible to perform the operation.
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998