Реферат: Сложность верификации мультиагентных систем с вероятностными состояниями и программами* Валиев М. К

СЛОЖНОСТЬ ВЕРИФИКАЦИИ МУЛЬТИАГЕНТНЫХ СИСТЕМ С ВЕРОЯТНОСТНЫМИ СОСТОЯНИЯМИ И ПРОГРАММАМИ*


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

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

e-mail: valiev@keldysh.ru

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

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

e-mail: Michael.Dekhtyar@tversu.ru


1. ВВЕДЕНИЕ

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

^ 2. ВЕРОЯТНОСТНЫЕ МУЛЬТИАГЕНТНЫЕ СИСТЕМЫ

Имеются различные подходы к определению интеллектуальных агентов [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 параметризованных действий вида 1,…,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 ).

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

^ 3. ПОВЕДЕНИЕ ВЕРОЯТНОСТНЫХ МУЛЬТИАГЕНТНЫХ СИСТЕМ

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

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

S = 1,…,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):pUPDi} и добавления к 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), чему посвящен следующий раздел.

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

В этом пункте мы рассмотрим вычисление оператора 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. Тогда и интерпретация f = min(f1,f2)= {q:p|q U Λ p=min(f1(q), f2(q))} является моделью P.

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

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

Определим Perm = Sem(P) как множество всех аннотированных атомов действий a(c1,…cm):p из fminP.

^ 5.ВЫЧИСЛЕНИЕ ВЕРОЯТНОСТЕЙ ПЕРЕХОДОВ

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

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

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

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

Алгоритм 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) PermAct :- { a(c1,…cm) | a(c1,…cm):p  Permi};

(12) pi, := 0 ;

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

(14) BEGIN UPD := { q(t1,…,tk):p | p = max{ p’ |

q(t1,…,tk):p’PUTa(c1,…,cm) Λ a(c1,…cm) Obl }} ;

(15) UPD_OLD= {q(t1,…,tk):r Ii | q(t1,…,tk):p  UPD};

(16) IF (Ii’:= ((Ii \ UPD_OLD)  UPD) Λ (Λ mi {ms| (ms,0) 

CHi,m’} = {ms | msg(Ai,Am,ms)SENDa(c1,…,cq) для

некоторого a(c1,…cm) Obl})

(17) THEN pi, := pi +  {pa | a(c1,…cm) Obl Λ a(c1,…cm):p  Permi}

(18) END;

(16) p(S, S’) :=  { pi,j | 1  i, j  n, j  i }*  { pi, | 1  i n};

(18) RETURN p(S, S’).

Теорема 2. Алгоритм Prob(S, S’) вычисляет вероятность p(S, S’) перехода S A S’. Время работы Prob(S, S’) ограничено величиной 2r pol(|A| + |S| +|S’|), где r – максимальное число различных базисных действий одного агента системы, pol – некоторый полином, а |A| + |S| +|S’| – сумма размеров МАС A и размеров исходного и результирующего состояний S и S’.

Заметим, что экспонента 2r возникла из-за перебора всех подмножеств множества PermAct в строке (13) алгоритма. Если ограничить выбор действий для выполнения фиксированным числом, например, самых вероятных действий, то алгоритм становится полиномиальной сложности.

^ 6. ВЕРИФИКАЦИЯ ДИНАМИЧЕСКИХ СВОЙСТВ

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

Так же как и в [3] мы приведем только некоторые из следствий применения результатов из [4, 5] к (обобщенным) вероятностным МАС.

Теорема 3. (1) Существует алгоритм, который проверяет выполнимость FLTL-формулы F на состоянии S базисной вероятностной МАС A в памяти, полиномиальной от |A| и |F|.

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

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

Теорема 4. (1) Существует алгоритм, который проверяет выполнимость FPCTL-формулы F на состоянии S базисной вероятностной МАС A за время, зависящее экспоненциально от |A| и линейно от |F|.

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


Литература

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.

Валиев М.К., Дехтярь М.И., Диковский А.Я, О свойствах многоагентных систем с вероятностными каналами связи// Интегрированные модели и мягкие вычисления в искусственном интеллекте. Труды IV-й Международной научно-практической конференции (Коломна, 28-30 мая 2007 г.).– М.: Физматлит, 2007. – С.119-126.

Валиев М.К., Дехтярь М.И. Вероятностные мультиагентные системы: семантика и верификация// Вестник Тверского государственного университета, серия «Прикладная математика». – 2008. –№35(95). – С.9-22.

Courcoubetis C., Yannakakis M. The Complexity of Probabilistic Verification// Communications of ACM. – 1995. – Vol.42, №4. – P.857-907.

Hansson H., Jonsson B. A Logic for Reasoning about Time and Reliability// Formal Aspects of Computing. – 1994. – №6(5). – P.512-535.

Subrahmanian V. S., Bonatti P., Dix J., et al. Heterogeneous Agent Systems. – Cambridge MA: MIT Press, 2000.

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

Dix J., Nanni M., Subrahmanian V.S. Probabilistic Agent Reasoning// ACM Transactions of Computational Logic. – 2000. –№1(2). – P.201-245.

Ng R., Subrahmanian V.S. Probabilistic Logic Programming//Information and Computation. – 1993. – Vol.101, №2. – P.150-201.

Dekhtyar A., Dekhtyar M.I. Revisiting the Semantics of Interval Probabilistic Logic Programs// Proceedings 8th International Conference on Logic Programming and Non-Monotonic Reasoning (LPNMR'05), LNAI. – 2005. – Vol.3662. – P.330-342.

Baier C., Katoen J. Principles of Model Checking. – Cambridge MA: MIT Press, 2008.

Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. – М.: МЦНМО, 2002.

Dekhtyar M.I., Dikovsky A.Ja., Valiev M.K. On Сomplexity of Verification of Interacting Agents’ Behavior// Annals of Pure and Applied Logic. – 2006. – №141. – P.336-362.




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