SYMBOLIC VERIFICATION OF A STRENGTH BASED MULTI-AGENT ARGUMENTATION SCHEME

Software systems have evolved to the age of Artificial Intelligence (AI), consist- ing of independentautonomous agents interacting with each other in dynamic and unpredictable environments. In this kindof environment it is often very difficult to predict all the interactions between the agents. Henceverification of an interaction between multiple agents has become a key research area in AI. In this paperwe model and verify an Automatic Meeting Scheduling (AMS) problem having multiple agentcommunication. The AMS problem helps us to emulate a real life scenario where multiple agents can argue over thedefined constraints. A weighted strength based argu- mentation scheme is proposed, where eachargument is weighed against each other to determine the strongest evidence. The argumentation modeldescribed in the paper have six agents: Initiator, Scheduler and four Participant agents. We haveformalized the agent interactions using Computation Tree Logic (CTL) and verified the scheme byproviding suitable specifications (SPEC) in a symbolic model verifier tool called, NuSMV.