Введение. 
Программа верификации вероятностных многоагентных систем

Данная статья посвящена описанию программной системы VMASTER, предназначенной для разработки и верификации вероятностных многоагентных систем. Интеллектуальные агенты таких систем используют стохастичность в программе выполнения действий на каждом шаге работы, также ненадёжными могут быть почтовые системы передачи сообщений между агентами. Такие системы могут моделироваться конечными цепями Маркова.

Основной подход к их верификации основан на так называемом методе проверки на моделях, который широко используется в настоящее время для верификации моделей с детерминированными и недетерминированными переходами. Верификация — это проверка (или вычисление вероятности) выполнимости некоторого свойства модели.

При этом подходе спецификации свойств поведения ВМАС представляются формулами различных темпоральных логик.

Для верификации ВМАС в работах [Валиев и др., 2008], [Dekhtyar et al., 2008] было показано, как проблема верификации ВМАС в архитектуре IMPACT [Subrahmanian et al., 2000] может быть сведена к верификации конечных цепей Маркова. Некоторые другие подходы к верификации ВМАС рассматривались в работе [Kwiatkowska, 2003] .

Рассматриваемая ниже программная система VMASTER позволяет создавать и редактировать ВМАС, пошагово моделировать их работу и верифицировать созданные системы. Мы кратко описываем архитектуру и язык, даём определения нескольких темпоральных логик, и описываем возможности системы VMASTER по верификации ВМАС, а также несколько режимов верификации.