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

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

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

Институт прикладной математики им. М.В.Келдыша РАН

О верификации свойств вероятностных мультиагентных систем Эта работа выполнена при поддержке РФФИ (гранты 07-01-00637-а и 05-01-01006-а).

Валиев М.К., к.ф.-м.н.

Введение

Настоящая работа является расширением нашей работы [6], в которой рассматривалась проблема верификации динамических свойств мультиагентных систем (МАС), состоящих из интеллектуальных агентов, которые взаимодействуют через вероятностные каналы связи. Расширение состоит в том, что здесь мы дополнительно допускаем, что действия агентов также могут быть вероятностными. Мы обобщаем конструкцию из [6], которая строит конечную марковскую цепь по МАС с вероятностными каналами связи, на эти более общие вероятностные МАС. Это позволяет применить (так же, как в [6]) к последним алгоритмы верификации конечных Марковских цепей из [2].

Вероятностные МАС

Имеются различные подходы к определению интеллектуальных агентов (см., например, [5,7]). Наши определения здесь в основном (с некоторыми упрощениями) следуют [5].

Мультиагентная система (МАС) A = {A1,...,An} состоит из конечного множества {A1,...,An} взаимодействующих интеллектуальных агентов Ai. У интеллектуального агента A имеется внутренняя база данных (БД) IA, содержащая конечное множество базисных атомов (т.е. выражений вида p(c1,…, ck), где p-предикатный символ, c1,…, ck - константы, причем множество используемых данной системой констант ограничено), и почтовый ящик MsgBoxA. Текущие содержимые внутренней БД и почтового ящика агента A составляют его текущее локальное состояние IMA=<IA,MsgBoxA>.

Агенты из A общаются между собой посредством передачи сообщений вида msg(Sender, Receiver, Msg), где Sender и Receiver - имена агентов (источника и адресата), a Msg - (передаваемый) базисный атом.

Для каждой пары агентов A, B из A имеется канал связи CHAB, в который попадают сообщения, посылаемые агентом A агенту B. Затем из этого канала они попадают в почтовый ящик MsgBoxB. Время пребывания каждого сообщения «в пути» мы будем рассматривать как случайную величину, задаваемую конечным дискретным распределением вероятностей. Через pAB(t) обозначим вероятность того, что B получит сообщение, посланное ему агентом A, ровно через t ? 1 шагов (тактов) после его отсылки (t0 будет обозначать минимальное число такое, что pAB(t) =0 для всех t>t0).

Для разных сообщений соответствующие случайные величины будем считать независимыми. Мы будем предполагать, что ?t=1? pAB(t) 1 . Тогда разность 1 - ?t=1? pAB(t) определяет вероятность того, что сообщение никогда не достигнет адресата, т.е. будет утеряно в канале. Например, pAB(1) = 1 означает, что каждое сообщение, посланное агентом A агенту B, будет получено адресатом на следующем шаге после его посылки. Именно такой вариант рассматривался в работах [3, 4]. Если pAB(1)=0.5, pAB(2)=0.4 и pAB(t)=0 при t >2 , то половина всех сообщений A агенту B будет получена на следующем шаге после их отсылки, еще 4/10 будут находиться в пути 2 такта, и в среднем десятая часть таких сообщений будет утеряна.

Текущее состояние канала CHAB будет включать все сообщения, посланные агентом A агенту B, которые еще не дошли до B, с указанием времени их нахождения в канале. Мы будем обозначать текущее состояние канала так же как и сам канал, т.е. CHAB ={(Msg, t) | сообщение Msg от агента A агенту b находится в канале t тактов}. Мы будем также использовать сокращения CHij и pij для CHAiAj и pAiAj, соответственно.

