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

Настоящая работа посвящена вопросам реализации и верификации вероятностных многоагентных систем (ВМАС). В литературе описано уже достаточно много различных архитектур МАС [1]. Мы рассматриваем достаточно простую продукционную модель с вероятностной почтовой подсистемой и вероятностным выбором действий — упрощенный вариант ВМАС из работ [2−4]. В этих работах было показано, как проблема верификации ВМАС в архитектуре IMPACT [5] может быть сведена к верификации конечных цепей Маркова. В данной работе мы расширяем темпоральный язык PTL, введя в него формулы вида X[k] f, содержательно означающие, что формула f истинна по крайней мере на одном из k следующих состояний.

Введение

этого оператора позволяет существенно сократить естественные утверждения о поведении динамических систем. Мы модифицируем алгоритм верификации конечных цепей Маркова из [6] для этого расширенного языка. Использование модифицированного алгоритма позволяет существенно ускорить верификацию значительного класса содержательно интересных свойств систем.

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