An approach to verification of a family of multiagent systems for conflict resolution
Modelirovanie i analiz informacionnyh sistem, Tome 23 (2016) no. 6, pp. 703-714.

Voir la notice de l'article provenant de la source Math-Net.Ru

In the paper, we describe a verification method for families of distributed systems generated by context-sensitive network grammar of a special kind. This grammar includes special non-terminal symbols, so called quasi-terminals, which uniquely correspond to grammar terminals. These quasi-terminals specify processes which are merging of base system processes, in contrast to simple nonterminals which specify networks of parallel compositions of the processes. The method is based on model checking technique and abstraction. An abstract representative model for a family of systems depends on their specification grammar and system properties to be verified. This model simulates the behaviour of the systems in such a way that the properties which hold for the representative model are satisfied for all these systems. The properties of the representative model can be verified by model checking method. The properties of a generated system are specified by universal branching time logic $\forall CTL$ with finite deterministic automata as atomic formulas. We show the use of this method for verification of some properties of a multiagent system for conflict resolution, in particular, for context-dependent disambiguation in ontology population. We also suggest that this approach should be used for verification of computations on sub-grids which are sub-graphs of computation grids. In particular, we consider the computation of parity of the active processes number in a sub-grid.
Keywords: model checking, context-sensitive network grammar, multi-agent systems, abstractions.
@article{MAIS_2016_23_6_a2,
     author = {N. O. Garanina and E. A. Sidorova},
     title = {An approach to verification of a family of multiagent systems for conflict resolution},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {703--714},
     publisher = {mathdoc},
     volume = {23},
     number = {6},
     year = {2016},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2016_23_6_a2/}
}
TY  - JOUR
AU  - N. O. Garanina
AU  - E. A. Sidorova
TI  - An approach to verification of a family of multiagent systems for conflict resolution
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2016
SP  - 703
EP  - 714
VL  - 23
IS  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2016_23_6_a2/
LA  - ru
ID  - MAIS_2016_23_6_a2
ER  - 
%0 Journal Article
%A N. O. Garanina
%A E. A. Sidorova
%T An approach to verification of a family of multiagent systems for conflict resolution
%J Modelirovanie i analiz informacionnyh sistem
%D 2016
%P 703-714
%V 23
%N 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2016_23_6_a2/
%G ru
%F MAIS_2016_23_6_a2
N. O. Garanina; E. A. Sidorova. An approach to verification of a family of multiagent systems for conflict resolution. Modelirovanie i analiz informacionnyh sistem, Tome 23 (2016) no. 6, pp. 703-714. http://geodesic.mathdoc.fr/item/MAIS_2016_23_6_a2/

[1] Bergenti F., Franchi E., Poggi A., “Selected models for agent-based simulation of social networks”, Proc. of 3rd Symposium on Social Networks and Multiagent Systems, SNAMAS 2011, 2011, 27–32

[2] Clarke E. M., Grumberg O., Jha S., “Verifying Parameterized Networks”, ACM Transactions on Programming Languages and Systems, 19:5 (1997), 726–750 | DOI

[3] Clarke E. M., Grumberg O., Peled D., Model Checking, MIT Press, 1999

[4] Dassow J., “Grammars With Regulated Rewriting”, Formal Languages and Applications, Studies in Fuzziness and Soft Computing, 148, 2004, 249–273 | DOI | MR | Zbl

[5] De Gennaro M. C., Jadbabaie A., “Decentralized Control of Connectivity for Multi-Agent Systems”, Proc. of 45th IEEE Conference on Decision and Control, 2006, 3628–3633 | DOI

[6] Fagin R., Halpern J. Y., Moses Y., Vardi M. Y., Reasoning about Knowledge, MIT Press, 1995 | MR | Zbl

[7] Garanina N. O., Sidorova E .A., “Ontology Population as Algebraic Information System Processing Based on Multi-agent Natural Language Text Analysis Algorithms”, Programming and Computer Software, 41:3 (2015), 140–148 | DOI | MR | Zbl

[8] Garanina N., Sidorova E., “An Approach to Ambiguity Resolution for Ontology Population”, Proc. of 24th International Workshop on Concurrency, Specification, and Programming, (CS 2015) (Rzeszow, Poland, 2015, Sep. 28–30), v. 1, 2015, 27–32

[9] Garanina N. O., Sidorova E. A., Anokhin S. A., “Conflict Resolution in Multi-agent Systems with Typed Connections for Ontology Population”, Perspectives of System Informatics, Lecture Notes in Computer Science, 9609, 2016, 116–129 | DOI | Zbl

[10] Hopcroft J. E., Ullman J. D., Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, 1979 | MR | Zbl

[11] Huhns M. N., Stephens L. M., “Multiagent Systems and Societies of Agents”, Multiagent Systems: A Modern Approach to Distributed Artificial Intelligence, MIT Press, 1999, 79–120

[12] Tel G., Introduction to Distributed Algorithms, Cambridge University Press, 2000 | MR | Zbl

[13] Wooldridge M., An Introduction to Multiagent Systems, Willey Ltd, 2002