С каждым агентом A связана его база ACTA параметризованных действий. Каждое (параметризованное) действие имеет имя вида a(X1,…,Xm) и множество альтернатив a1= <ADDa1(X1,…,Xm), DELa1(X1,…,Xm), SENDa1(X1,…,Xm)>,…, ak= <ADDak(X1,…,Xm), DELak(X1,…,Xm), SENDak(X1,…,Xm)>. На этих альтернативах определено некоторое вероятностное распределение pa(j). Множества ADDaj(X1,…,Xm) и DELaj (X1,…,Xm) - списки атомов вида p(t1,…,tk), где p - k-местный предикат из сигнатуры внутренней БД, t1,…,tk - либо константы, либо параметры X1,…,Xm. Эти множества определяют изменения внутренней БД (добавления и удаления фактов) при выполнении данной альтернативы. SENDaj (X1,…,Xm) определяет аналогичным образом список сообщений вида msg(A,B, p(t1,…,tk)), отправляемых другим агентам. Пусть c1,…,cm - константы. Обозначим через ADDaj (c1,…,cm) множество фактов, получаемых подстановкой c1,…,cm вместо X1,…,Xm в атомы из ADDaj (X1,…,Xm). Аналогично определяются DELaj (c1,…,cm) и SENDaj (c1,…,cm). Базисные атомы вида a(c1,…, cl) назовем базисными именами действий (или просто базисными действиями).

Конкретный выбор действий для выполнения в зависимости от текущего локального состояния агента определяется парой < LPA , SelA>. Здесь LPA - логическая программа агента, определяющая совместно с фактами из текущего локального состояния агента некоторое множество Perm (= PermAt) допустимых для выполнения в данный момент базисных имен действий, а полиномиально вычислимая функция SelA выделяет из Perm некоторое базисное действие a(c1,…cq), альтернативы которого должны выполняться в текущий момент с соответствующими вероятностями (один из естественных вариантов функции выбора связан с определением некоторого отношения приоритета на действиях). Выполнение такой альтернативы (скажем, aj) состоит в следующем: 1) следующее состояние внутренней БД агента A получается из текущего состояния удалением элементов из DELaj (c1,…,cm)и добавлением элементов из ADDaj (c1,…,cm), 2) для каждого агента B A в канал CHAB добавляются пары вида (Ms, 0) для всех экземпляров сообщений Ms, для которых msg(A, B, Ms) SEND aj (c1,…,cm).

В качестве программы LPA мы рассматриваем логическую программу с предложениями вида H :- L1,...,Ln со следующими свойствами: H -атом действия, т.е. имеет вид a(t1,…,tm), где a - имя действия, t1,…,tm - либо константы, либо переменные; литералы Li - либо литералы действия, либо (экстенсиональные) литералы с предикатами из сигнатуры внутренней БД, либо литералы сообщений вида msg(Sender, A, Msg) или not msg(Sender, A, Msg), либо некоторые вычислимые в полиномиальное время встроенные предикаты.

Мы предполагаем, что предложения в программах агентов являются безопасными в том смысле, что все переменные из головы предложения H входят позитивно в тело предложения L1,...,Ln. Кроме того, мы считаем, что программа LPA является стратифицированной [1]. Тогда в каждом локальном состоянии state= <IA, MsgBoxA> программа

LPA,state = LPA IA MsgBoxA,

определяющая множество действий, которые в принципе может выполнить агент в текущем состоянии, является стратифицированной.

Хорошо известно (см. [1]), что стратифицированные логические программы имеют единственную минимальную модель. Обозначим такую модель программы LPA,state через MA,state. Стандартная процедура вычисления неподвижной точки позволяет вычислить эту модель по базисной развертке gr(LPA,state ) программы LPA,state. Отметим, что размер gr(LPA,state) может быть экспонентой от размера LPA,state. Напомним также, что предположение о замкнутости области, которое мы используем, предполагает вычислимость за полиномиальное время всех встроенных предикатов. Поэтому сохраняется вычислимость неподвижной точки за полиномиальное время.

Упомянутое выше множество Perm определяется тогда как множество базисных имен действий, содержащихся в минимальной модели MA,state . Обозначим через Sem функцию, которая по LPA,state строит это множество Perm.

Поведение вероятностных МАС

Глобальное состояние S системы A включает в себя локальные состояния ее агентов и состояния всех ее (n2-n) каналов:

S = <I1,…,In; CH1,2, CH2,1,… , CHn-1,n, CHn,n-1>.

Обозначим через SA множество всех глобальных состояний МАС A.

Тогда одношаговая семантика МАС A задает отношение S A S'

