Designing Multi-Agent Systems from Logic Specifications - Distributed Artificial Intelligence, Agent Technology, and Collaborative Applications - page 10

• Maintenance agent (MA): The maintenance agent provides proxy services to the instructor. It

takes updating instructions from the instructor and dispatches them to the monitoring agent. We
use UD to denote the domain of updates made by the instructor and predicate MA ( u , l ) to denote
that an update is made on topic link l . We assume that there is only one instructor in the system.

There are two databases used by this system:

• Topic tree or Link database (LK): The course material is organized in the form of a topic tree.

Each entry in the topic tree is a link to a Web page. We use LK to denote the domain of topic
links.

• Student information database (DT): This database maintains student information and their mail

boxes. We use DT to denote the domain of students.

Note that although we will focus on modeling the agent conversation in the following discussion,
we would like to point out that by no means we are talking about the entire system for e-learning. As a
matter of fact, the background system has other functionalities that we do not address here (Lin, Lin,
& Holt, 2003). Our point is to describe our methodology to specify agent conversation in a distributed
system.
Based on the above conversation schema, the ground theory TH should include the following con-
straints:

A1: ∀ u : UD . ∀ l : LK . ( MA ( u , l ) → ∃ n : NF . MT ( l , n ))
A2. ∀ l : LK . ∀ n : NF . ( MT ( l , n ) → ∃ e : EM . NT ( n , e ))
A3. ∀ n : NF . ∀ e : EM . ( NT ( n , e ) → ∀ s : DT . ST ( e , s ))

A1 means that if the instructor makes any update on any topic link, there exists a notification message
that is generated to notify the change made on the topic link. A2 means that for any notification message
that is generated to notify a change made on any topic link, there exists an email to deliver the notice.
A3 means that for any email that is generated to deliver any notice, the email to sent to all students.
The logic specification of the system is:

spec ≡ ∀ u : UD . ( TH → ∃ e : EM . ∀ s : DT . ST ( e , s ))

which means that for any update made by the instructor, an email notification is sent to all students.
The input is u and the goal is:

goal ≡ ∃ e : EM . ∀ s : DT . ST ( e , s )

The goal is not verifiable with respect to the given input because the input is not present in the goal,
which means that the input and the output are not handled by the same agent. Based on constraint A3,
we can infer that:

∀ n : NF . ∀ e : EM . ( NT ( n , e ) → ∀ s : DT . ST ( e , s ))
⇒ ∀ n : NF . ∃ e : EM . ( NT ( n , e ) → ∀ s : DT . ST ( e , s ))