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

Размещено на http://www.allbest.ru/

ПРОГРАММА ВЕРИФИКАЦИИ ВЕРОЯТНОСТНЫХ МНОГОАГЕНТНЫХ СИСТЕМ

П.В. Лебедев Тверской государственный университет, Тверь

Аннотация

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

Введение

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

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

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

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

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

1. Архитектура ВМАС

Вероятностная многоагентная система A состоит из набора интеллектуальных агентов {A₁, … , A_N} и каналов связи между агентами CH[i, j]. У каждого агента A_i имеется набор параметров {x₁, … , x_m}, значения которых в каждый момент времени задают состояние агента. Кроме того, у него имеется почтовый ящик MsgBox_i, в котором содержатся сообщения, полученные им на текущем шаге от других агентов. Работа агента A_i определяется его управляющей вероятностной программой Pr_i, которая на каждом шаге в зависимости от значений параметров агента и состояния его почтового ящика может изменять значения параметров и посылать сообщения другим агентам.

Для каждой пары агентов есть каналы связи, хранящие сообщения, отправленные от одного агента другому. В канале связи CH[i, j] между агентами A_i и A_j хранится множество пар CH[i, j] = {(t₁, msg₁), …, (t_r, …, msg_r)}, где msg_l - сообщение, посланное агентом A_i агенту A_j t_l шагов назад.

Для каждого канала связи определена функция распределения вероятности доставки сообщения в течение заданного числа шагов. Для каждой пары агентов A_i и A_j через pCH[i, j](t) обозначим вероятность того, что сообщение от агента A_i будет доставлено агенту A_j в течении (t+1) шагов с момента отправки. В случае pCH[i, j](1)=1 для всех пар агентов, все сообщения будут передаваться ровно за два шага работы системы. Для того, чтобы все сообщения доходили до получателя, должно выполняться условие max_t pCH[i, j](t) = 1. Если это значение меньше единицы, то возможна потеря сообщений в каналах связи. Таким образом, состояние ВМАС - это состояние агентов и состояние каналов связи. Имеется некоторое начальное состояние ВМАС. Выполнение шага системы на состоянии:

1. Опустошение почтовых ящиков всех агентов.

2. Увеличение времени хранения всех сообщений в каналах связи на единицу.

3. Доставка сообщений с заданными вероятностями.

4. Выполнение программ агентов Pr₁, …, Pr_N.

Язык программ агентов системы представляет собой процедурный C-подобный язык с добавленной возможностью работы с агентами:

1) Типы данных: целое, вещественное, строка, массив, ссылка.

2) Константы.

3) Операции:

а) арифметические операции: +, -, *, /, ^;

б) операции сравнения: >, <, >=, <=, ==, != ;

в) логические операции: && (и), || (или), !(не);

г) операции преобразования типов;

д) операции для работы с массивами.

4) Оператор присваивания, условный оператор, оператор цикла.

5) Возможность объявления и вызова функций.

6) Возможность использования локальных переменных внутри функций.

7) Оператор отправки сообщения message(«A», «B», «msg»), который посылает от агента «A» агенту «B» сообщение «msg».

8) Вероятностный оператор random(p₁, …, p_m), возвращающий случайное число k = 1, …, m с вероятностью p_k.

Программа каждого агента имеет некоторую процедуру шага, которая выполняется на каждом шаге работы системы.

верификация вероятностный многоагентный логика

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

2.1 PTL

PTL (propositional temporal logic) - темпоральная логика линейного времени. Формулы PTL выражают свойства бесконечных траекторий графа состояний ВМАС:

Ф :: = true | a | Ф Щ Ф| Ф Ъ Ф | Ш Ф | X(Ф) | Ф U Ф

a - пропозициональная переменная.

X(Ф) - оператор Next. Требует, чтобы свойство Ф выполнялось во втором состоянии пути.

Ф₁ U Ф₂ - оператор Until. Оператор выполняется, если на пути имеется состояние, в котором соблюдается свойство Ф₂ и в каждом предшествующем состоянии этого пути соблюдается свойство Ф₁.

