An Approach to Model Checking of Multi-agent Data Analysis
This work addresses verification challenges for multi-agent systems in data analysis, but it appears incremental as it applies existing tools to a specific domain.
The paper tackles the problem of verifying multi-agent data analysis algorithms by modeling them as finite integer systems and using the SPIN model checker with Promela and LTL, reporting successful experiments.
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.