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

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


Смотрите также:
Верификация автоматных программ...
Реферат Отчёта по нир на тему: Разработка и внедрение автоматизированной информационной системы...
О. И. Федяев fedyaev@ dgtu donetsk ua...
Стеки сетевых протоколов...
Методы и модели анализа и оценки экологического риска: классификации...
Лекция Введение...
1. Спиральная модель проектирования вычислительных систем...
Лекция 5 Методы построения математических моделей асу...
Особенности реализации систем идентификации диктора...
2. Модель взаимодействия открытых систем Открытые системы и модель их взаимодействия...
05. 13. 15 Вычислительные машины, комплексы и компьютерные сети...
Программа государственного экзамена по направлению (магистерская подготовка)...



Загрузка...
МОДЕЛЬ ВЕРОЯТНОСТНЫХ МНОГОАГЕНТНЫХ СИСТЕМ И ИХ ВЕРИФИКАЦИЯ*


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

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

e-mail: leb_87_@mail.ru


1. ВВЕДЕНИЕ


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

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


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

Для описания свойств ВМАС мы используем известную темпоральную логику линейного времени 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’. Через Xn(s0) обозначим множество всех путей в цепи М длины n, начинающихся в состоянии s0. Пусть X =  Xn(s0) , Вероятность этого пути равна 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|∙2k), и количество состояний в построенной новой цепи Маркова после выполнения этой последовательности операторов может быть в 2k раз больше, чем первоначальное.

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

Вероятностная многоагентная система (ВМАС) состоит из интеллектуальных агентов {a1, … , aN}. Каждый агент аi имеет набор параметров (переменных) {x1, …, xki}, набор посылаемых сообщений {msgi1, …, msgiri} и программу, управляющую его работой. Предполагается, что наборы сообщений, посылаемых различными агентами, не пересекаются.

Для каждой пары агентов аi, аj есть канал связи CH[i, j], хранящий сообщения, отправленные от аi агенту аj: CH[i, j] = {(t1, msg1),…,(tk,msgk)}, где в паре (ti, msgr) msgr – имя отправленного агентом ai сообщения, ti – время нахождения сообщения msgr в канале связи (т.е. количество шагов, прошедшее с момента отправки сообщения через канал связи). Для каждого канала CH[i, j] задана дискретная функция распределение вероятностей:

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

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

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

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

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

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

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

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

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

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

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

,

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Для верификации ВМАС необходимо получить её представление в виде цепи Маркова. В работе построен алгоритм TranslateMarkovChain, который по данным, задающим ВМАС A, строит эквивалентную цепь Маркова MA. Мы приведем содержательное описание этого алгоритма. Входными данными алгоритма TranslateMarkovChain являются: описание ВМАС, включающее параметры, сообщения и программы всех агентов системы и вероятностные распределения для каналов связи, набор возможных начальных состояний S1, …, Ss с распределением вероятностей на них: p01,…,p0s. Результатом работы алгоритма TranslateMarkovChain является цепь Маркова, состояния которой соответствуют состояниям входной ВМАС, и для каждого состояния цепи указан список исходящих дуг с вероятностями переходов по ним.

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

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

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

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

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

Алгоритм TranslateMarkovChain

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

P0 = {p01,…,p0s}.

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

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

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

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

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

  6. Получение сообщений агентами с вероятностью: для каждого текущего состояния 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.

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

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

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

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

Пусть с – число констант, используемых в описании системы, p максимальное число параметров у агента, m – число различных сообщений и n – число агентов системы. Тогда прямой подсчет показывает, что число всех глобальных состояний системы |S|(cp2m)n.

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

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

Указанные выше алгоритмы были реализованы в программе 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.




*Эта работа выполнена при поддержке РФФИ гранты 07-01-00637 и 08-01-00241-а





Скачать 131.22 Kb.
оставить комментарий
Дата27.08.2012
Размер131.22 Kb.
ТипДокументы, Образовательные материалы
Добавить документ в свой блог или на сайт

Ваша оценка этого документа будет первой.
Ваша оценка:
Разместите кнопку на своём сайте или блоге:
rudocs.exdat.com

Загрузка...
База данных защищена авторским правом ©exdat 2000-2017
При копировании материала укажите ссылку
обратиться к администрации
Анализ
Справочники
Сценарии
Рефераты
Курсовые работы
Авторефераты
Программы
Методички
Документы
Понятия

опубликовать
Загрузка...
Документы

Рейтинг@Mail.ru
наверх