An Approach to Verification of a Family of Multi- agent Systems for Conflict Resolution
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 sp...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2016-12-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/408 |
| _version_ | 1797877888557514752 |
|---|---|
| author | N. O. Garanina E. A. Sidorova |
| author_facet | N. O. Garanina E. A. Sidorova |
| author_sort | N. O. Garanina |
| collection | DOAJ |
| description | 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 ∀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. |
| first_indexed | 2024-04-10T02:24:12Z |
| format | Article |
| id | doaj.art-97e21b0835864362a79767e9288fb11f |
| institution | Directory Open Access Journal |
| issn | 1818-1015 2313-5417 |
| language | English |
| last_indexed | 2024-04-10T02:24:12Z |
| publishDate | 2016-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-97e21b0835864362a79767e9288fb11f2023-03-13T08:07:34ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172016-12-0123670371410.18255/1818-1015-2016-6-703-714337An Approach to Verification of a Family of Multi- agent Systems for Conflict ResolutionN. O. Garanina0E. A. Sidorova1Институт систем информатики им. А.П. Ершова СО РАНИнститут систем информатики им. А.П. Ершова СО РАН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 ∀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.https://www.mais-journal.ru/jour/article/view/408проверка моделейконтекстно-зависимая сетевая грамматикамультиагентные системыабстракция |
| spellingShingle | N. O. Garanina E. A. Sidorova An Approach to Verification of a Family of Multi- agent Systems for Conflict Resolution Моделирование и анализ информационных систем проверка моделей контекстно-зависимая сетевая грамматика мультиагентные системы абстракция |
| title | An Approach to Verification of a Family of Multi- agent Systems for Conflict Resolution |
| title_full | An Approach to Verification of a Family of Multi- agent Systems for Conflict Resolution |
| title_fullStr | An Approach to Verification of a Family of Multi- agent Systems for Conflict Resolution |
| title_full_unstemmed | An Approach to Verification of a Family of Multi- agent Systems for Conflict Resolution |
| title_short | An Approach to Verification of a Family of Multi- agent Systems for Conflict Resolution |
| title_sort | approach to verification of a family of multi agent systems for conflict resolution |
| topic | проверка моделей контекстно-зависимая сетевая грамматика мультиагентные системы абстракция |
| url | https://www.mais-journal.ru/jour/article/view/408 |
| work_keys_str_mv | AT nogaranina anapproachtoverificationofafamilyofmultiagentsystemsforconflictresolution AT easidorova anapproachtoverificationofafamilyofmultiagentsystemsforconflictresolution AT nogaranina approachtoverificationofafamilyofmultiagentsystemsforconflictresolution AT easidorova approachtoverificationofafamilyofmultiagentsystemsforconflictresolution |