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

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

Сложность верификации мультиагентных систем с вероятностными состояниями и программами*^*Эта работа выполнена при поддержке РФФИ (гранты 07-01-00637-а и 08-01-00241-а).

Валиев М.К.

Дехтярь М.И.

Введение

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

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

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

Вероятностная мультиагентная система (МАС) A = {A1,...,An} состоит из конечного множества {A1,...,An} взаимодействующих вероятностных интеллектуальных агентов Ai. У каждого агента A системы имеется внутренняя вероятностная база данных (ВБД) IA, содержащая конечное множество аннотированных базисных (ground) атомов вида q(c1,…, ck):p, где q-предикатный символ, c1,…, ck - константы, p[0,1] - степень уверенности в факте q(c1,…, ck) (или вероятность этого факта). Отметим, что множество используемых данной системой констант ограничено. Кроме ВБД у агента A имеется почтовый ящик 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 и всех агентов A и B системы).

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

?t=1? pAB(t) 1.

1 - ?t=1? pAB(t)

определяет вероятность того, что сообщение никогда не достигнет адресата, т.е. будет утеряно в канале. Текущее состояние канала CHAB будет включать все сообщения, посланные агентом A агенту B, которые еще не дошли до B, с указанием времени их нахождения в канале. Мы будем обозначать текущее состояние канала, так же как и сам канал, т.е.

CHAB ={(Msg, t) | сообщение Msg от агента A агенту b находится в канале t тактов}.

Мы будем также использовать сокращения CHij и pij для CHAiAj и pAiAj, соответственно.

С каждым агентом A связана его база ACTA параметризованных действий вида <a(X1,…,Xm), PUTa(X1,…,Xm), SENDa(X1,…,Xm)>. Здесь a(X1,…,Xm) - (параметризованное) имя действия, PUTa(X1,…,Xm) - список аннотированных атомов вида q(t1,…,tk):p, где q - k-местный предикат из сигнатуры внутренней ВБД, t1,…,tk - либо константы, либо параметры X1,…,Xm, p - вероятность атома q(t1,…,tk). Это множество определяет изменения внутренней ВБД при выполнении данного действия (это будет уточнено в следующем разделе). Список SENDa(X1,…,Xm) содержит сообщения вида msg(A,B, p(t1,…,tk)), отправляемые другим агентам. Пусть c1,…,cm - константы. Обозначим через PUTa(c1,…,cm) множество базисных аннотированных фактов, получаемых подстановкой c1,…,cm вместо X1,…,Xm в атомы из PUTa(X1,…,Xm). Аналогично определяется и SENDa(c1,…,cm). Базисные атомы вида a(c1,…, cl) назовем базисными именами действий (или просто базисными действиями).

Конкретный выбор действий агента, возможных в данном локальном состоянии, определяется его вероятностной логической программой LPA. В качестве программ LPA мы рассматриваем вероятностные логические программы с предложениями вида H:p :- L1,...,Ln .

Здесь H - атом действия, т.е. имеет вид a(t1,…,tm), где t1,…,tm - либо константы, либо переменные, p[0,1]; литералы Li - либо аннотированные атомы действий, либо (экстенсиональные) аннотированные атомы вида q(t1,…,tk):[l,u] с предикатами q из сигнатуры внутренней БД и аннотациями [l,u] - подинтервалами отрезка [0,1], либо литералы сообщений вида msg(Sender, A, Msg) или not msg(Sender, A, Msg), либо атомы с сигнатурой из некоторых вычислимых в полиномиальное время встроенных предикатов.

Такие вероятностные логические программы являются частным случаем логических программ с интервальными вероятностями, определенных в работе [9]. В [10] было показано, что в общем случае программы из [9] не имеют естественной просто вычислимой семантики. Можно показать, что для определенного выше варианта вероятностных логических программ такая семантика существует и может быть вычислена за полиномиальное время от размера базисной развертки gr(LPA,state) программы мультиагентный верификация программа логический

LPA, state = LPA IA MsgBoxA.

PermA (= Sem(LPAi,state))

множество базисных аннотированных имен действий {a1(c1,1,…cm1,1):p1, …, ak(c1,k,…cmk,k): pk} определяемых семантикой программы gr(LPA,state).

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

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

