Information Technology Reference
In-Depth Information
Our next concern is to axiomatize the notion of acceptable states wrt. a
set of state constraints. Based on the denition of predicate
Holds
, (2.20),
the encoding of fluent formulas is straightforward. In order to state that
some formula
F
is true in the state represented by some term
s
, each fluent
literal
`
occurring in
F
is replaced by the expression
Holds
(
`; s
). E.g., state
constraint
s
2
) becomes
Holds
(
light
;s
)
Holds
(
up
(
s
1
)
;s
)
^ Holds
(
up
(
s
2
)
;s
)
just like state constraint
8x
[
fleeing
(
x
)
alive
(
x
) ] becomes
(
s
1
)
^
(
light
up
up
8x
[
Holds
(
fleeing
(
x
)
;s
)
Holds
(
alive
(
x
)
;s
)]
For notational convenience we will simply write
Holds
(
F; s
) as abbrevia-
tion of the formula thus constructed which states that
F
is true in
s
. This
encoding of fluent formulas is justied by the following proposition.
Proposition 2.9.3.
Let F be a closed fluent formula and S a state.
Then EUNA;
(2
:
20)
j
=
Holds
(
F;
S
)
if and only if F is true in S, else
EUNA;
(2
:
20)
j
=
:Holds
(
F;
S
)
.
Proof.
A fluent literal
`
is true in
S
i
f`gS
. Following clause 2 of Propo-
sition 2.9.1, the latter is equivalent to
EUNA j
=
9z: `z
=
S
, which in turn is
equivalent to
EUNA;
(2
:
20)
j
=
Holds
(
`;
S
) according to axiom (2.20). The
claim follows by straightforward induction on the structure of formula
F
.
Qed.
In particular, a state term is
Acceptable
s
if it satises the underlying steady
state constraints
C
s
, and it is
Acceptable
if it satises the entire state con-
straints
C
, that is,
^
Acceptable
s
(
s
)
Holds
(
F; s
)
F 2C
s
^
(2.23)
Acceptable
(
s
)
Holds
(
F; s
)
F 2C
Suppose, for example,
s
2
)
;s
)]
then we can conclude, for instance,
Acceptable
(
:
up
(
s
1
)
up
(
s
2
)
:
light
)
and
:Acceptable
(
Acceptable
(
s
)
[
Holds
(
;s
)
Holds
(
(
s
1
)
;s
)
^ Holds
(
(
light
up
up
(
s
1
)
:
(
s
2
)
).
up
up
light
