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

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

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

Лебедев П. В., студент

Тверской государственный университет

e-mail: leb_87_@mail.ru



ВВЕДЕНИЕ

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

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



ЛОГИКА ДЛЯ СВОЙСТВ ВЕРОЯТНОСТНЫХ МНОГОАГЕНТНЫХ СИСТЕМ

Для описания свойств ВМАС мы используем известную темпоральную логику линейного времени PTL (Propositional Temporal Logic) [7, 8]. Формулы PTL описывают свойства деревьев вычислений. Такое дерево образуется за счёт выделения некоторого состояния в модели Крипке в качестве начального состояния и последующей развёртки модели в бесконечное дерево с корнем в выделенном состоянии.

Формулы PTL строятся из булевых и темпоральных операторов.

Имеются два основных темпоральных оператора:

· Оператор сдвига по времени X (neXttime, «в следующий момент») требует, чтобы свойство соблюдалось во втором состоянии пути.

· Оператор условного ожидания pUq (Until, «до тех пор пока») выполняется, если на пути имеется состояние, в котором выполняется второе свойство q, и при этом все предшествующие состояния обладают первым свойством p.

Стандартная интерпретация формулы PTL задается на парах <траектория, состояние>, и формула считается истинной на траектории, если она истинна в начальном состоянии этой траектории.

Добавим в логику PTL новый темпоральный оператор X[k], где k - натуральное число. Содержательно, X[k] f означает, что свойство f выполнится на одном из следующих k шагов. При k = 1 X[1] f = X f.

Вообще говоря, в общем случае этот оператор выражается через обычные операторы PTL таким образом:

X[k]f ?

Определим вероятность формулы PTL на цепи Маркова. Пусть M - конечная цепь Маркова, p(s, s') - вероятность перехода из состояния s в состояние s'. Через X_n(s₀) обозначим множество всех путей в цепи М длины n, начинающихся в состоянии s₀. Пусть X = X_n(s₀) , Вероятность этого пути равна P(X) = Будем говорить, что f истинна на X , если она истинна на любой траектории, имеющей префикс X, т.е. на траекториях, продолжающих X. Тогда вероятность формулы f на M равна:

Наш алгоритм верификации основан на алгоритме из работы [6], который поочередно устраняет темпоральные операторы из верифицируемой формулы PTL, увеличивая при этом размер цепи Маркова M.

Теорема 1. Алгоритм из [6] можно без увеличения временной сложности распространить на PTL+ X[k] . При этом вероятность формул вида X[k] f вычисляется за время O(|M|•k), а размер цепи изменяется так же, как и при обработке обычного оператора X.

В то же время, например, формула вычисляется стандартным алгоритмом из [6] за время O(|M|•2^k), и количество состояний в построенной новой цепи Маркова после выполнения этой последовательности операторов может быть в 2^k раз больше, чем первоначальное. верификация вероятностный многоагентный почтовый

ВЕРОЯТНОСТНАЯ МНОГОАГЕНТНАЯ СИСТЕМА

Вероятностная многоагентная система (ВМАС) состоит из интеллектуальных агентов {a₁, … , a_N}. Каждый агент а_i имеет набор параметров (переменных) {x₁, …, x_ki}, набор посылаемых сообщений {msgⁱ₁, …, msgⁱ_ri} и программу, управляющую его работой. Предполагается, что наборы сообщений, посылаемых различными агентами, не пересекаются.

Для каждой пары агентов а_i, а_j есть канал связи CH[i, j], хранящий сообщения, отправленные от а_i агенту а_j: CH[i, j] = {(t₁, msg₁),…,(t_k,msg_k)}, где в паре (t_i, msg_r) msg_r - имя отправленного агентом a_i сообщения, t_i - время нахождения сообщения msg_r в канале связи (т.е. количество шагов, прошедшее с момента отправки сообщения через канал связи). Для каждого канала CH[i, j] задана дискретная функция распределение вероятностей:

P[i, j]: P[i, j](t)

Это вероятность того, что сообщение будет передано агенту a_j за не более чем t шагов. В случае P[i, j](1) = 1 для всех пар агентов, все сообщения будут передаваться ровно за один шаг работы системы. Для того чтобы все сообщения доходили до получателя, последней вероятностью в списке P[i, j](t) должна быть единица. Если эта вероятность меньше единицы, то возможна потеря сообщений.

У каждого агента есть вероятностная программа, способная изменять значения переменных и посылать сообщения другим агентам. Она состоит из набора групп событий {G₁, …, G_r}. Каждая группа G имеет входное условие, а также содержит некоторый список процедур {P₁, … ,P_s}. Каждая процедура имеет вероятность выполнения, а также пару объектов: (Operators, Messages). Operators представляют список операторов программы вида:

<Условие> <Переменная>= <Присваиваемое выражение>,

где «Условие» и «Присваиваемое выражение» являются обычными логическими и арифметическими выражениями, над переменными и целыми константами.

Объект Messages является списком отправляемых сообщений вида:



<Условие> <Имя агента-получателя> <Имя сообщения>.

Назовём глобальным состоянием системы набор

(,…, ,…,,…,)}

