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

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

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

Институт прикладной математики РАН

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

М.К. Валиев

М.И. Дехтярь

Аннотация

Приводится обзор полученных авторами результатов о моделировании вероятностных мультиагентных систем Марковскими цепями и процессами принятия решений. Применяя известные результаты о сложности верификации динамических свойств Марковских систем, мы получаем верхние оценки сложности верификации для обычных и недетерминированных вероятностных мультиагентных систем.

Введение

Мультиагентные системы (МАС) составляют одну из наиболее активно развивающихся областей теории и практики искусственного интеллекта (см., например, [Subrahmanian et al., 2000], [Тарасов, 2002]). При этом значительное место занимает изучение МАС, содержащих агенты, действия которых включают в себя элементы случайности (вероятностных МАС, кратко ВМАС). Уже обычные МАС довольно сложны и включают в себя много разных средств, позволяющих достаточно адекватно моделировать разнообразные практические системы, но затрудняющих их формальное изучение. Для ВМАС последнее обстоятельство еще более усугубляется из-за добавления новых (вероятностных) элементов. Поэтому представляет интерес изучение возможности моделирования ВМАС классическими хорошо изученными марковскими системами (Марковскими цепями или процессами принятия решений).

В этой работе мы приводим краткий обзор наших результатов по такому моделированию (см., в частности, [Dekhtyar et al., 2008], [Валиев и др., 2009]). Заметим, что в общем случае действия агентов ВМАС могут быть не только вероятностными, но и недетерминированными. ВМАС, содержащие такие агенты, будем называть недетерминированными (НВМАС). ВМАС, которые содержат только обычные вероятностные агенты, будем называть (чтобы отличать их от НВМАС) последовательными (ПВМАС).

Наши результаты в раз. 3 ниже показывают, что ПВМАС достаточно эффективно моделируются конечными Марковскими цепями, а НВМАС - конечными Марковскими процессами принятия решений. В разделе 4 приводятся некоторые результаты о сложности верификации динамических свойств ПВМАС и НВМАС, которые следуют из результатов раздела 3 и известных результатов Варди, Куркубетиса-Яннакакиса и др. о верификации Марковских цепей и процессов (соответствующие ссылки см. в разделе 4).

1. Вероятностные мультиагентные системы

Два типа вероятностных МАС: последовательные и недетерминированные.

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

НВМАС A содержит конечное множество взаимодействующих интеллектуальных агентов A_i, управляемых некоторыми вероятностными логическими программами. У каждого агента A системы имеется внутренняя вероятностная база данных (ВБД) I_A, содержащая конечное множество аннотированных базисных (ground) атомов вида q(c₁,…, c_k):p, где q - предикатный символ, c₁,…, c_k - константы, p[0,1] - степень уверенности в факте q(c₁,…, c_k) (или вероятность этого факта). Будем считать, что множество используемых данной системой констант ограничено. Кроме ВБД у агента A имеется почтовый ящик 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 шагов (тактов) после его отсылки (t₀ будет обозначать минимальное число такое, что p_AB(t) = 0 для всех t > t₀ и всех агентов A и B системы).

Для разных сообщений соответствующие случайные величины будем считать независимыми. Мы предполагаем, что ?_t=1^? p_AB(t)1. Тогда разность 1-?_t=1^? p_AB(t) определяет вероятность того, что сообщение никогда не достигнет адресата, т.е. будет утеряно в канале. Текущее состояние канала 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), PUT_a(X₁,…, X_m), SEND_a(X₁,…, X_m)>. Здесь a(X₁,…, X_m) - (параметризованное) имя действия, PUT_a(X₁,…, X_m) - список аннотированных атомов вида q(t₁,…, t_k):p, где q - k-местный предикат из сигнатуры внутренней ВБД, t₁,…, t_k - либо константы, либо параметры X₁,…, X_m, p - вероятность атома q(t₁,…, t_k)). Это множество определяет изменения внутренней ВБД при выполнении данного действия (это будет уточнено ниже в п.3). Список SEND_a(X₁,…, X_m) содержит сообщения вида msg(A, B, p(t₁,…, t_k))), отправляемые другим агентам. Пусть c₁,…, c_m - константы. Обозначим через PUT_a(c₁,…, c_m) множество базисных аннотированных фактов, получаемых подстановкой c₁,…, c_m вместо X₁,…,X_m в атомы из PUT_a(X₁,…, X_m). Аналогично определяется и SEND_a(c₁,…, c_m). Базисные атомы вида a(c₁,…, c_m) назовем базисными атомами действий (или просто базисными действиями).

