Information Technology Reference
In-Depth Information
Ramify
s
(
s; e; s
0
;e
0
)
8
<
9
=
8s
1
;e
1
:
(
s
1
;e
1
;s
1
;e
1
)
^
2
3
8s
1
;e
1
;s
2
;e
2
;s
3
;e
3
[
(
s
1
;e
1
;s
2
;e
2
)
^ Causes
s
(
s
2
;e
2
;s
3
;e
3
)
(
s
1
;e
1
;s
3
;e
3
)]
4
5
8
(2.32)
:
;
(
s; e; s
0
;e
0
)
^ Acceptable
s
(
s
0
)
That is, an instance
Ramify
s
(
s; e; s
0
;e
0
) holds if and only if (
s; e; s
0
;e
0
)be-
longs to the transitive closure of
Causes
s
and if
s
0
satises the underlying
steady state constraints. Analogously, we dene
Ramify
(
s; e; s
0
)
8
<
9
=
8s
1
;e
1
;s
2
;e
2
: Ramify
s
(
s
1
;e
1
;s
2
;e
2
)
(
s
1
;e
1
;s
2
;e
2
)
^
2
3
8s
1
;e
1
;s
2
;e
2
;s
3
;e
3
;s
4
;e
4
[
(
s
1
;e
1
;s
2
;e
2
)
^ Causes
(
s
2
;e
2
;s
3
;e
3
)
^ Ramify
s
(
s
3
;e
3
;s
4
;e
4
)
(
s
1
;e
1
;s
4
;e
4
)]
4
5
8
(2.33)
:
;
9e
0
:
(
s; e; s
0
;e
0
)
^ Acceptable
(
s
0
)
That is, an instance
Ramify
(
s; e; s
0
) holds if and only if there exists some
e
0
such that (
s; e; s
0
;e
0
) belongs to the transitive closure of joining
Ramify
s
to
Causes
, and if
s
0
satises the underlying entire set of state constraints. Com-
bining the axiomatization of action laws with this denition of ramication
leads to the following characterization of successor states:
Successor
(
s; a; s
0
)
9c; e; z
[
Action
(
a; c; e
)
^ c z
=
s ^ Ramify
(
z e; e; s
0
)]
(2.34)
To summarize, let
D
be a ramication domain, and let then
FC
D
denote the
union of
EUNA
with the denitions of
Holds
, axiom (2.20);
Acceptable
and
Acceptable
s
, axiom (2.23);
Action
, axiom (2.24);
Causes
s
and
Causes
, ax-
ioms (2.29) and (2.30);
Ramify
s
and
Ramify
, axioms (2.32) and (2.33); and
Successor
, axiom (2.34). The axioms
FC
D
provide a correct axiomatization
of transition in ramication domains, as the following theorem shows.
Theorem 2.9.1.
Let D be a ramication domain and FC
D
its encoding.
Furthermore, let S and S
0
be two states and a an action. Then
FC
D
j
=
Successor
(
s; a; s
0
)
i there is a successor state S
0
of S and a such that EUNA j
=
s
0
=
S
0
,
else
FC
D
j
=
:Successor
(
s; a; s
0
)