Здесь x_ij - значение j-ого параметра агента a_i, msg_ij - j-е сообщение агента a_i, полученное на текущем шаге, CH[i, j] - состояние соответствующего канала связи.

Шаг системы означает переход из одного глобального состояния в другое. Для простоты записи пусть глобальное состояние имеет вид

,

где - переменные всех агентов, - сообщения всех агентов. Начальное состояние имеет вид:

(0,…,0),…,(0,…,0),(,…, )},

Алгоритм выполнения одного шага системой:

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

Для i= 1, … , q выполняем: m_i := 0;

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

Для i, j = 1, … , N и (t, msg) CH[i, j] выполняем: t := t+1;

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

Для i, j = 1, …, N и (t, msg) CH[i, j] по порядку с вероятностью

P[i, j](t) выполняем следующие действия:

А) Удаляем сообщение из канала связи:

CH[i, j] := CH[i, j] \ (t, msg)

Б) Пополняем почтовый ящик: m_msg := m_msg + 1;

В) Если P[i, j](t) - последний элемент списка P[i, j] и P[i, j](t) < 1 и сообщение не послано агенту, то удаляем сообщение (т.к. происходит потеря информации): CH [i, j] := CH[i, j] \ (t, msg).

4) Вычисление условий групп событий агентов.

Для каждого агента a_i и для каждой группы событий G_j агента a_i вычисляем условие группы событий G_j над переменными глобального состояния:

e[i][j] := Calculate(«Условие входа Gj»), где Calculate(expression) - вычисление значения выражения expression на текущем состоянии.

5) Вычисление групп событий.

Пусть Gj - группа событий агента ai , для которой e[i][j] ? 0.

Для каждой такой группы выполняем одну из её процедур P_k c заданной для неё вероятностью входа.

6) Выполнение процедуры. Выполнение операторов.

Операторы выполняются последовательно по расположению в списке. Оператор («Условие» «Переменная» «Присваиваемое выражение») выполняется таким образом:

IF Calculate(«Условие») = true THEN

x[«Переменная»] := Calculate(«Присваиваемое выражение»)

Отправка сообщений.

Сообщения отправляются последовательно по расположению в списке. Сообщение («Условие» «Имя агента» «Имя сообщения») обрабатывается таким образом:

IF Calculate(Условие) = true THEN

CH[i,«Имя агента»] := CH[i, «Имя агента»] (0, «Имя сообщения»).

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

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

