О ВЕРИФИКАЦИИ СВОЙСТВ ВЕРОЯТНОСТНЫХ МУЛЬТИАГЕНТНЫХ СИСТЕМ[1]

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

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

(495)250-79-38, valiev@keldysh.ru

Дехтярь М.И., к.ф.-м.н., доцент

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

(482-2)365410, Michael.Dekhtyar@tversu.ru

Диковский А.Я., д.ф.-м.н.

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

(495)250-79-38, dikovsky@keldysh.ru

1. Введение

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

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

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

Мультиагентная система (МАС) A = {A₁,...,A_n} состоит из конечного множества {A₁,...,A_n} взаимодействующих интеллектуальных агентов A_i. У интеллектуального агента A имеется внутренняя база данных (БД) I_A, содержащая конечное множество базисных атомов (т.е. выражений вида p(c₁,…, c_k), где p-предикатный символ, c₁,…, c_k - константы, причем множество используемых данной системой констант ограничено), и почтовый ящик MsgBox_A. Текущие содержимые внутренней БД и почтового ящика агента A составляют его текущее локальное состояние IM_A=<I_A,MsgBox_A>.

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

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

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

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

С каждым агентом A связана его база ACT_A параметризованных действий. Каждое (параметризованное) действие имеет имя вида a(X₁,…,X_m) и множество альтернатив a¹= <ADD_a¹(X₁,…,X_m), DEL_a¹(X₁,…,X_m), SEND_a¹(X₁,…,X_m)>,…, a^k= <ADD_a^k(X₁,…,X_m), DEL_a^k(X₁,…,X_m), SEND_a^k(X₁,…,X_m)>. На этих альтернативах определено некоторое вероятностное распределение p_a(j). Множества ADD_a^j(X₁,…,X_m) и DEL_a^j (X₁,…,X_m) – списки атомов вида p(t₁,…,t_k), где p – k-местный предикат из сигнатуры внутренней БД, t₁,…,t_k – либо константы, либо параметры X₁,…,X_m. Эти множества определяют изменения внутренней БД (добавления и удаления фактов) при выполнении данной альтернативы. SEND_a^j (X₁,…,X_m) определяет аналогичным образом список сообщений вида msg(A,B, p(t₁,…,t_k)), отправляемых другим агентам. Пусть c₁,…,c_m – константы. Обозначим через ADD_a^j (c₁,…,c_m) множество фактов, получаемых подстановкой c₁,…,c_m вместо X₁,…,X_m в атомы из ADD_a^j (X₁,…,X_m). Аналогично определяются DEL_a^j (c₁,…,c_m) и SEND_a^j (c₁,…,c_m). Базисные атомы вида a(c₁,…, c_l) назовем базисными именами действий (или просто базисными действиями).

Конкретный выбор действий для выполнения в зависимости от текущего локального состояния агента определяется парой < LP_A , Sel_A>. Здесь LP_A - логическая программа агента, определяющая совместно с фактами из текущего локального состояния агента некоторое множество Perm (= Perm_At) допустимых для выполнения в данный момент базисных имен действий, а полиномиально вычислимая функция Sel_A выделяет из Perm некоторое базисное действие a(c₁,…c_q), альтернативы которого должны выполняться в текущий момент с соответствующими вероятностями (один из естественных вариантов функции выбора связан с определением некоторого отношения приоритета на действиях). Выполнение такой альтернативы (скажем, a^j) состоит в следующем: 1) следующее состояние внутренней БД агента A получается из текущего состояния удалением элементов из DEL_a^j (c₁,…,c_m)и добавлением элементов из ADD_a^j (c₁,…,c_m), 2) для каждого агента B ¹ A в канал CH_AB добавляются пары вида (Ms, 0) для всех экземпляров сообщений Ms, для которых msg(A, B, Ms) Î SEND _a^j (c₁,…,c_m).

В качестве программы LP_A мы рассматриваем логическую программу с предложениями вида H :- L₁,...,L_n со следующими свойствами: H –атом действия, т.е. имеет вид a(t₁,…,t_m), где a – имя действия, t₁,…,t_m – либо константы, либо переменные; литералы L_i – либо литералы действия, либо (экстенсиональные) литералы с предикатами из сигнатуры внутренней БД, либо литералы сообщений вида msg(Sender, A, Msg) или not msg(Sender, A, Msg), либо некоторые вычислимые в полиномиальное время встроенные предикаты.

Мы предполагаем, что предложения в программах агентов являются безопасными в том смысле, что все переменные из головы предложения H входят позитивно в тело предложения L₁,...,L_n. Кроме того, мы считаем, что программа LP_A является стратифицированной [1]. Тогда в каждом локальном состоянии state= <I_A, MsgBox_A> программа

