Verification of Cooperative Multi-Agent Negotiation with Alloy Analyzer




Podorozhny, Rodion
Khurshid, Sarfraz
Perry, Dewayne
Zhang, Shelley Xiaoqin

Journal Title

Journal ISSN

Volume Title



Multi-agent systems provide an increasingly popular solution in problem domains that require management of uncertainty and high degree of adaptability. Robustness is a key design criteria in building multi-agent systems. We present a novel approach for the design of robust multi-agent systems. Our approach constructs a model of the design of a multi-agent system in Alloy, a declarative language based on relations, and checks the properties of the model using the Alloy Analyzer, a fully automatic analysis tool for Alloy models. While several prior techniques exist for checking properties of multi-agent systems, the novelty of our work is that we can check properties of coordination and interaction, as well as properties of complex data structures that the agents may internally be manipulating or even sharing. The suggested work is the first application of Alloy to checking properties of multi-agent systems. Such unified analysis has not been possible before.



verification, software, multi-agent negotiation, alloy analyzer, multi-agent systems, alloy models, Computer Science


Podorozhny, R., Khurshid, S., Perry, D., & Zhang, S. (2006). Verification of cooperative multi-agent negotiation with Alloy Analyzer (Report No. TXSTATE-CS-TR-2006-4). Texas State University-San Marcos, Department of Computer Science.


Rights Holder

Rights License

Rights URI