An Approach to Veriﬁcation of a Family of Multi- agent Systems for Conﬂict Resolution - N. O. Garanina; E. A. Sidorova (Моделирование и анализ информационных систем, 2016)
In the paper, we describe a veriﬁcation 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 speciﬁcation grammar and system properties to be veriﬁed. This model simulates the behaviour of the systems in such a way that the properties which hold for the representative model are satisﬁed for all these systems. The properties of the representative model can be veriﬁed by model checking method. The properties of a generated system are speciﬁed by universal branching time logic ∀CTL with ﬁnite deterministic automata as atomic formulas. We show the use of this method for veriﬁcation of some properties of a multiagent system for conﬂict resolution, in particular, for context-dependent disambiguation in ontology population. We also suggest that this approach should be used for veriﬁcation 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.