В статье [Courcoubetis et al., 1995] приводится алгоритм верификации для этой логики, имеющий полиномиальную сложность от размера модели и экспоненциальную сложность от размера формулы верификации.

2.2 Ограниченный PTL

Это подмножество PTL без оператора Until:

Ф :: = true | a | Ф Щ Ф| Ф Ъ Ф | Ш Ф | X(Ф)

Для ограниченного PTL автором разработан алгоритм верификации полиномиальной сложности от размера модели и размера формулы.

2.3 PCTL

PCTL (probabilistic computation tree logic) - темпоральная логика ветвящегося времени. Формулы PCTL выражают свойства деревьев вычислений:

Ф :: = true | a | Ф Щ Ф| Ф Ъ Ф | Ш Ф | [X(Ф)]_Кp | [Ф U Ф]_Кp

К--О { і, >}, p О [0; 1].

a - пропозициональная переменная.

[X(Ф)]_Кp - выполнено, если с вероятностью Кp на следующем состоянии выполнено Ф.

[Ф₁ U Ф₂]_--Кp - выполнено, если с вероятностью Кp существует путь, на некотором состоянии которого выполнено Ф₂, а на всех предшествующих состояниях этого пути выполнено Ф₁.

Для логики PCTL существует алгоритм верификации полиномиальной сложности от размера модели и размера формулы, представленный в [Hansson et al., 1994].

2.4 Расширенный PCTL

Мы расширяем PCTL, добавляя формулы следующего вида:

Ф :: = [X(k, Ф)]_--Кp | X^OR(k, Ф)]_--Кp | [X^AND(k, Ф)]_--Кp , (k ? 1, целое)

К--О { і, >}, p О [0; 1], k ? 1 - целое.

Эти формулы имеют следующий смысл:

[X(k, Ф)]_--Кp - выполнено, если с вероятностью Кp существует путь, ровно на k-ом состоянии которого выполнено Ф,

[X^OR(k, Ф)]_--Кp - выполнено, если с вероятностью Кp существует путь, для которого существует такое 1 ? i ? k, что на i-ом состоянии этого пути выполнено Ф,

[X^AND(k, Ф)]_--Кp - выполнено, если с вероятностью Кp существует путь, для которого для всех 1 ? i ? k на i-ом состоянии этого пути выполнено Ф.

Для расширенного PCTL в работе обобщен известный алгоритм верификации PCTL из [Hansson et al., 1994]. При этом сохранены его оценки сложности: он является полиномиальным от размера модели, размера формулы и максимального k.

3. Программа 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-00532а). Автор благодарен М. И. Дехтярю и М. К. Валиеву за помощь в работе.

Список литературы

[Валиев и др., 2008] Валиев М.К., Дехтярь М.И. Вероятностные мультиагентные системы: семантика и верификация. // Вестник Тверского государственного университета. Серия «Прикладная математика», 35(95), 4, 2008.

[Bianco et al., 1995] Bianco A., Alfaro L. Model checking of probabilistic and nondeterministic systems. In P. Thiagarajan, editor, Proc. 15^th Conference on Foundations of Software Technology and Theoretical 18 Computer Science, volume 1026 of LNCS. Springer, 1995.

[Courcoubetis et al., 1995] Courcoubetis C., Yannakakis M., The complexity of probabilistic verification. J. ACM, v. 42, 4, 1995.

[Dekhtyar et al., 2008] Dekhtyar M., Dikovsky A., Valiev M. Temporal Verification of Probabilistic Multi-Agent Systems. Pillars of Computer Science: Essays Dedicated to Boris (Boaz)Trakhtenbrot on the Occasion of His 85th Birthday LNCS, N 4800, 2008.

[Hansson et al., 1994] Hansson H., Jonsson B. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5), 1994.

[Kwiatkowska, 2003] Kwiatkowska Marta. Model checking for probability and time: from theory to practice. In Proc. 18th IEEE Symposium on Logic in Computer Science (LICS'03), IEEE Computer Society Press, 2003.

[Subrahmanian et al., 2000] Subrahmanian V. S., Bonatti P., Dix J., et al., Heterogeneous Agent Systems, MIT LPess, 2000.

Размещено на Allbest.ru