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)

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.

In Marcello Maria Bersani, Davide Bresolin, Luca Ferrucci and Manuel Mazzara: Proceedings First Workshop on Logics and Model-checking for Self-* Systems (MOD* 2014), Bertinoro, Italy, 12th September 2014, Electronic Proceedings in Theoretical Computer Science 168, pp. 32–44.
Published: 13th November 2014.

ArXived at: http://dx.doi.org/10.4204/EPTCS.168.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org