MULTI-AGENT SYSTEM FORMAL MODEL BASED ON
NEGOTIATION AXIOM SYSTEM OF TEMPORAL LOGIC
Xia Youming , Yin Hongli and Zhao Lihong
School of Computer Science and Information Technology,
Yunnan Normal University,Kunming , P.R.China
Keywords: Negotiation Axiom, Semantic Frame, Multi-Agent System, Negotiation Reasoning Logic, Temporal Logic
Abstract: In this paper we describe the formal semantic frame and introduce the formal language L
TN
to express the
time and the ability and right of an agent on selecting action and negotiation process in a Multi-Agent
System, the change of the right over time, the free action of an agent and the time need by a agent to
complete an action. Based on the above, the independent negotiation system has been further complete. In
this paper, it is also addressed that the axiom system is rational, validate and negotiation reasoning logic is
soundness, completeness and consistent.
1 INTRODUTION
The research of agent technique is a new field of
software design and realizationand has caught
people’s attention for years, especially in distribution
and open Internet software developing field. As the
mature of technique and more complex application
problems being put forward, the requirements of
multi-agent system based on peer-to-peer mode
communication have become more and more urgent.
The research of the key technology of MAS’s design
and effective implement has been carried out for
many years in the field of distribution artificial
intelligence.
For MAS, besides the consideration of the
representation and formalization of consciousness
attitude concerning individual agent, it must
consider the alternation of multi agents, the
consciousness attitude that is one of the important
portions of MAS theory research. As being able to
reason about other agents, consciousness attitude is
the main request that makes the agents to coexist,
compete and collaborate. The cooperation and
negotiation can be produced and accomplished
under the control of psychosis. Negotiation of MAS
include negotiation protocol, negotiation strategy
and negotiation disposal. The first part focus on
dealing with the intercommunication among agents,
and the second part has five basic types: one-part
giving in strategy, competitive strategy, cooperation
strategy, destroying strategy and delaying strategy.
This paper is based on Li Jing’s work, and add
temporal logic to complete negotiation between
independent agents by using linear temporal logic
describe right change to make contribution on letting
agents act more freely.
2 NEGOTIATION AXIOM
SYSTEM WITH TEMPORAL
LOGIC
The Negotiation Axiom System based on Capability
and Thought of MAS(Li Jing 03)is viewed as a
sequence of “PerceivingSelecting
actionsNegotiating to resolve conflictsDeciding
actions by arbitrage Executing actions”.
In the TN system (the abbreviation of the
negotiation axiom system with temporal logic), the
primary work unit is spitted into many small units,
that allow agents behaviors to be asynchronous, that
is the starting point of negotiations and the other
actions taken by agents can be different, so a agent is
able to start a negotiation when there is another
agent is still executing an action; Further, when
some agents are executing actions, other agents keep
observing the environment, and then choose their
The work is supported by the Natural Science Foundation of Yunnan province under the grant No. 2003F0038M, the
Key Project of Yunnan Natural Science Foundation under the grant No. 04F00062, and the Province-Institute and
Province-Universit
y
Scientific and technolo
g
ical collaborative
p
ro
j
ect of Yunnan Province
(
2004YX42
)
362
Youming X., Hongli Y. and Lihong Z. (2005).
MULTI-AGENT SYSTEM FORMAL MODEL BASED ON NEGOTIATION AXIOM SYSTEM OF TEMPORAL LOGIC.
In Proceedings of the Seventh International Conference on Enterprise Information Systems, pages 362-365
DOI: 10.5220/0002517503620365
Copyright
c
SciTePress
Perceiving
Selecting actions
Negotiating to resolve
conflicts
Deciding actions
by arbitrage
Executing actions
Figure 2: Interpretation of the negotiation axiom system with temporal logic
Perceiving
Selecting actions
Negotiating to resolve
conflicts
Deciding actions
by arbitrage
Executing actions
Figure 1: Interpretation of the negotiation axiom system based on capability and thought of MAS
next movements based on local states, power and
rights, that is the environment observations are
simultaneous.
In our work, the VSK-AF logic system is still
valid in the course of perceiving, but in the course of
selecting actions, negotiating to resolve conflicts,
deciding actions by arbitrage and executing actions,
we use the negotiation with temporal logic. In the
TN systemnegotiation concurrence is allowed, and
all those negotiations may start at a different time
point, last for a different time period, end at a
different time point.
2.1 Semantic Frame
To discus the TN system we define the following
semantic frame:
T = {t
0
, t
1
, t
2
,…, t
n
, …}: a set of time points;
Actions = {α
0
, α
1
,…}: a set of actions, which
consists of all actions involved in this system;
NS = {ns
0
, ns
1
,…}: a set of negotiation
strategies;
AS = {as
0
,as
1
,…}: a set of arbitrage strategies;
Message = a set of (i,α,w), Ag
i
select the
action α to execute the task w;
E = {e
0
, e
1
, …}: a set of the external
environment states;
S = {s
0
, s
1
, …}: a set of the Agents environment
states;
W = {w
1
, w
2
, …}: a set of tasks;
Environment: one of the two important parts
of the model, denoted as Env = <E, S, W, vis
1
, …,
vis
n
, acce
1
, …, acce
n
, Arbitrage, τ
g
, e
0
, s
0
>;
L
i
= { l
0
i
, l
1
i
…}: the set of local state for Agent
i
;
Agents: one of the two important parts of the
model, denoted as Ag
i
=<L
i
, See
i
, Feel
i
, Th
i
, Ability
i
,
Power
i
, SelectAP
i
, Donetime
i
NS
i
, Decide
i
, CR
i
, τ
i
, l
0
i
, Poss
i
>;
Negotiation: denoted as N=<Ags, Isu, O, V
O
,
Ans, Time, Thread, Protocol>;
TN System: denoted as S=<Actions, NS, AS,
Env, Agents, N, PoS, SR, T>;
Global states for a TN system: denoted as
G={ε
0
, ε
1
, …};
The class of TN system: consists of all TN
system, denoted as S;
Run: A sequence ε
0
, ε
1
, …(enumerable) over G
represents the run of a TN system
The set of reachable states for TN system:
denoted as G
S;
At the very beginning, L
i
is initialized as the initial
local state, E is initialized as the external state, and S
is initialized as the initial agent state, then each
agent start the first observation and use the vis (the
partition function of the external environment for
Agent
i
) and the acce
i
( the partition function of
the Agents environment for Agent
i
) to product a p
0
i
(the acknowledge of the external environment) and a
q
0
i
(the acknowledge of the agents environment),
thus the L
i
transfer to a new local state L
i+1
and we
get a initial global states for the TN system. With the
initial global states, each agent makes its own
selection according to the power and right they have
at this moment, on the contrary, a agent has no
power and right doing nothing till the next time
point comes, they start a new observation. Those
agents with power and right select an action and the
corresponding task, if there is no confliction among
those selected actions, the agent then execute the
selected action, transfer the environment states.
When they finish the execution start an observation
again. Once the conflictions occur, those agents
MULTI-AGENT SYSTEM FORMAL MODEL BASED ON NEGOTIATION AXIOM SYSTEM OF TEMPORAL
LOGIC
363
involved negotiate with each other till the
agreements are finally reached, and they act
according to the agreement to transfer the state of
the system. Till all problems are solved, the process
will be repeated.
2.2 Negotiation Logic in TN System
This section gives an overview of the formal
framework in which the model of negotiation will be
expressed in language L
TN.
The language expresses
the model of negotiation, and describes the system
information, which consists of two parts: the first
part—the language of VSK-AF logic, is used in the
course of perceiving to express the objective
phenomenon in multi-Agent systems, the
information that can be visited, learn or perceived by
a agent in the system, the second part—L
TN
, is used
in the rest phases, to describe how the time, power,
and right effect the agent on the action selection and
negotiation, especially the change of the right during
the whole process.
In TN system, we introduce five temporal
operators: (always),◇(eventually),○(next),◆
(ever),∪(until).
Given a set P of prepositional variables, set
Agents of agents, set Actions of actions, set W of
task, and for an action α∈ Actions has a set of
preconditions Pre(α), and a set of effects Eff(α), the
language L
TN
is defined as below:
A list of predications as following:
Exu(Agi,α,w), Capable(Agi,α), R-Entitle (Agj,Agi,
α), NR-Entitle (Agj, Agi,α), Entitle(Agj,Agi,α),
Right(Agi,α), Done(Agi,α,w), Agree(Γ,ϕ), Bound
(Agi,agm), Commit (Agi, Agj, agm), Benefit(Agi,α),
Select(Agi,α,w), Collision(Agts,α,w), Negotiation
(Agts,α,w), DuringNegotiation (Agts, α, w), Join-
Negotiation(Agi,α,w), OverNegotiation(Agts,Agk,α,
w), Permit(Agi,Agj,Entitle(Agj,Agk,α)), Deprive
(Agi, Agj,α) and so on.
Φ
0
(the set of atomic propositions of L
TN
):
consists of P and predications mentioned above.
Φ (the set of compound formula of L
TN
):
1True, False∈Φ, Φ
0
⊆Φ;
2If ϕ
1
, ϕ
2
∈Φ, then ¬ϕ
1
∈Φ, ϕ
1
ϕ
2
∈Φ,
ϕ
1
∈Φ,ϕ
1
∈Φ,ϕ
1
∈Φ,ϕ
1
∈Φ,ϕ
1
ϕ
2
∈Φ;
3 If ϕ∈Φ and π∈Π, where
iii
))},,(),,,({(
jjj
wAgExuwAgExu
α
α
L=Π
, then
[π]ϕ∈Φ, <π>ϕ∈Φ;
[π]ϕ means it is certain that the execution of
actions in π lead to a state in which ϕ is True; <π>ϕ
means it is possible that the execution of actions in π
lead to a state in which ϕ is True.
2.3 The Semantic of Negotiation
Logic
Definition 2.3.1 The negotiation model is defined as
M =<G
S
, ρ, λ>, where:
G
S
E×S×L
1
××L
n
is the set of all
possible multi-agent world states; the
element ε
i
of G
S
is (n+2)-ary tuple (e,s, l
1
,
l
2
, …, l
n
) called as global state;
ρ:G
S
×Π→ G
S
, is a function that defines
the accessibility relation from states
associated with the action tuple to state.
For instance, if there is a state ε
i
G
S
in
which the execution of actions in π
produces a new state ε
j
G
S
, then (ε
i
,ε
j
) is
said to be “reachable”, denoted (ε
i
,
ε
j
)∈ρ( π);
λ:Φ→2
GS
, is the interpretation function
for formulae; for ϕ∈Φ and ε
i
G
S
, λ(ϕ)
refers to the set of states in which ϕ holds,
and ε
i
∈λ(ϕ) if and only if ϕ holds in ε
i
.
Definition2.3.2 Semantic rules of negotiating logic:
I
T
<M, ε
I
> true
I
P
<M, ε
i
> ϕ iff ε
i
∈λ(ϕ)
I
F
<M, ε
i
> ¬ϕ iff <M, ε
i
> ϕ
I
O
<M, ε
i
> ϕ ψ iff <M, ε
i
> ϕ<
M, ε
i
> ψ
I
N
<M, ε
i
> ϕ iff, <M, ε
i +1
> ϕ
I
A
<M, ε
i
> ϕ iff ∀ε
j
G
S
ε
i
ε
j
, <M,
ε
j
> ϕ
p
I
E
<M, ε
i
> ϕ, iff ε
j
G
S
ε
i
ε
j
, <M,
ε
j
> ϕ
p
I
G
<M, ε
i
> ϕ, iff ε
j
G
S
ε
j
ε
i
, <M,
ε
j
> ϕ
p
Iu <M, ε
i
> ϕψ iff ε
j
G
S
ε
i p
ε
j
, < M,
ε
j
> ψ,and
ε
k
, ε
i
Με
k
ε
j,
p
<M, ε
k
> ϕ
Theorem 2.3.1 M, ε
i
│= [π]ϕ M, ε
i
│=
¬<π>¬ϕ
Theorem 2.3.2 M, ε
i
<π>ϕ M, ε
i
¬[π]¬ϕ
2.4 Axiomatics of L
TN
Transmutation rule of formulas in nego-
tiation logic
T1Substitution rule: If ϕ, ψ are formulae of
L
TN
, and L
TN
ϕ, then if p is a variable in ϕ,
substituting p in ϕ with ψ, the result ϕ satisfies
L
TN
ϕ;
T2Separation rule: From L
TN
ϕ→ψ and
L
TN
ϕ, L
TN
ψ holds;
T3Certainty rule: From L
TN
ϕ, L
TN
[π]ϕ
holds;
T4Temporal rule: FromL
TN
ϕ, L
TN
i
ϕ
j
ICEIS 2005 - ARTIFICIAL INTELLIGENCE AND DECISION SUPPORT SYSTEMS
364
holdswhere
i
={, , , },
FromL
TN
ϕ
i
andL
TN
ϕ
j
, L
TN
ϕ
i
ϕ
j
holds;
The strategy of selecting action
S1If Capable(Ag
i
,α) and Right(Ag
i
,α) and
Benefit(Ag
i
,Exu(Ag
i
,α,w) )then
Select(Ag
i
,α,w)
S2If Right(Ag
i
,α) and Capable(Ag
j
,α) and
¬Right(Ag
j
,α) and Benefit(Ag
i
,Exu(Ag
j
,α,w))
then Entitle(Ag
i
,Ag
j
,α)
S3 If ¬Benefit(Ag
i
,Exu(Ag
i
,α,w)) then
¬Exu(Ag
i
,α,w)
3 SOUNDNESS AND COMPLETE-
NESS OF NEGOTIATION LOGIC
Theorem 3.1 (Soundness of L
TN
) ΓL
TN
ϕ Γ ϕ
Theorem 3.2 (Consistency of L
TN
)There does not
exist formula ϕ that makes ΓL
TN
ϕ and ΓL
TN
¬ϕ
hold at the same time.
Theorem 3.3 (Completeness of L
TN
) Γ ϕ⇒ ΓL
TN
ϕ.
Theorem 3.4 (Logic completeness of L
TN
)∀ϕ∈ L
TN
,
there is one and only one holds between L
TN
ϕ and
L
TN
¬ϕ.
Theorem 3.5The TN system is uncontradictory.
4 NEGOTIATION AND ARBITRA-
GE MECHANISM OF CONFICTS
RESOLVING
Definition 4.1 arbitrage strategies
Strategy 1
If conflict(select(Ag
i
,α,w), select(Ag
j
,α,w)) then
Exu(Ag
i
,α,w);
Strategy 2
If conflict(select(Ag
i
,α,w),select(Ag
j
,α,w)) and
w
1
(w
1
w) and capable(Ag
j
,α
1
) and right(Ag
j
,α
1
)
then Exu(Ag
i
,α,w) and Exu(Ag
j
,α
1
,w
1
);
Strategy 3
If conflict(select(Ag
i
,α,w), select(Ag
j
,α,w)) and
w
1
(w
1
w) and capable(Ag
j
,α
1
) and
¬right(Ag
j
,α
1
)and m right(Ag
m
,α
1
) then
Entitle(Ag
m
,Ag
j
,α
1
) and Exu(Ag
i
,α,w) and Exu(Ag
j
,
α
1
,w
1
);
Strategy 4
If conflict(select(Ag
i
,α,w),select(Ag
j
,α,w)) and
w
1
(w
1
w) and ¬capable(Ag
j
,α
1
) and
¬right(Ag
j
,α
1
) and m capable(Ag
j
,α
2
) and
right(Ag
j
,α
2
) and capable(Ag
m
,α
1
) and right(Ag
m
,α
1
)
then Exu(Ag
i
,α,w) and Exu(Ag
j
,α
2
,w
2
) and
Exu(Ag
m
,α
1
,w
1
).
5 CONCLSION
In this paper we design a negotiation model of
Multi-Agent system based on the temporal logic in
formal theory. In this model we describe the
application of the time and the ability and right of an
agent on selecting action and negotiation process in
a Multi-Agent system, the change of the right over
time, and the free action of an agent.
REFERENCE
N.R.Jennings, P.Faratin et al. Automated Negotiation:
Prospects, Methods and Challenges, Int Journal of
Group Decision and Negotiation, 2000
Sarit Kraus, Automated Negotiation and Decision Making
in Multiagent Environments, 9
th
ECCAI, ACAI 2001,
EASSS 2001 P151-171
Pietro Panzarasa and Nicholas R.Jennings, Formalizing
collaborative decision-making and practical reasoning
in multi-agent systems. Logic computer,
Vol.12,pp.55-117,2002
M. Wooldridge and A. Lomuscio. A Computationally
Grounded Logic of Visibility, Perception, and
Knowledge In Logic Journal of the IGPL
9(2):273-288, 2001.
Li JingMulti-Agent System based on Negotiation Axiom
System of Capability and Thought, master dissertation,
2003, Yunnan Normal University, Kunming P.R.China.
MULTI-AGENT SYSTEM FORMAL MODEL BASED ON NEGOTIATION AXIOM SYSTEM OF TEMPORAL
LOGIC
365