Для верификации ВМАС необходимо получить её представление в виде цепи Маркова. В работе построен алгоритм TranslateMarkovChain, который по данным, задающим ВМАС A, строит эквивалентную цепь Маркова M_A. Мы приведем содержательное описание этого алгоритма. Входными данными алгоритма TranslateMarkovChain являются: описание ВМАС, включающее параметры, сообщения и программы всех агентов системы и вероятностные распределения для каналов связи, набор возможных начальных состояний S₁, …, S_s с распределением вероятностей на них: p₀₁,…,p_0s. Результатом работы алгоритма TranslateMarkovChain является цепь Маркова, состояния которой соответствуют состояниям входной ВМАС, и для каждого состояния цепи указан список исходящих дуг с вероятностями переходов по ним.

Алгоритм использует следующие внутренние структуры данных:

Q - очередь для хранения расширенных состояний, для которых ещё не находились переходы в другие состояния.

GlobalStates - упорядоченный список всех найденных состояний.

q.probability - вероятность перехода в состояние q из текущего.

OldStates, NewStates - упорядоченные списки, хранящие состояния, получающиеся за один шаг из текущего.

Алгоритм TranslateMarkovChain

1) Заполняем начальное распределение цепи Маркова:

P0 = {p01,…,p0s}.

2) Добавляем начальные состояния в очередь Q.

3) Пока очередь Q не пуста, выполняем шаги 4-11:

4) Выбираем текущее состояние C0 из очереди Q, помещаем его в список текущих состояний NewStates и помечаем его вероятность С.probability := 1.

5) Опустошаем почтовые ящики для C: m_i := 0 для всех i=1,…,q.

6) Увеличиваем время хранения сообщений в каналах связи CHij={t,msg} на единицу для С: CH_ij:= {t+1,msg} для всех i, j.

7) Получение сообщений агентами с вероятностью: для каждого текущего состояния C из NewStates и для каждого агента вычисляются два состояния C1 и С2: C1 - если сообщение будет доставлено, C2 - если сообщение не будет доставлено, и вычисляется вероятность этих состояний: C1.probability := C.probability * pCH[i,j](t), C2.probability := C1.probability * (1-pCH[I,j](t)). После чего C1 и C2 помещаются в отсортированный список NewStates вместо C.

8) Выполнение программы с вероятностью: для каждого текущего состояния C из NewStates, для каждого агента и для каждой группы событий G вычисляются состояния C1,…,Ck, где Ci - состояние, полученное из C путём выполнения процедуры Proci из группы событий G, и вычисляется вероятность каждого такого состояния: Сi .probability := C.probability * Probi , где Probi - вероятность входа в процедуру Proci. После этого C1,…,Ck помещаются в NewStates вместо C.

9) Если в список NewStates попали два одинаковых состояния, то оставляем одно из них, а вероятность обоих складываем.

10) Для каждого состояния C, находящегося в NewStates, добавляем переход в цепь Маркова с вероятностью P(С0, С) = С.probability. Если состояние С ещё не встречалось в списке GlobalStates, то добавляем его в этот список и в очередь Q, а также в список состояний марковской цепи.

11) Продолжаем цикл, переходя к шагу 3.

Пусть с - число констант, используемых в описании системы, p максимальное число параметров у агента, m - число различных сообщений и n - число агентов системы. Тогда прямой подсчет показывает, что число всех глобальных состояний системы |S|(c^p2^m)ⁿ.

Теорема 2. Алгоритм TranslateMarkovChain по ВМАС A строит эквивалентную цепь Маркова M_A за время O(|S|²log |S|), где S - множество всех глобальных состояний A.

ЭКСПЕРИМЕНТАЛЬНОЕ ИССЛЕДОВАНИЕ

Указанные выше алгоритмы были реализованы в программе PMASVerification, которая содержит следующие основные компоненты:

· Редактор ВМАС позволяет задавать и редактировать все данные, задающие ВМАС.

· Транслятор ВМАС в цепь Маркова реализует алгоритм TranslateMarkovChain.

· Редактор формул темпоральной логики позволяет вводить и редактировать формулы, задающие проверяемые свойства ВМАС.

· Верификатор реализует алгоритм вычисления вероятностей формул PTL+ X[k].

