Information Technology Reference
In-Depth Information
s
1
)] to denote what we call
observations
. A scenario
can then be modeled as a collection of observations, and drawing the right
conclusions amounts to deciding which observations follow from the given
ones. E.g.,
:
up
(
s
1
) after [ ] could be one such conclusion.
Observations may be more complex than the two examples just men-
tioned. For instance,
(
s
1
) after [
(
up
toggle
s
2
) after [ ] says that both switches are
in the same position|though it is not known what position they share. A rea-
sonable conclusion here would be, say,
:
(
up
(
s
1
)
up
(
s
2
)) after [
toggle
(
s
2
)],
that is, toggling the second switch results in both switches being in dierent
positions. Another variant is to ask hypothetical questions like the following.
Suppose the result of toggling
s
2
would be that all switches have the same
position. Suppose further that toggling
s
1
would bring this switch down.
What, then, follows as for the result of toggling both
s
1
and
s
2
? Clearly,
the assumptions imply that initially
(
s
1
)
(
up
up
s
2
is down. From
this we conclude that the right answer to the question is that switch
s
1
is
down and switch
s
2
is up. More formally, we say that the two observations
8x:
s
1
is up and (hence)
(
x
)
_8x: :
s
2
)]
:
up
(
s
1
) after [
toggle
(
s
1
)]
(
x
) after [
(
up
up
toggle
(1.4)
entail
the observation
:
up
(
s
1
)
^
up
(
s
2
) after [
toggle
(
s
1
)
;
toggle
(
s
2
)].
Again, to reiterate the obvious, the conclusion relies on the correct denition
of the action laws. In the remainder of this section, we show how conclusions
of this kind are obtained on a formal basis. To this end, we rst need a
precise denition of observations. This in turn requires the formal notion of
a so-called fluent formula, such as
:
(
up
(
s
1
)
up
(
s
2
)) or
8x: :
up
(
x
).
Denition 1.2.4.
Given sets of entities, fluent names, and variables, the set
of
fluent formulas
is inductively dened as follows: Each fluent expression and
> (tautology) and ? (contradiction) are fluent formulas, and if F and G
are fluent formulas so are :F , F ^ G, F _ G, F G, F G, 9x: F ,
and 8x: F (where x is a variable). A
closed
formula is a fluent formula
without free variables, that is, where variables only occur in the scope of some
quantier using this variable.
8
Denition 1.2.5.
Let E , F , and A be sets of entities, fluent names, and
action names, respectively. An
observation
is of the form
F
after [
a
1
(
e
1
)
;:::;a
n
(
e
n
)]
where F is a closed fluent formula and each of a
1
(
e
1
)
;:::;a
n
(
e
n
)
is an
action (n
0
).
Denition 1.2.6.
A
basic action scenario
is a pair
(
O; D
)
where D is a
basic action domain and O is a set of observations (based on the entities
and fluent and action names in D).
8
The
scope
of the quantiers in
9x: F
and
8x: F
is dened as the sub-
formula
F
.
