Information Technology Reference
In-Depth Information
designing Mul ti-agent syste Ms fro M logic sPecifica tions
A special issue in a distributed system is that the system is composed of interacting, but independent
program units, each has its own data domain; and the architectural design focuses on the conversation
among these units (Bradshaw, 1997). A conversation is a sequence of messages involving two or more
agents and centering on a set of pre-designated topics, intended to achieve a particular purpose. To
correctly and efficiently engineer software architecture, we can model and specify agent interactions
in distributed learning as conversation schemata, in which interaction patterns and task constraints
in collaborative agent systems are constructed within class hierarchies of conversation schemata (Lin
et. al., 2000). When the agent system is modeled by γ-Calculus, conversation is modeled as solution,
which can be constructed automatically when the logic specification is converted into the verification
program, if the conversing agents and their input-output are included in the specification. Therefore,
for a specification in the form of
spec
≡ ∀
a
:
T
a
. (
TH
→ ∃
z
:
T
z
.
Q
(
a
,
z
))
when input
a
and output
z
are not handled by the same agent,
spec
must be decomposed into a series
of sub-specifications:
spec
i
=
∀
x
i
:
T
i
. (
TH
i
→∃
x
i
+1
:
T
i
+1
.
Q
i
(
x
i
,
x
i
+1
))
i
= 0, …,
n
where
x
0
=
a
and
x
n
+1
=
z
, and sub-goals
goal
i
(
x
i
)
=
∃
x
i
+1
:
T
i
+1
.
Q
i
(
x
i
,
x
i
+1
)
i
= 0, …,
n
to be verifiable, where
Q
i
(
x
i
-1
,
x
i
) is the specification of an agent with respect of the conversation and
TH
i
and its ground theory (or constraints). To this end, theory
TH
(=
TH
0
∪ … ∪
TH
n
) may be used to
decompose the original specification.
Because the output
x
i
+1
of
goal
i
is the input to
goal
i+
1
, the verification program of
goal
i+
1
must use the
result obtained by the verification program of
goal
i
. Referring to Section 3, we know the verification
program of a logic expression is a solution. Let <
goal
i
> be the verification program of
goal
i
, according
to the the construction rules, when <
goal
i
> is inert, it must be either <
x
i
+1
,
true
> or <
false
>, where
x
i
+1
is the result. Let's define:
extract
= γ<
x
,
true
>
true
.
x
fail
= γ<
false
>
true
.
false
result
= γ<
x
,
false
>
true
.
x
then the verification program of
goal
i+
1
can be written as:
<goal
i+
1
[
extract
,
fail
,
result
, <
goal
i
>]>
For example, let's consider an online course material maintenance system, which was studied in
(Lin, Lin, & Holt, 2003), (Lin, 2004), and (Lin & Yang, 2006). The conversation schema is shown in
Figure 1. As we know of e-learning systems, the online course materials are updated often in order to
keep them as current as possible, esp. in some rapidly changing fields like “computing and information
Search WWH ::
Custom Search