Ниже в таблицах представлены некоторые результаты экспериментов с программой PMASVerification. Определялось время работы в мсек программы верификации цепи Маркова в зависимости от сложности верифицируемой формулы, числа состояний цепи и процента количества дуг в среднем из одного состояния по отношению к общему числу состояний (например, если в таблице указано 10% процентов дуг, а всего состояний 1000, то из каждого состояния в среднем выходит 100 дуг). Вероятности переходов и начальное распределение, а также значения пропозициональных переменных на состояниях задавались случайно. Верифицируемые формулы имеют вид:

· (x1 U x2)

· (x1 U x2) & (x3 U x4)

· (x1 U x2) & (x3 U x4) & (x5 U x6)

· X x1

· X x1 & X x2

· X x1 & X x2 & X x3

Начнем со сравнения времени вычисления оператора X[3] с его аналогом, выраженным через оператор X.

Табл. 1. Формулы с оператором X[k] (1% дуг)

Состояния	X[3](x1)	XXX(x1) v XX(x1) v X(x1)
1000	2	344
3000	78	2734
5000	219	6250
8000	625	13969

Таблица 1 показывает, что использование оператора X[k] существенно сокращает время вычисления.



Табл. 2. Формулы с оператором U (1% дуг)

Состояния	1 оператор	2 оператора	3 оператора
1000	31	94	140
2000	531	1875	4687
3000	3125	9672	15406
5000	20515	59500	121765

Табл. 3. Формулы с оператором X (1% дуг)

Состояния	1 оператор	2 оператора	3 оператора
1000	15	31	63
2000	32	94	297
3000	63	203	609
5000	203	593	1422

Табл. 4. Формулы с оператором U (10% дуг)

Состояния	1 оператор	2 оператора	3 оператора
1000	219	625	1234
2000	2250	5329	10968
3000	5532	20110	37937
5000	29656	89797	170047

Табл. 5. Формулы с оператором X (10% дуг)

Состояния	1 оператор	2 оператора	3 оператора
1000	47	141	596
2000	219	547	1468
3000	532	1344	3234
5000	1313	3547	9125

Таблицы 2 - 5 показывают, что формулы, содержащие только X, верифицируются существенно быстрее формул с тем же числом операторов U, но во всех случаях усложнение формулы приводит к быстрому (теоретически экспоненциальному) росту времени ее верификации. Увеличение «плотности» цепи Маркова также приводит к почти линейному росту времени верификации.

Благодарности

Автор благодарен М.И. Дехтярю за постановку задачи и внимание к работе и М.К. Валиеву за полезные замечания.



ЛИТЕРАТУРА

1. Тарасов В.Б. От многоагентных систем к интеллектуальным организациям. - М.: Эдиториал УРСС, 2002.

2. Dekhtyar M.I., Dikovsky A.Ja., Valiev M.K. Temporal Verification of Probabilistic Multi-Agent Systems// Pillars of Computer Science: Essays Dedicated to Boris (Boaz)Trakhtenbrot on the Occasion of His 85th Birthday. Lecture Notes in Computer Science, №4800. - Berlin: Springer, 2008. - P.256-265.

3. Валиев М.К., Дехтярь М.И., Диковский А.Я. О свойствах многоагентных систем с вероятностными каналами связи// Интегрированные модели и мягкие вычисления в искусственном интеллекте. Труды IV-ой Международной научно-практической конференции (Коломна, 28-30 мая 2007 г.). - М.: Физматлит, 2007. - С.119-126.

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

5. Dix J., Nanni M., and Subrahmanian V. S. Probabilistic Agent Reasoning// ACM Transactions of Computational Logic. - 2000. - Vol.1, №2. - P.201-245.

6. Courcoubetis C., Yannakakis M. The Complexity of Probabilistic Verification // Communications of ACM. - 1995. - Vol.42, №4. - P.857-907.

7. Baier C., Katoen J. Principles of Model Checking.- Cambridge MA: MIT Press, 2008.

8. Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. - М.: МЦНМО, 2002.

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

...