Конкретный выбор действий агента, исполняемых в данном локальном состоянии, определяется парой (LP_A, Sel_A). Здесь LP_A - вероятностная логическая программа, которая в каждый момент времени определяет в зависимости от текущего локального состояния Im_A некоторое множество Perm_A аннотированных базисных действий, разрешенных к выполнению на этом шаге (более точно Perm_A будет определено ниже в п. 1.2). Sel_A - полиномиально вычислимый оператор, который недетерминированным образом окончательно выбирает для выполнения некоторое подмножество из Perm_A. Последовательные ВМАС выделяются из общего случая тем, что в них в качестве Sel_A допускается произвольный полиномиально вычислимый детерминированный оператор. Таким образом, это определение последовательных ВМАС несколько обобщает определение ВМАС. [Валиев и др., 2009] В этой работе оператор SelA не использовался, и для исполнения всегда выбиралось все множество PermA допустимых в данный момент действий. Но в некоторых случаях желательно выбирать для выполнения не все множество PermA , а, например, некоторое его непротиворечивое подмножество..

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

Вычисление семантики вероятностной логической программы

В этом пункте мы рассмотрим вычисление оператора Sem(P) для базисной вероятностной логической программы P. Обозначим множество всех базисных (неаннотированных) атомов (эрбранов универсум, включающий как экстенсиональные атомы, так и атомы действий) через U. Интерпретация f: U >[0,1] сопоставляет каждому атому q(c₁,…, c_m)U его вероятность f(q(c₁,…, c_m)). Атом действия a(c₁,…, c_m):p выполнен на интерпретации f, если f(a(c₁,…,c_m))?p. Аннотированный экстенсиональный атом вида q(t₁,…, t_k):p выполнен на интерпретации f, если p ? f(q(t₁,…, t_k)). Выполнимость литералов сообщений вида msg(Sender, A, Msg) или not msg(Sender, A, Msg) определяется относительно текущего состояния MsgBox_A обычным образом. Выполнимость встроенных предикатов определяется их естественной семантикой. Предложение программы P a(c₁,…, c_m):p:- L₁,..., L_n выполняется на интерпретации f (для данного MsgBox_A), если при условии, что каждый L_i выполняется на f, имеет место неравенство f(a(c₁,…, c_m))?p. Интерпретация f является моделью P, если на ней выполнены все предложения P. Определим на множестве интерпретаций частичный порядок ? следующим образом: f₁ ? f₂ для каждого атома qU, f₁(q) ? f₂(q). Модель f программы P назовем минимальной, если для всякой другой модели f₁ программы P неверно, что f₁ ? f. Множество моделей P замкнуто относительно «минимизации».

Рассматриваемые здесь вероятностные логические программы являются частным случаем логических программ с интервальными вероятностями, определенных в работе [Ng et al., 1993] (наши программы соответствуют случаю, когда все интервалы имеют вид [p,1]). В [Dekhtyar et al., 2009] было показано, что в общем случае вычисление семантики программ из [Ng et al., 1993] вызывает определенные трудности. Можно показать, что для рассматриваемого здесь варианта программ семантика возможных миров совпадает с семантикой минимальной неподвижной точки, для вычисления которой имеется эффективный алгоритм.

