TY - GEN
T1 - Logical modeling and verification of a strength based multi-agent argumentation scheme using NuSMV
AU - Shetty, Shravan
AU - Shashi Kiran, H. S.
AU - Namala, Murali Babu
AU - Singh, Sanjay
PY - 2011/12/1
Y1 - 2011/12/1
N2 - Software systems have evolved to the age of Artificial Intelligence (AI), consisting of independent autonomous agents interacting with each other in dynamic and unpredictable environments. In this kind of environment it is often very difficult to predict all the interactions between the agents. Hence verification of an interaction between multiple agents has become a key research area in AI. In this paper we model and verify an Automatic Meeting Scheduling (AMS) problem having multiple agent communication. The AMS problem helps us to emulate a real life scenario where multiple agents can argue over the defined constraints. A weighted strength based argumentation scheme is proposed, where each argument is weighed against each other to determine the strongest evidence. The argumentation model described in the paper have six agents: Initiator, Scheduler and four Participant agents. We have formalized the agent interactions using Computation Tree Logic (CTL) and verified the scheme by providing suitable specifications (SPEC) in a symbolic model verifier tool called, NuSMV.
AB - Software systems have evolved to the age of Artificial Intelligence (AI), consisting of independent autonomous agents interacting with each other in dynamic and unpredictable environments. In this kind of environment it is often very difficult to predict all the interactions between the agents. Hence verification of an interaction between multiple agents has become a key research area in AI. In this paper we model and verify an Automatic Meeting Scheduling (AMS) problem having multiple agent communication. The AMS problem helps us to emulate a real life scenario where multiple agents can argue over the defined constraints. A weighted strength based argumentation scheme is proposed, where each argument is weighed against each other to determine the strongest evidence. The argumentation model described in the paper have six agents: Initiator, Scheduler and four Participant agents. We have formalized the agent interactions using Computation Tree Logic (CTL) and verified the scheme by providing suitable specifications (SPEC) in a symbolic model verifier tool called, NuSMV.
UR - http://www.scopus.com/inward/record.url?scp=84874671574&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84874671574&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-17857-3_38
DO - 10.1007/978-3-642-17857-3_38
M3 - Conference contribution
AN - SCOPUS:84874671574
SN - 9783642178566
T3 - Communications in Computer and Information Science
SP - 378
EP - 387
BT - Advances in Computer Science and Information Technology - First International Conference on Computer Science and Information Technology, CCSIT 2011, Proceedings
T2 - 1st International Conference on Computer Science and Information Technology, CCSIT 2011
Y2 - 2 January 2011 through 4 January 2011
ER -