LP_A,state = LP_A È I_A È MsgBox_A,

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

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

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

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

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

S = <I₁,…,I_n; CH_1,2, CH_2,1,… , CH_n-1,n, CH_n,n-1>.

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

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

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

Переход S Þ_A S’ начинается с работы каналов и формирования нового содержимого почтовых ящиков. Сначала каждый канал увеличивает на 1 счетчик времени у всех находящихся в нем сообщений. Пары (Msg, t) такие, что t>t₀, удаляются из CH_i,j Затем для каждой пары (Msg, t) Î CH_i,j в почтовый ящик MsgBox_j агента A_j с вероятностью p_i,j(t) помещается факт msg(A_i, A_j ,Msg). После этого каждый агент A_i Î A формирует множество всех допустимых на данном шаге действий Perm_i = Sem(LP_A,state). А затем, используя свой оператор выбора Sel_Ai , определяет выполняемое действие a(c₁,…c_q). Почтовые ящики всех агентов МАС A после этого опустошаются, т.е. полученные сообщения “забываются”. Разумеется, это не ограничивает общности, поскольку агент может все нужные ему данные перенести из почтового ящика в свою базу данных. Затем с вероятностью p_a(j) выбирается альтернатива a^j состояния внутренней БД I_i и соответствующих каналов заменяются в соответствии с определением действия этой альтернативы.

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

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

(1) FOR EACH A_i, A_j Î A (i ¹ j) DO

(2) FOR EACH (Msg, t) Î CH_i,j DO

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

(4) if t ≤ t₀ then CH_i,j := (CH_i,j \ {(Msg, t+1)} ) ; END

(5) FOR EACH A_i, A_j Î A (i ¹ j) DO

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

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

(8) MsbBox_j := MsbBox_j È{msg(A_i, A_j , Msg)}

(9) END;

(10) FOR EACH A_i Î A DO

(11) BEGIN Perm_i := Sem(LP_Ai,state );

(12) Пусть значение Sel_Ai (Perm_i) равно a_i(c₁,…c_qi) ;

(13) Пусть a_i¹,…, a_i^k - все альтернативы для a_i;

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

(15) I_i^`:= ((I_i \ DEL_ai^j(c₁,…c_q)) È ADD_ai^j(c₁,…c_q));

(16) FOR EACH (m ¹ i) DO

(17) CH_i,m` := (CH_i,m È

{(ms,0)| msg(A_i, A_m, Ms) Î SEND _ai^j (c₁,…,c_q)});

(18) MsgBox_i := Æ;

(19) END;

(20) RETURN S’.

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

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

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

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

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

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

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

Algorithm Prob(S, S’)

(1) FOR EACH A_i, A_j Î A (i ¹ j) DO

(2) BEGIN M[i,j] := {(m, t) | ((m, t) Î CH_i,j) & ((m,t+1) Ï CH’_i,j )};

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

(4) END;

(5) FOR EACH A_j Î A DO

(6) BEGIN MsgBox_j := Æ;

(7) FOR EACH A_i Î A (i ¹ j) DO

(8) MsgBox_j := MsgBox_j È {msg( A_i, A_{j ,}m) | $t ( (m,t) ÎM[i,j] )}

(9) END;

(10) FOR EACH A_j Î A DO

(11) BEGIN Perm_i := Sem(LP_A,state );

(12) Пусть значение Sel_Ai (Perm_i) равно a_i(c₁,…c_q) ;

(13) Пусть a_i¹,…, a_i^k - все альтернативы для a_i;

(14) p_i, := ∑_j {p_ai(j)| (I_i^`= ((I_i \ DEL_ai^j(c₁,…c_q)) È ADD_ai^j(c₁,…c_q)) ) &

(&_m¹i {ms| (ms,0) Î CH_i,m`} =

{ms| msg( A_i, A_{m ,}ms) Î SEND_ai^j (c₁,…,c_q)});

(15) END;

(16) p(S, S’) := Õ { p_i,j | 1 £ i, j £ n, j ¹ i }* Õ { p_i, | 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) существование алгоритма, вычисляющего вероятность P_M(F) выполнения F на M за время, экспоненциальное относительно |F| и полиномиальное относительно |M|.

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

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

Следствие 2. Существует алгоритм, который по произвольной вероятностной МАС A, начальному состоянию S⁰ и формуле F из PLTL вычисляет вероятность P_A(S⁰, 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.

---

[1] Эта работа выполнена при поддержке РФФИ (гранты 07-01-00637-а и 05-01-01006-а).