RUS  ENG JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB
General information
Latest issue
Archive
Impact factor

Search papers
Search references

RSS
Latest issue
Current issues
Archive issues
What is RSS



Model. Anal. Inform. Sist.:
Year:
Volume:
Issue:
Page:
Find






Personal entry:
Login:
Password:
Save password
Enter
Forgotten password?
Register


Model. Anal. Inform. Sist., 2016, Volume 23, Number 6, Pages 703–714 (Mi mais534)  

An approach to verification of a family of multiagent systems for conflict resolution

N. O. Garanina, E. A. Sidorova

A.P. Ershov Institute of Informatics Systems, SB RAS, 6 Acad. Lavrentjev pr., Novosibirsk 630090, Russia

Abstract: 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.

Funding Agency Grant Number
Russian Foundation for Basic Research 15-07-04144_
Siberian Branch of Russian Academy of Sciences 15/10
The research has been supported by Russian Foundation for Basic Research (grant 15-07-04144) and Siberian Branch of Russian Academy of Science (Integration Grant n.15/10 Mathematical and Methodological Aspects of Intellectual Information Systems).


DOI: https://doi.org/10.18255/1818-1015-2016-6-703-714

Full text: PDF file (547 kB)
References: PDF file   HTML file

Bibliographic databases:

UDC: 004.052, 519.179.2
Received: 13.03.2016

Citation: N. O. Garanina, E. A. Sidorova, “An approach to verification of a family of multiagent systems for conflict resolution”, Model. Anal. Inform. Sist., 23:6 (2016), 703–714

Citation in format AMSBIB
\Bibitem{GarSid16}
\by N.~O.~Garanina, E.~A.~Sidorova
\paper An approach to verification of a family of multiagent systems for conflict resolution
\jour Model. Anal. Inform. Sist.
\yr 2016
\vol 23
\issue 6
\pages 703--714
\mathnet{http://mi.mathnet.ru/mais534}
\crossref{https://doi.org/10.18255/1818-1015-2016-6-703-714}
\mathscinet{http://www.ams.org/mathscinet-getitem?mr=3596155}
\elib{http://elibrary.ru/item.asp?id=27517417}


Linking options:
  • http://mi.mathnet.ru/eng/mais534
  • http://mi.mathnet.ru/eng/mais/v23/i6/p703

    SHARE: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles
  • Number of views:
    This page:81
    Full text:29
    References:11

     
    Contact us:
     Terms of Use  Registration  Logotypes © Steklov Mathematical Institute RAS, 2020