Лемма 1. Пусть f₁ и f₂ - модели программы P. Тогда и интерпретация f = min(f₁, f₂)= {q:p|qUЛp=min(f₁(q), f₂(q))} является моделью P.

Из этой леммы следует существование минимальной модели P. Ее вычисление обеспечивается процедурой вычисления неподвижной точки, аналогичной процедуре из [Ng et al., 1993].

Теорема 1. Для всякой вероятностной логической программы P (определенного в этой работе типа) существует минимальная модель fmin(P), которая вычислима за полиномиальное время от размера базисной развертки gr(P) программы P.

Для агента A в текущем состоянии Im_A пусть программа

LP_A,state = LP_A I_A MsgBox_A.

Определим Perm_A=Sem(LP_A,state) как множество всех аннотированных атомов действий a(c₁,…, c_m):p из fmin(LP_A,state).

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 определяет, как A преобразует одно глобальное состояние S в другие состояния.

Переход S_AS' начинается с опустошения почтовых ящиков всех агентов. После этого формируются новые содержимые всех каналов CH_i,j и почтовых ящиков: 1) счетчики времени сообщений, находящихся в CH_i,j, увеличиваются на 1, 2) пары (Msg, t) такие, что t>t₀, удаляются из CH_i,j, 3) для каждой пары (Msg, t)CH_i,j в почтовый ящик MsgBox_j агента A_j с вероятностью p_i,j(t) помещается факт msg(A_i, A_j , Msg). После этого каждый агент A_iA формирует множество всех допустимых на данном шаге аннотированных базисных действий Perm_i=Sem(LP_i,state), и оператор Sel_Ai недетерминированно выбирает некоторое подмножество Selected_Ai из Perm_i. После этого формируется множество Obl_i выполняемых агентом A_i действий: а именно, для каждого аннотированного атома a(c₁,…, c_m):p из Sel(Perm_i) действие a(c₁,…, c_m) помещается в Obl_i с вероятностью p. После этого каждый агент A_i выполняет действия из Obl_i следующим образом. Обозначим через UPD_i множество {q(t₁,…, t_k):p | p = max{p'|q(t₁,…, t_k):p'PUT_a(c₁,…, c_m) для некоторого a(c₁,…, c_m) из Obl_i}}. Тогда новое состояние ВБД I_i получается путем удаления из I_i всех старых фактов из множества UPD_OLD_i ={q(t₁,…, t_k):r|для некоторого p q(t₁,…, t_k):pUPD_i} и добавления к I_i новых аннотированных фактов из UPD_i. И наконец, агент A_j добавляет в каждый канал CH_ij (ij) все пары вида (Msg,0), где Msg является базисным экземпляром некоторого сообщения вида msg(A_i, A_j, p(t₁,…, t_k)) из множества SEND_a(c₁,…, c_m) для некоторого a(c₁,…, c_m) из Obl_i.

Определение семантики для ПВМАС практически совпадает с вышеприведенным определением, нужно только учесть, что у ПВМАС оператор Sel является детерминированным и однозначно по множеству Perm определяет множество исполняемых действий Obl.

3. Моделирование ВМАС Марковскими системами

Так же как в предыдущем разделе мы начнем с моделирования НВМАС Марковскими процессами принятия решений, а затем приведем простые соображения, как из этого получается моделирование ПВМАС марковскими цепями.

Вспомним определение Марковских процессов принятия решений. Процесс M состоит из 1) множества S (состояний), 2) множества A действий (мы будем называть их M-действиями, чтобы отличить от действий НВМАС), 3) вероятностных распределений P_S,a на S для каждого состояния S из S и действия a из A и 4)начального состояния S₀ из S. Выполнение процесса M состоит в переходе из одних состояний в другие, начиная с S₀. Любой переход из S выполняется в два шага: 1) недетерминированно выбирается некоторое M-действие a, и 2) выполняется переход от S к S' с вероятностью P_S,a(S').

