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

Автором была разработана программная система VMASTER, предназначенная для моделирования и верификации ВМАС. VMASTER включает в себя подсистемы:

• 1. Редактор ВМАС (рис. 1), который позволяет создавать и редактировать программы агентов и функции вероятностей каналов связи. Описание ВМАС можно сохранять в формате xml.
• 2. Интерпретатор ВМАС, позволяющий выполнять заданное число шагов работы ВМАС.

Рис. 1. Редактор ВМАС

• 3. Транслятор ВМАС, транслирующий ВМАС в цепь Маркова для дальнейшей верификации. Значения переменных на состояниях цепи Маркова, а также матрица переходов хранится в некотором компактном виде. Цепи Маркова можно сохранять и загружать.
• 4. Верификатор цепи Маркова (рис. 2), построенной по ВМАС.

Рис. 2. Верификатор ВМАС

Реализовано 5 видов верификации:

• 1) CY — верификация формулы логики PTL алгоритмом из статьи [Courcoubetis et al., 1995] с некоторыми добавлениями. Кроме стандартных темпоральных операторов X и U добавлены операторы:
  • а) X (k, f) — оператор, эквивалентный X^k(f).
  • б) X_OR (k, f) — оператор, эквивалентный X (f) Ъ X²(f) Ъ … Ъ X^k(f).
  • в) X_AND (k, f) — оператор, эквивалентный X (f) Щ X²(f) Щ … Щ X^k(f).

k? 1 — целое число.

При верификации формул операторы X (k, f), X_OR (k, f) и X_AND (k, f) не раскрываются в соответствии с эквивалентностями (а), (б), (в), а обрабатываются более быстрым алгоритмом, линейным от k.

• 2) k-find — поиск минимального числа шагов k, ровно через которое или за которое заданная формула f логики PTL будет выполняться с заданной вероятностью. Заданная формула f верифицируется алгоритмом из [Courcoubetis et al., 1995], а число шагов k находится специально разработанным алгоритмом за линейное время от k. 3) GTP — верификация формулы ограниченной логики PTL. Для этого случая автором разработан алгоритм полиномиальной сложности от размера формулы и размера цепи Маркова. Он строит по цепи Маркова некоторый специальный граф, который позволяет получить все траектории, на которых истинна верифицируемая формула, и определить вероятность ее истинности.
• 4) CY+GTP — верификация с совместным использованием CY и GTP.
• 5) PCTL — верификация формул расширенной логики PCTL с помощью обобщённого алгоритма верификации.

Система VMASTER предоставляет следующие дополнительные возможности:

• 1) Возможность просмотра графа состояний ВМАС и переходов между ними.
• 2) После верификации CY помимо вероятности есть возможность просмотреть те траектории графа состояний ВМАС, на которых истинна заданная формула верификации.
• 3) Возможность представления информации о небольших цепях Маркова графически.
• 4) Возможность представления специального графа из верификации GTP графически.
• 5) Вывод всех значений параметров на состояниях ВМАС.

Эксперименты, проведенные с системой VMASTER, показали, что она достаточно успешно справляется с верификацией формул. В табл. 1 представлены результаты верификации некоторых темпоральных формул различными алгоритмами. Верифицируемая цепь Маркова имеет указанное в третьем столбце число состояний, 5 случайных переходов из каждого состояния, одно начальное состояние и случайные значения переменных на состояниях. Время верификации приводится в секундах.

Табл. 1.

Благодарности. Работа выполнена при финансовой поддержке РФФИ (проект № 10−01−532а). Автор благодарен М. И. Дехтярю и М. К. Валиеву за помощь в работе.