Подход к верификации семейства мультиагентных систем разрешения конфликтов

В данной работе мы описываем метод верификации для семейств распределенных систем, которые порождаются контекстно-зависимой сетевой грамматикой специального вида. Эта грамматика содержит специальные нетерминальные символы — квази-терминалы. Квази-терминалы однозначно соответствуют терминалам грамматики и могут задавать процессы, которые определяются слиянием базовых процессов системы, в то время как нетерминалы задают сети параллельных композиций этих процессов. Данный метод верификации основан на техниках верификации моделей и абстракции. Абстрактная репрезентативная модель семейства систем зависит от задающей их грамматики и верифицируемых свойств системы. Эта модель симулирует поведение заданных систем таким образом, что свойства, которые выполняются в репрезентативной модели, также выполняются и во всех заданных системах. Проверку свойств репрезентативной модели можно осуществлять с помощью метода проверки моделей. Свойства порождаемых систем специфицируются с помощью универсальной логики ветвящегося времени $\forall CTL$ с конечными детерминированными автоматами в качестве атомарных формул. Мы показываем, что предложенный метод верификации можно применять для проверки некоторых свойств мультиагентных систем разрешения конфликтов, в частности, систем разрешения неоднозначностей при пополнении онтологий. Также показано, что этот подход можно использовать для верификации вычислений на подрешетках, являющихся подграфами решеток вычислений, например, для вычисления четности числа работающих процессов.