Следовательно, для моделирования НВМАС A Марковским процессом Mod_A нам нужно определить соответствующие компоненты Mod_A. Множество состояний Mod_A мы определим как множество глобальных состояний A. M-действия будут составными и будут задаваться как наборы Selected=(Selected₁,…, Selected_n), где Selected_i - некоторое подмножество множества всех аннотированных базисных атомов действий агента A_i. Остается определить P_S,Selected для любого глобального состояния S системы A и M-действия Selected. Они определяются следующей (детерминированной) программой, которая вычисляет вероятность перехода от S к глобальному состоянию S' при условии, что каждый агент A_i выбирает для выполнения аннотированные действия из Selected_i.

Алгоритм Prob_Selected(A, 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]} END;

(4) FOR EACH A_j A DO

(5) BEGIN MsgBox_j := ;

(6) FOR EACH A_i A (i j) DO

(7) MsgBox_j := MsgBox_j {msg( A_i, A_{j ,}m) | t ( (m,t) M[i,j] )} END;

(8) FOR EACH A_i A DO

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

(10) IF Selected_i не входит в Range(Sel(Perm_i)) THEN RETURN 0 END;

(11) FOR EACH A_j A DO

(12) SelAct_j := { a(c₁,…c_m) | a(c₁,…c_m):p Selected_j};

(13) p_i := 0 ;

(14) FOR EACH Obl, где Obl - подмножество из SelAct_i DO

(15) BEGIN UPD:= {q(t₁,…,t_k):p | p = max{p' | q(t₁,…,t_k):p'PUT_a(c₁,…,c_m) Л a(c₁,…c_m) Obl }};

(16) UPD_OLD= {q(t₁,…,t_k):r I_i | q(t₁,…,t_k):p UPD};

(17) IF (I_i':= ((I_i \ UPD_OLD) UPD) Л (Л _mi {ms| (ms,0) CH_i,m'} =

{ms | msg(Ai,Am,ms)SEND_a(c₁,…,c_q) для некоторого a(c₁,…c_m) Obl})

(18) THEN p_i := p_i + {p_a | a(c₁,…c_m) Obl Л a(c₁,…c_m):p Selected_i}*

*{(1 ? p_a) | a (SelAct_i \ Obl) Л a: p_a Selected_i };

(19) END;

(20) p(S, S') := {p_i,j|1i, jn, ji}* {p_i|1in};

(21) RETURN p(S, S').

Теорема 2. Алгоритм Prob_Selected(A, S, S') вычисляет вероятность p_Selected(S, S') перехода S _A S' при условии выбора процессом Mod_A M-действия Selected. Время его работы ограничено сверху величиной 2^r_* pol(|A| + |S| +|S'|), где r - максимальное число различных базисных действий одного агента системы, pol - некоторый полином, а |A| + |S| +|S'| - сумма размеров НВМАС A и размеров исходного и результирующего состояний S и S'.

Заметим, что наличие параметра Selected у вышеописанного алгоритма связано с необходимостью определения матрицы вероятностей переходов отдельно для каждого M-действия Selected. Конечно, таких M-действий очень много (до 2^{r n}, где n - число агентов в A), но большинство из них не будет использовано (см. строку (10) программы). Кроме того, при моделировании можно использовать вычисление вероятностей переходов по мере необходимости, а не вычислять их все заранее.

При моделировании ПВМАС параметр Selected вырождается, и можно говорить просто о вычислении вероятностей переходов из состояния S в состояние S' (т.е. получаем обычную цепь Маркова). Соответствующий алгоритм вычисления почти совпадает с Prob_Selected(A, S, S'), нужно только заменить строку (10) на (10') Selected_i :=Sel_i (Perm_i). Ясно, что при этом время вычисления не увеличится (обычно даже уменьшится) по сравнению со временем работы алгоритма Prob_Selected(A, S, S').

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