перехода (за один шаг) на множестве SA, а вероятности pi,j(t) индуцируют вероятности таких переходов p(S, S').

Переход S A S' начинается с работы каналов и формирования нового содержимого почтовых ящиков. Сначала каждый канал увеличивает на 1 счетчик времени у всех находящихся в нем сообщений. Пары (Msg, t) такие, что t>t0, удаляются из CHi,j Затем для каждой пары (Msg, t) CHi,j в почтовый ящик MsgBoxj агента Aj с вероятностью pi,j(t) помещается факт msg(Ai, Aj ,Msg). После этого каждый агент Ai A формирует множество всех допустимых на данном шаге действий Permi = Sem(LPA,state). А затем, используя свой оператор выбора SelAi , определяет выполняемое действие a(c1,…cq). Почтовые ящики всех агентов МАС A после этого опустошаются, т.е. полученные сообщения “забываются”. Разумеется, это не ограничивает общности, поскольку агент может все нужные ему данные перенести из почтового ящика в свою базу данных. Затем с вероятностью pa(j) выбирается альтернатива aj состояния внутренней БД Ii и соответствующих каналов заменяются в соответствии с определением действия этой альтернативы.

Таким образом, переход S A S' вычисляется следующим вероятностным алгоритмом:

A-шаг ( Вход: S ; Выход: S' )

(1) FOR EACH Ai, Aj A (i j) DO

(2) FOR EACH (Msg, t) CHi,j DO

(3 ) BEGIN CHi,j := (CHi,j \ {(Msg, t)} ) ;

(4) if t ? t0 then CHi,j := (CHi,j \ {(Msg, t+1)} ) ; END

(5) FOR EACH Ai, Aj A (i j) DO

(6) FOR EACH (Msg, t) CHi,j DO с вероятностью pi,j(t)

(7) BEGIN CHi,j := (CHi,j \ {(Msg, t)} ) ;

(8) MsbBoxj := MsbBoxj {msg(Ai, Aj , Msg)}

(9) END;

(10) FOR EACH Ai A DO

(11) BEGIN Permi := Sem(LPAi,state );

(12) Пусть значение SelAi (Permi) равно ai(c1,…cqi) ;

(13) Пусть ai1,…, aik - все альтернативы для ai;

(14) Выберем альтернативу aij с вероятностью pai(j);

(15) Ii`:= ((Ii \ DELaij(c1,…cq)) ADDaij(c1,…cq));

(16) FOR EACH (m i) DO

(17) CHi,m` := (CHi,m

{(ms,0)| msg(Ai, Am, Ms) SEND aij (c1,…,cq)});

(18) MsgBoxi := ;

(19) END;

(20) RETURN S'.

В соответствии с вышеприведенным определением семантики с МАС A можно связать Марковскую цепь MC(A) с множеством состояний SA и вероятностями переходов p(S, S') между ними (алгоритм вычисления p(S, S') описан в следующем разделе). Поведение A в начальном глобальном состоянии S0 описывается деревом TA(S0) возможных траекторий этой цепи, начинающихся с S0. Узлы этого дерева помечены глобальными состояниями системы, причем каждый узел, находящийся на (t+1)-ом уровне и помеченный состоянием S', связан с узлом на t-ом уровне, из пометки которого S возможен переход S A S' c вероятностью p(S, S') >0.

Заметим, что количество состояний цепи MC(A) в худшем случае может быть экспоненциальной относительно размера A , если A - базисная, и даже двойной экспоненциальной, если A - не базисная ((в размер |A| МАС A входят размеры всех сигнатур, множества констант, описаний агентов, включающих их базы действий и базисные развертки программ агентов, и распределения вероятностей).

Верификация динамических свойств

мультиагентный верификация динамический связь

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

Проблема верификации динамических свойств мультиагентных систем (которую мы называем MA-BEHAVIOR) формулируется следующим образом. Пусть даны МАС A, ее начальное глобальное состояние S0 и формула F, выражающая некоторое свойство траекторий, нужно вычислить меру (вероятность) PA(S0 , F) множества траекторий дерева TA(S0), на которых выполнена F.

Отметим, что единственным источником неопределенности в программе A-шаг являются операторы в строках 5-9 и 14, которые определяют, как сообщения попадают в почтовые ящики агентов с учетом вероятностей времен их пересылки и как выбираются альтернативы для действия ai. Мы предполагаем, что все вероятностные выборки независимы.

Это позволяет предложить следующую эффективную процедуру вычисления вероятности p(S, S') перехода S A S'

Algorithm Prob(S, S')

(1) FOR EACH Ai, Aj A (i j) DO

(2) BEGIN M[i,j] := {(m, t) | ((m, t) CHi,j) & ((m,t+1) CH'i,j )};

(3) pi,j := { pi,j(t) | ((m, t) M[i,j]}

(4) END;

(5) FOR EACH Aj A DO

(6) BEGIN MsgBoxj := ;

(7) FOR EACH Ai A (i j) DO

(8) MsgBoxj := MsgBoxj {msg( Ai, Aj ,m) | t ( (m,t) M[i,j] )}

(9) END;

(10) FOR EACH Aj A DO

(11) BEGIN Permi := Sem(LPA,state );

(12) Пусть значение SelAi (Permi) равно ai(c1,…cq) ;

(13) Пусть ai1,…, aik - все альтернативы для ai;

(14) pi, := ?j {pai(j)| (Ii`= ((Ii \ DELaij(c1,…cq)) ADDaij(c1,…cq)) ) &

(&mi {ms| (ms,0) CHi,m`} =

{ms| msg( Ai, Am ,ms) SENDaij (c1,…,cq)});

(15) END;

(16) p(S, S') := { pi,j | 1 i, j n, j i }* { pi, | 1 i n};

(18) RETURN p(S, S')

Теорема 1. Алгоритм Prob(S, S') вычисляет вероятность p(S, S') перехода S A S' за время, полиномиальное от суммы размеров МАС A и размеров исходного и результирующего состояний S и S': |A| + |S| +|S'|.

Теперь для решения проблемы MA-BEHAVIOR для вероятностных МАС мы можем использовать теорему 3.1.2.1 из работы [2], которая утверждает 1) существование алгоритмов, проверяющих выполнимость формулы F из LPTL на конечной марковской цепи M за время O(|M|2|F|) или с объемом памяти, полиномиальным относительно |F| и полилогарифмическим относительно |M|, 2) существование алгоритма, вычисляющего вероятность PM(F) выполнения F на M за время, экспоненциальное относительно |F| и полиномиальное относительно |M|.

Для применения этой теоремы нам нужно только использовать замечания в конце предыдущего раздела об оценке размера MC(A) относительно размера A. Приведем здесь только два из ряда возможных следствий.

Следствие 1. Существует алгоритм, который по базисной вероятностной МАС A, начальному состоянию S0 и формуле F из PLTL вычисляет вероятность PA(S0, F) за время, экспоненциальное относительно размера входа.

Следствие 2. Существует алгоритм, который по произвольной вероятностной МАС A, начальному состоянию S0 и формуле F из PLTL вычисляет вероятность PA(S0, F) за время, экспоненциальное относительно размера |F| и двойное экспоненциальное относительно |A|.

Следует заметить, что оценки для |MC(A)| выше были указаны для худшего случая. На практике во многих случаях эти оценки могут быть сильно понижены. Например, если арности всех используемых предикатов и действий ограничены, то число глобальных состояний для произвольной (не обязательно базисной) МАС ограничено некоторой экспонентой от полинома от размера этой МАС. Поэтому в этом случае слова «двойное экспоненциальное» в следствии 2 могут быть заменены на «экспоненциальное с полиномиальным показателем». Кроме того, при построении MC(A) многие глобальные состояния могут оказаться недостижимыми или недопустимыми, что также может привести к значительному снижению вычислительной сложности проблемы верификации.

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

1. Apt K. R., Logic programming. In: J. van Leeuwen (Ed.), Handbook of Theoretical Computer Science. Volume B. Formal Models and Semantics, Chapter 10, Elsevier Science Publishers B.V. 1990, 493-574.

2. Courcoubetis C., Yannakakis M., The complexity of probabilistic verification. J. ACM, v. 42, 4, 1995, 857-907.

3. Dekhtyar M., Dikovsky A., and Valiev M., On Feasible Cases of Checking Multi-Agent Systems Behavior. Theoretical Computer Science, Elsievier Science, 2003, vol. 303, no. 1, 63-81.

4. Dekhtyar M.I., Dikovsky A.Ja., Valiev M.K., On complexity of verification of interacting agents' behavior. Annals of Pure and Applied Logic, 141, 2006, 336 - 362.

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

6. Валиев М.К., Дехтярь М.И., Диковский А.Я, О свойствах многоагентных систем с вероятностными каналами связи. Труды IV-ой Межд. научно-практической конференции "Интегрированные модели и мягкие вычисления в искусственном интеллекте", М.; Физматлит, Коломна, 2007.

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

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