An Approach to Model Checking of Multi-agent Data Analysis
Natalia Garanina (A.P. Ershov Institute of Informatics Systems,, Novosibirsk, Russia), Eugene Bodin (A.P. Ershov Institute of Informatics, Systems, Novosibirsk, Russia), Elena Sidorova (A.P. Ershov Institute of, Informatics Systems, Novosibirsk, Russia)
TL;DR
This paper introduces a method for verifying multi-agent data analysis algorithms using model checking, translating agent protocols into Promela and properties into LTL, validated through experiments with SPIN.
Contribution
It presents a novel approach to verify multi-agent data analysis systems by modeling them with finite integer models and applying SPIN model checker.
Findings
Successful verification of multi-agent protocols using SPIN
Effective modeling of multi-agent systems with finite integer models
Demonstrated feasibility through experimental validation
Abstract
The paper presents an approach to verification of a multi-agent data analysis algorithm. We base correct simulation of the multi-agent system by a finite integer model. For verification we use model checking tool SPIN. Protocols of agents are written in Promela language and properties of the multi-agent data analysis system are expressed in logic LTL. We run several experiments with SPIN and the model.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsMobile Agent-Based Network Management · Multi-Agent Systems and Negotiation · Network Security and Intrusion Detection