Определим операционную семантику введенных в предыдущем разделе вероятностных МАС.

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

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

Обозначим через SA множество всех глобальных состояний МАС A. Тогда одношаговая семантика МАС A задает отношение S A S' перехода (за один шаг) на множестве SA, а вероятности, участвующие в определениях агентов A, индуцируют вероятности таких переходов 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(LPi,state).

Затем по Permi формируется множество выполняемых агентом Ai действий Obli: для каждого аннотированного атома a(c1,…cm):p из Permi действие a(c1,…cm) помещается в Obli с вероятностью p. Почтовые ящики всех агентов МАС A после этого опустошаются, т.е. полученные сообщения "забываются". Разумеется, это не ограничивает общности, поскольку агент может все нужные ему данные перенести из почтового ящика в свою базу данных. После этого каждый агент Ai выполняет действия из Obli следующим образом. Обозначим через UPDi множество

{q(t1,…,tk):p | p = max{ p' | q(t1,…,tk):p'PUTa(c1,…,cm)

для некоторого a(c1,…cm) из Obli }}. Тогда новое состояние ВБД Ii получается путем удаления из Ii всех старых фактов из множества

UPD_OLDi = {q(t1,…,tk):r | для некоторого p q(t1,…,tk):pUPDi}

и добавления к Ii новых аннотированных фактов из UPDi. И наконец, агент Aj добавляет в каждый канал CHij (i j) все пары вида (Msg, 0), где Msg является базисным экземпляром некоторого сообщения вида msg(Ai, Aj, p(t1,…,tk)) из множества SENDa(c1,…cm) для некоторого a(c1,…cm) из Obli.

Таким образом, переход 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) FOR EACH a(c1,…cm):p Permi DO

(13) помеcтить a(c1,…cm) в Obli с вероятностью p;

(14) UPDi :={q(t1,…,tk):p|p = max{p'|

q(t1,…,tk):p'PUTa(c1,…,cm)Лa(c1,…cm) Obli}};

(15) UPD_OLDi= {q(t1,…,tk):r Ii | q(t1,…,tk):p UPDi};

(16) Ii':= ((Ii \ UPD_OLDi) UPDi;

(17) FOR EACH (m i) DO

(18) CHi,m' := (CHi,m

{(ms,0)| msg(Ai, Am, Ms) SEND a (c1,…,ck)

Л a(c1,…ck) Obli });

(19) MsgBoxi := ;

(20) END;

(21) RETURN S'=(Ii',…,In', CH1,2',…, CHn-1,n').

Для завершения определения одношаговой семантики A нужно еще дать точное описание для Sem(LPAi,state), чему посвящен следующий раздел.

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

В этом пункте мы рассмотрим вычисление оператора Sem(P) для базисной вероятностной логической программы P. Обозначим множество всех базисных (неаннотированных) атомов (эрбранов универсум, включающий как экстенсиональные атомы, так и атомы действий) через U. Интерпретация f: U >[0,1] сопоставляет каждому атому q(c1,…cm)U его вероятность f(q(c1,…cm)). Атом действия a(c1,…cm):p выполнен на интерпретации f, если p ? f(a(c1,…cm)). Аннотированный экстенсиональный атом вида q(t1,…,tk):[l,u] выполнен на интерпретации f, если l ? f(q(t1,…,tk)) ? u. Выполнимость литералов сообщений вида msg(Sender, A, Msg) или not msg(Sender, A, Msg) определяется относительно текущего состояния MsgBoxA обычным образом. Выполнимость встроенных предикатов определяется их естественной семантикой. Предложение a(c1,…cm):p :- L1,...,Ln выполняется на интерпретации f (для данного MsgBoxA), если при условии, что каждый Li выполняется на f, имеет место неравенство f(a(c1,…cm)) ? p. Интерпретация f является моделью P, если на ней выполнены все предложения P. Определим на множестве интерпретаций частичный порядок ? следующим образом: f1 ? f2 для каждого атома q U f1(q) ? f2(q). Модель f программы P назовем минимальной, если для всякой другой модели f1 программы P неверно, что f1 ? f. Множество моделей P замкнуто относительно "минимизации".

Лемма 1. Пусть f1 и f2 - модели программы P. Тогда и интерпретация