Приведенные выше результаты о моделировании позволяют применить известные результаты о верификации динамических свойств Марковских систем (Vardi, 1985], [Courcoubetis et al., 1995], [Hansson et al., 1994], [De Alfaro, 1998] и др.; подробное обсуждение этих вопросов см. в книге [Baier et al., 1974] или обзорной статье [Kwiatkowska, 2003]]) к верификации ВМАС. Из большого количества возможных следствий приведем только некоторые.

В частности, мы ограничим обсуждение базисными ВМАС и верификацией их динамических свойств, выражаемых формулами пропозициональных темпоральных логик (для небазисных систем и предикатных логик имеются аналогичные результаты, но с существенным возрастанием временной сложности). В приводимых ниже следствиях PLTL обозначает пропозициональную логику линейного времени с оператором Until, PCTL - пропозициональную логику ветвящегося времени с вероятностно-временным оператором Until_p (истинность [Ф Until ]_p в состоянии s означает, что с вероятностью p существует путь с началом s, на некотором состоянии которого выполнено , а на всех предшествующих состояниях этого пути выполнено Ф), PCTL* - некоторое существенное расширение PCTL (более точные определения см. в вышеприведенных ссылках).

Следствие 1. Выполнимость PLTL-формулы Ф на базисной ПВМАС A может быть проверена с использованием памяти, полиномиальной относительно размеров A и Ф.

Следствие 2. Выполнимость PLTL-формулы Ф на базисной НВМАС A может быть проверена за время, экспоненциальное от размера A и двойное экспоненциальное от размера Ф.

Следствие 3. Выполнимость PCTL-формулы Ф на базисной ПВМАС или НВМАС A может быть проверена за время, экспоненциальное от размера A (для НВМАС с более высоким основанием экспоненты) и линейное от размера Ф.

Следствие 4. Выполнимость PCTL*-формулы Ф на базисной ПВМАС A может быть проверена за время, экспоненциальное от размера A и линейное от размера Ф.

Следствие 5. Выполнимость PCTL*-формулы Ф на базисной НВМАС A может быть проверена за время, экспоненциальное от размера A и двойное экспоненциальное от размера Ф.

Благодарности. Работа выполнена при финансовой поддержке РФФИ (проекты № 10-01-00532а, , 08-01-00241-a)).

1. Валиев М.К., Дехтярь М.И.. Сложность верификации мультиагентных систем с вероятностными состояниями и программами. // Труды V Межнар. научно-практической конференции. "Интегрированные модели и мягкие вычисления в искусственном интеллекте", т.1. - М.: Физматлит, 2009.

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

3. Baier C., Katoen J. Principles of model checking. MIT Press, 2008.

4. Courcoubetis C., Yannakakis M., The complexity of probabilistic verification.// J. ACM, 1995. V. 42. №4.

5. De Alfaro L. Formal verification of probabilistic systems. PhD Thesis, Stanford Univ., 1998.

6. Dekhtyar A., Dekhtyar M.I. The Theory of Interval Probabilistic Logic Programs. // Annals of Mathematics and Artificial Intelligence, 55, 2009. № 3-4.

7. Dekhtyar M.I., Dikovsky A.Ja., Valiev M.K. Temporal verification of probabilistic multi-agent systems. //Pillars of Computer Science: Essays Dedicated to Boris Trakhtenbrot on the Occasion of His 85th Birthday, LNCS, 4800, 2008.

8. Hansson H., Jonsson B. A logic for reasning about time and reliability.// Formal Aspects of Computing. 1994. №6 (5).

9. Kwiatkowska Marta. Model Checking for probability and time:from theory to practice. //: Proc. 18th IEEE Symposium on Logic in Computer Science, 2003.

10. Ng R. and Subrahmanian V.S. Probabilistic logic programming. // Information and Computation, 101, 2, 1993.

11. Subrahmanian V.S., Bonatti P., Dix J., et al., Heterogeneous agent systems, MIT LPess, 2000.

12. Vardi M.Y., Automatic verification of probabilistic concurrent finite State programs. //: Proceedings of 26th IEEE Symposium on Foundations of Computer Science. IEEE, New York, 1985.

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