О сложности поведения систем взаимодействующих агентов1

Валиев М.К.
Институт прикладной математики им. М.В.Келдыша РАН
Дехтярь М.И.
Тверской государственный университет
Диковский А.Я.
Институт прикладной математики им. М.В.Келдыша,
Нантский университет

Анноиация:

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

The complexity is investigated, of the properties of interacting intelligent agents' behavior, expressible in the first order logic of linear time. Some tight complexity bounds for such properties are established under certain restrictions on the classes of agent programs.


Введение

При построении сложных программных систем все больше используются технологии, основанные на понятии программных агентов. Агенты используются при построении систем искусственного интеллекта, работы в Интернете и т.д. Имеются различные подходы к архитектуре и построению агентов. Обзор многих из этих подходов содержится в книге В.Субраманяна и др.  [12]. Эта книга также содержит подробное рассмотрение некоторого теоретического подхода к определению и исследованию вычислений, основанных на использовании агентов, и некоторых методов их построения. Этот подход отличается от многих других подходов своей ориентацией на логическое описание агентов. В нашей статье мы в основном следуем понятиям из  [12], однако в связи с ограничениями на объем, используем их в несколько упрощенном виде.

Многие важные теоретические проблемы, связанные с программными агентами, уже были предметом интенсивных исследований, но, тем не менее, все еще остается ряд не менее существенных проблем, не привлекших пока достаточного внимания исследователей. Одна из таких проблем - это сложностной анализ поведения систем взаимодействующих агентов. Подобные проблемы активно изучались для параллельных программ (см., например,  [8,10]). Результаты этих исследований неприменимы непосредственно к системам агентов, рассматриваемым в данной работе, которые ближе с семантической точки зрения к динамическим дедуктивным базам данных (ДДБД). Сложностные проблемы для ДДБД рассматривались нами в  [4,5,6], и наш подход здесь к анализу поведения систем агентов близок к подходу, использованному в этих работах.

Другой логический подход к описанию систем агентов содержится в  [1], где представлены три различные модели: так называемые I/O-автоматы, среда программирования Erdös, основанная на понятиях из теории представления знаний, и некоторое расширение $\pi$-исчисления Милнера. В среде Erdös поведение систем агентов специфируется в пропозициональной временной логике CTL, и эти спецификации верифицируются с помощью проверки истинности формул (model checking) на моделях CTL. Среди работ других авторов этот подход кажется наиболее близким к подходу, используемому в данной работе.

Еще один логический подход к системам агентов связан с языком Concurrent Metatem  [2,9]. В этом случае агенты описываются с помощью формул линейной временной логики, и для верификации динамических свойств систем агентов используется метод резолюции, адаптированный к временной логике.

В настоящей работе мы рассматриваем поведение системы $\mathcal{A}$ из $n$ агентов, общающихся между собой с помощью сообшений. На каждом шаге работы каждый агент выполняет некоторое подмножество действий в зависимости от своего внутреннего состояния и полученных сообщений. В результате этих действий он изменяет свое внутреннее состояние и посылает сообщения другим агентам. Говоря неформально, архитектура агента включает в себя (i) внутренние структуры данных (базу данных), определяющие внутреннее состояние агента, (ii) a почтовый ящик, содержащий сообщения от других агентов, (iii) ограничения целостности на состояния агента, (iv) базу действий, которые агент может выполнить, и (v) программу, определяющую политику выполнения действий. Выполнение действия состоит из (a) изменения текущего состояния пгента и (b) посылки сообщений другим агентам. Текущее содержание почтового ящика состоит из сообщений, полученных агентом от других агентов на предыдущем шаге. Глобальное состояние системы состоит из внутренних состояний и содержимых почтовых ящиков всех агентов системы.

Пошаговая семантика системы $\mathcal{A}$ описывается как детерминированный оператор переходов над глобальными состояниями. Таким образом, для каждого начального глобального состояния $S$ поведение системы $\mathcal{A}$ задается в терминах единственной траектории, определяемой последовательностью переходов глобальных состояний, начиная с $S$.

В настоящей работе мы изучаем сложность алгоритмических проблем, связанных с анализом поведения систем агентов. Одна из наиболее важных проблем такого типа - это проблема инвариантности (safety problem), т.е. сохранения некоторого свойства начального состояния $S$ на всех состояниях траектории, начинающейся с $S$. Другая интересная проблема - это проблема достижимости цели, т.е. выяснения того, попадет ли система в состояние, удовлетворяющее заданному свойству. Для систематического рассмотрения динамических свойств систем агентов в качестве языка спецификации мы используем некоторую версию первопорядковой логики линейного времени (FLTL) без функциональных символов. Подобные логики широко используются как средство формальной спецификации и верификации параллельных программ (см. [8,10]).

Общая алгоритмическая проблема (AGENT_BEHAVIOR), которую мы рассматриваем, формулируется следующим образом: для данной системы $\mathcal{A}$ , ее начального глобального состояния $S$ и FLTL-формулы $\Phi$ выяснить, выполняется ли $\Phi$ на траектории системы
$\mathcal{A}$ , начинающейся с $S$. Для этой проблемы мы устанавливаем некоторые точные оценки сложности при некоторых ограничениях на классы программ-агентов.

Эта проблема представляет собой вариант хорошо известной проблемы проверки на моделях, широко используемой при верификации параллельных программ (см. [8,3]). Обычно проверка на моделях выполняется в два этапа. Вначале параллельная система $C$ преобразуется в недедетерминированный автомат (transition system) $T$, и после этого фактическая проверка на моделях применяется к $T$. Размер $T$ может существенно (в общем случае экспоненциально) вырасти относительно размера $C$. В настоящей работе мы показываем, что в ряде случаев вместо явного полного построения $T$ можно ограничиться ее построением по частям, что позволяет существенно понизить верхние оценки сложности проблемы AGENT_BEHAVIOR по сравнению с обычными подходами к проверке на моделях.

Взаимодействующие интеллектуальные агенты

Определение понятия агента, используемое в настоящей работе, в основном следует работе  [12]. Конечно, архитектура IMPACT для систем агентов, введенная в этой книге, слишком сложна для представления в короткой статье. Кроме того, некоторые ее особенности не имеют значения при анализе сложности поведения этих систем. Поэтому мы представляем здесь несколько упрощенное по сравнению с  [12] определение агентов. В частности, мы не рассматриваем средств, связанных с включением в архитектуру обычных программ (legacy code), средств обеспечения безопасности, метазнания и рассуждений в условиях неопределенности. В качестве внутренних структур агентов мы используем реляционные базы данных (в архитектуре IMPACT допускаются более общие структуры) и для описания политики действий агентов используем обычные логические программы (в IMPACT программы агентов могут включать деонтические модальности "разрешенное действие", "обязательное действие" и т.д.).

Система агентов в настоящей статье - это система $\mathcal{A}$, состоящая из $n$ взаимодействующих агентов $ a_1,...,a_n$ . Формальное определение $\mathcal{A}$ включает три конечные предикатные сигнатуры: экстенсиональная сигнатура ${\bf P}_e$, используемая для представления фактов внутренней базы данных, сигнатура сообщений ${\bf P}_m$ и интенсиональная сигнатура ${\bf P}_{act}$, используемая для представления действий агентов. Кроме этого, с $\mathcal{A}$ связаны конечные множества переменных ${\bf V}$ и констант ${\bf C}$. Через ${\bf A}_e, {\bf A}_m$ и ${\bf A}_{act}$ мы обозначаем множества атомов над соответствующими предикатными сигнатурами, ${\bf V}$ и ${\bf C}.$ Через ${\bf B}_e, {\bf B}_m$ и ${\bf B}_{act}$. Также мы обозначаем соответствующие множества базисных атомов, через ${\bf LB}_e, {\bf LB}_m$ и ${\bf LB}_{act}$ соответствующие множества базисных литералов.

Структуры данных у агентов. Каждый агент $ a \in \mathcal{A}$ обладает собственными внутренними структурами данных. Мы считаем, что эти данные имеют вид некоторой реляционной базы данных со схемой ${\bf P}_e$. Текущее состояние обозначается $I_a.$

Сообщения. Агенты из $\mathcal{A}$ общаются с помощью сообщений. Сообщения - это базисные факты (атомы) в сигнатуре ${\bf P}_m$. Каждый агент $a$ имеет буфер (почтовый ящик) $MsgBox_a$, содержащий сообщения, получаемые им от других агентов. Элементы в $MsgBox_a$ - это пары вида $(Source\_agent, Message),$ где $Source\_agent$ - имя агента, пославшего сообщение. Пару $(I_a, MsgBox_a)$ мы называем локальным состоянием агента $a$.

Ограничения целостности. С каждым агентом $a$ ассоциировано некоторое множество ограничений целостности, задающее некоторое свойство состояний его базы данных. Ограничения целостности могут быть представлены формулами, логическими программами или обычными программами, распознающими это свойство. Мы предполагаем, что существует алгоритм, проверяющий ограничение целостности $IC_a$ в состоянии $I_a$, используя полиномиальный относительно $\vert I_a\vert + \vert IC_a\vert$ объем памяти.

Действия. С каждым агентом ассоциировано некоторое множество действий. Действие представляется атомом $\alpha(X_1,..., X_l),$ где $\alpha^{(l)}$ - предикат в сигнатуре ${\bf P}_{act}$, $X_i$ - различные переменные. и тремя (возможно, пустыми) множествами атомов с переменными из $\{X_1,..., X_l\}$ :
$ADD(\alpha)$ - список фактов из ${\bf A}_e$, добавляемых к $I_a$;
$DEL(\alpha)$ - список фактов из ${\bf A}_e$, удаляемых из $I_a$;
$SEND(\alpha)$ - список пар вида $(destination\_agent, Msg),$ где $Msg \in {\bf B}_m$.

Параллельное выполнение действий. Пусть $AS=\{\alpha_1(\bar{T_1}),...,\alpha_k(\bar{T_k} )\}$ $\subseteq {\bf B}_{act}$ - множество базисных действий агента $a$ и $\bar{\sigma}=$ $(\sigma_1,...,\sigma_k)$- список базисных подстановок таких, что $ \sigma_j(\alpha_j(\bar{X_j}) )=\alpha_j(\bar{T_j} )$. Параллельное выполнение множества действий $\bar{\sigma}(AS)$ в локальном состоянии $(I_a, MsgBox_a)$ определяется следующим образом:
a) новое внутреннее состояние $a$ получается из текущего состояния присваиванием

\begin{displaymath} I_a:= ((I_a \setminus \bigcup_{j=1}^k \sigma_j( DEL(\alpha_j)) ) \cup \bigcup_{j=1}^k \sigma_j( ADD(\alpha_j) )).\end{displaymath}

(Таким образом, когда некоторый факт должен быть удален и добавлен, он добавляется. Конечно, другие стратегии разрешения конфликтов тоже возможны, например, когда удаление и добавление взаимно аннигилируют);
b) любое сообщение, порождаемое множеством $\bar{\sigma}(AS)$ помещается в буфер $MsgBox$ агента назначения Более точно, для любого агента $b\neq a $

\begin{displaymath}MsgBox_{b}:=MsgBox_{b}\cup \bigcup_{j=1}^k \{(a,\sigma_j (Msg)) \vert (b,Msg) \in SEND(\alpha_j) \} .\end{displaymath}

Программа агента Программа $P_a$ определяет политику выполнения действий агентом $a$ и представляет собой логическую программу с предложениями вида

\begin{displaymath}H \leftarrow L_1,...,L_n,\end{displaymath}

где голова $H$ - (интенсиональный) атом действия из ${\bf A}_{act}$, а литералы $L_i$ - либо атомы из ${\bf A}_{act},$ либо (экстенсиональные) литералы из ${\bf LB}_e,$ либо литералы сообщений вида $Received(Source\_agent, Message)$ или $\neg Received(Source\_agent, Message)$, где $Message \in {\bf A}_m$.

Семантика программ определяет множество действий, выполняемых агентом в его текущем локальном состоянии. Семантика $Sem(P_a)(I_a,MsgBox_a) $ программы $P_a$ относительно состояния $I_a$ и состояния буфера $MsgBox_a$ определяется как минимальная эрбранова модель программы $P_a\cup I_a\cup \{Received(Agent\_source,Message) \vert $ $ (Agent\_source,$ $Message)\in MsgBox_a\}.$
Очевидно, рассматриваемые здесь логические программы являются нормальными программами без рекурсии через отрицание, т.е. очень специальным случаем стратифицируемых логических программ. Как хорошо известно, любая такая программа имеет единственную минимальную модель, которая может быть вычислена за полиномиальное время, используя простую процедуру вычисления неподвижной точки. Фактически, приводимые в этой работе сложностные результаты верны для любых подклассов нормальных логических программ, для которых существует единственная минимальная модель, вычислимая в полиномиальное время, например, для стратифицируемых логических программ.

Глобальное состояние системы агентов $\mathcal{A}$ в момент $t$ определяется как $n$-ка локальных состояний агентов $ a_1,...,a_n$, т.е. $ S^t = <(I_{a_1}^t,MsgBox_{a_1}^t),$ $..., (I_{a_n}^t,MsgBox_{a_n}^t)>.$

Детерминированная одношаговая семантика системы агентов $\mathcal{A}$ определяется как оператор $\Rightarrow$ переходов глобальных состояний системы, который мы представляем в виде следующего алгоритма, преобразующего глобальное состояние $S^t$ в следующее глобальное состояние $S^{t+1}:$

(1) ДЛЯ ЛЮБОГО $a_i \in \mathcal{A}$ ВЫПОЛНИ $ Acts_i^t := Sem(P_{a_i})(I_{a_i}^t, MsgBox_{a_i}^t)$;
(2) ДЛЯ ЛЮБОГО $a_i \in \mathcal{A}$ ВЫПОЛНИ $ MsgBox_{a_i}^{t+1} := \emptyset;$
(3) ДЛЯ ЛЮБОГО $a_i \in \mathcal{A}$ ВЫПОЛНИ
ЕСЛИ $IC_{a_i}$ не нарушено выполнением действий $Acts_i^t$
ТО выполни $Acts_i^t$ параллельно в локальном состоянии $(I_{a_i}^t,MsgBox_{a_i}^{t+1}).$

Таким образом, в итоге содержание почтового ящика агента $a$ в момент $t+1$ состоит из всех сообщений, посланных агенту $a$ другими агентами в момент $t$.

Поведение системы агентов $\mathcal{A}$ для начального глобального состояния $ S^0 =$
$ <(I_{a_1}^0,MsgBox_{a_1}^0),..., (I_{a_n}^0,MsgBox_{a_n}^0)>$ описывается как следующая бесконечная последовательность глобальных состояний, $\tau = \tau( \mathcal{A} ,S^0):$
$<(I_{a_1}^0,MsgBox_{a_1}^0),..., (I_{a_n}^0,MsgBox_{a_n}^0)> \Rightarrow$ ...
$<(I_{a_1}^t,MsgBox_{a_1}^t),..., (I_{a_n}^t,MsgBox_{a_n}^t)> \Rightarrow$
$<(I_{a_1}^{t+1},MsgBox_{a_1}^{t+1}),..., (I_{a_n}^{t+1},MsgBox_{a_n}^{t+1})> \Rightarrow ... $
где глобальное состояние на шаге $t+1$ получается из предыдущего состояния применением оператора перехода. Эту последовательность мы называем траекторией системы $\mathcal{A}$ в состоянии $S^0.$

Это определение гарантирует локальную совместность поведения системы агентов.

Лемма 1   Пусть $\tau$ - траектория системы $\mathcal{A}$ в состоянии $S^0$. Тогда, если для некоторого $j, 1\leq j\leq n,$ начальное локальное состояние $I^0_{a_j}$ агента $a_j$ удовлетворяет ограничению $ IC_{a_j},$ то состояние $I^t_{a_j}$ также удовлетворяет ограничению $IC_{a_j}$ для любого $t >0$.

Пример. Рассмотрим следующую игрушечную систему распределения ресурсов $\mathcal{A},$ состоящую из агента-менеджера $m,$ который владеет некоторыми ресурсами и распределяет их среди четырех агентов-пользователей $u_1, u_2, u_3 $ и $ u_4$. У каждого из пользователей имеется собственная стратегия запроса ресурсов:
1) $u_1$ запрашивает ресурс в первый момент и затем всякий раз повторяет свой заказ после того, как будет выполнен предыдущий;
2) $u_2$ запрашивает ресурс непосредственно после того, как запрашивает $u_1$ ;
3) $u_3$ запрашивает ресурс непосредственно после того, как $u_1$ получает ресурс ;
4) $ u_4$ запрашивает ресурс в каждый момент времени.
Менеджер $m$ ведет список заказов и в каждый момент времени выполняет первый заказ из этого списка. Только один заказ каждого пользователя может присутствовать в списке заказов $m$. Поэтому, если $m$ получает заказ некоторого пользователя до того, как был выполнен его предыдущий заказ, то этот новый заказ игнорируется.

Система $\mathcal{A}$ задается следующим образом. Состояние $I_{u_1}$ агента $u_1$ может содержать факт $put\_order$, а состояния $I_{u_i} (i=2,3,4)$ остальных пользователей всегда пусты. База данных $I_m$ агента $m$ содержит факты вида:
1) $ order(X,I) $ - $order(u_i,j)$ означает, что заказ агента $u_i$ находится на $j$-ом месте в списке заказов $m,$
2) $is(X)$ - заказ пользователя $X$ содержится в списке $m,$
3) $num\_orders(I)$ - число невыполненных заказов равно $I$.

Чтобы сообщить $m$ и другим пользователям о своем заказе $u_i$ посылает им сообщение $order$. Когда $m$ выполняет заказ $u_i$, он посылает $u_i$ сообщение $ok$. Когда $u_1$ хочет информировать $u_3$ об очередном получении ресурса от $m,$ он посылает $u_3$ сообщение $ok$.

Агент $u_1$. Действия:
$do\_order: ADD=\{put\_order\}, SEND=\{(m,order), (u_2,order)\};$
$receive\_order: DEL=\{put\_order\}, SEND=\{(u_3,ok) \}$;
$P_{u_1}:$
$do\_order \leftarrow \neg put\_order $
$receive\_order \leftarrow Received(m,ok) $

Агент $u_2$. Действия:
$do\_order: SEND=\{(m,order)\};$
$P_{u_2}:$
$do\_order \leftarrow Received(u_1, order)$

Агент $u_3$. Действия:
$do\_order: SEND=\{(m,order)\};$
$P_{u_3}:$
$do\_order \leftarrow Received(u_1, ok) $

Агент $ u_4$. Действия:
$do\_order: SEND=\{(m,order)\};$
$P_{u_4}:$
$do\_order \leftarrow .$

Агент $m$. Действия:
$ins\_order(X,I): ADD=\{order(X,I),is(X)\}; $
$fulfill\_order(X): DEL=\{order(X,1), is(X)\}, SEND=\{(X,ok)\};$
$move(X,I): ADD=\{order(X,I)\}, DEL =\{order(X,I+1)\}$;
$new\_num(I,J): ADD= \{num\_orders(J)\}, DEL=\{num\_orders(I)\}$
$P_{m}:$
$new\_order(X) \leftarrow Received(X,order), \neg is(X)$
$first\_place(I)\leftarrow num\_orders(I), I>0$
$first\_place(1)\leftarrow num\_orders(0)$
$ins\_order(X,I)\leftarrow new\_order(X),first\_place(I) (X\in \{u_1,u_2\})$
$ins\_order(u_3,I) \leftarrow new\_order(u_3), ins\_order(X, I-1) (X\in \{u_1,u_2\}$
$ins\_order(u_3,I)\leftarrow new\_order(u_3),first\_place(I), \neg ins\_order(u_1,I),$
$\neg ins\_order(u_2,I)$
$ins\_order(u_4,I) \leftarrow new\_order(u_4), ins\_order(u_3, I-1)$
$ins\_order(u_4,I) \leftarrow new\_order(u_3),\neg ins\_order(u_3,I-1),$
$ins\_order(X, I-1) (X\in \{u_1,u_2\})$
$ins\_order(u_4,I)\leftarrow new\_order(u_3),first\_place(I), \neg ins\_order(u_1,I),$
$\neg ins\_order(u_2,I), \neg ins\_order(u_3,I-1)$
$fulfill\_order(X) \leftarrow order(X,1)$
$move(X,1) \leftarrow fulfill\_order, order(X,2)$
$move(X,I) \leftarrow move(Y,I-1),order(X,I+1)$
$new\_num(I,J) \leftarrow num\_orders(I),num\_new\_orders(K), J=I+K$

Вначале БД менеджера $m$ содержит только фактt $num\_orders(0)$. Затем на каждом шаге предикат $new\_order(X)$ проверяет, нужно ли включать в список заказ агента $X$, Предикат $first\_place(I)$ определяет то место $I$ в списке, на которое должен быть помещен очередной заказ, $ins\_order$ вставляет новые заказы в конец списка (при конкуренции используется порядок: $u_1<u_2<u_3<u_4$), $fulfill\_order$ посылает ресурс первому агенту из списка, $move$ сдвигает все элементы списка на l ``влево'', а $new\_num(I,J)$ определяет новое значение $I$ для $num\_orders(I)$, добавляя к прежнему число $K$ новых незарегистрированных ранее сообщений из $MessageBox_m.$ Это число $K$ вычисляется не определяемым здесь предикатом $num\_new\_orders$.

Свойства поведения агентов и временная логика

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

Язык FLTL определяется как замыкание множества формул состояний (первого порядка) относительно булевых связок и временных операторов ``пока'' ( ``until", $U$) и ``в следующий момент'( ``nexttime", $\circ$). Сигнатура формул состояний включает предикат равенства и множество $ \bigcup_1^n {\bf P}_e^i \cup \{ Received^{(3)}\},$ где $Received^{(3)}$ - это имя предиката $Received(Source\_agent,$ $Target\_agent, Message)$, а ${\bf P}_e^i$ обозначает множество символов предикатов экстенсиональной сигнатуры $\mathcal{A}$ , проиндексированной номерами агентов $i$. Термами этого языка являются либо переменные, либо константы из множества D. Мы предполагаем, что D включает все константы, встречающиеся в программах агентов, их состояниях и почтовых ящиках. Моделями FLTL служат траектории систем агентов. Истинность формулы в модели определяется поточечно, т.е. на каждом глобальном состоянии траектории.

Пусть $\tau = \tau( \mathcal{A} ,S^0)$ - некоторая траектория $\mathcal{A}$ , $ S^t =<(I_{a_1}^t,MsgBox_{a_1}^t),...,\\ (I_{a_n}^t,MsgBox_{a_n}^t)>$ - некоторое глобальное состояние траектории $\tau$, $p^i$ - $k$-местный предикатный символ из ${\bf P}_e^i$ и $c_1,...c_k$ - некоторые константы из D. Тогда базисный атом $p^i(c_1,...,c_k)$ истинен в $<\tau,S^t>$ (обозначение: $\tau,S^t \models p^i(c_1,...,c_k)$) тогда и только тогда, когда $p^i(c_1,...,c_k) \in I_{a_i}^t$.

Пусть $m$ - это $k$-местный предикатный символ из ${\bf P}_m$. Тогда атом $ Received(a_i,a_j, $ $m(c_1,...,$ $c_k))$ истинен в $<\tau,S>$ тогда и только тогда, когда $(a_i,m(c_1,...,c_k)) \in MsgBox_{a_j}^t$. Семантика булевых связок, кванторов по объектным переменным и временных операторов определяется обычным образом. Например, $\tau,S^t \models \Phi U \Psi , если и только если \quad \exists t'\geq t $ такое, что $ \tau,S^t \models \Psi $ и для всех $ t'' (t \leq t''\leq t'), \tau,S^{t''} \models \Phi$. Ниже в примере мы будем также использовать обычные временные операторы $\Box$ (``всегда в будущем") и $\Diamond$ (``когда-нибудь в будущем"), которые выразимы в этой логике. Временная логика FLTL, которую мы рассматриваем в этой работе, отличается от обычных пропозициональных временных логик тем, что в ней используются базисные формулы состояний первого порядка вместо пропозициональных символов. Это может, конечно, приводить к увеличению сложности проверки истинности формул. Хорошо известно, например, что проблема проверки истинности замкнутой формулы первого порядка на модели является PSPACE-полной. Поэтому имеет смысл выделить в FLTL естественный специальный случай, когда базисные формулы состояний не содержат объектных переменных. При таком ограничении мы, фактически, получаем логику, эквивалентную пропозициональной линейной временной логике LTL, для которой будем использовать такое же обозначение.

В общем виде проблема AGENT_BEHAVIOR проверки свойств поведения системы агентов, которую мы рассматриваем в этой работе, формулируется следующим образом: для заданной системы агентов $\mathcal{A}$ , ее начального глобального состояния $S^0$ и FLTL-формулы $\Phi$ выяснить верно ли, что $ \tau( \mathcal{A} ,S^0),S^0 \models \Phi$.

В частности, вышеуказанные проблемы безопасности и достижимости цели являются частными случаями AGENT_BEHAVIOR, в которых $\Phi$ имеет форму $\Box \Psi$ (соответственно, $\Diamond \Psi$) для соответствующей формулы состояний $\Psi.$ Мы рассматриваем также некоторые другие подклассы общей проблемы AGENT_BEHAVIOR, которые получаются при некоторых ограничениях, накладываемых на программы агентов (например, отсутствие переменных), их действия (отсутствие удалений), сигнатуры (ограниченность количества и арности предикатов).

Пример (продолжение). Для определенной выше системы $\mathcal{A}$ можно установить истинность следующих формул на траектории, порожденной $\mathcal{A}:$
$\Box\Diamond Received(m,u_i,ok)$ (каждый агент-пользователь получает ресурс бесконечное число раз), $\Box \forall I \forall X\forall Y ($ orders $(X,I) $ $ \& orders(Y,I) \rightarrow X=Y)$ (в каждый момент только один заказ может быть на каждом месте списка заказов). Следующие две формулы оказываются на этой траектории ложными: $\Diamond (Received(m,u_1,ok) \& \circ Received(m,u_1,ok))$ (имеются два последовательных момента времени, в которые $u_1$ получает заказанный ресурс) и $\Box (orders(u_i,2) \rightarrow$ $\circ\circ\neg Received(m,u_i,ok)). $

Нетрудно понять, что рассматриваемая проблема AGENT_BEHAVIOR является некоторым вариантом известной проблемы проверки на модели (model checking problem) для модели $\tau( \mathcal{A} ,S^0)$, неявно заданной системой агентов $\mathcal{A}$ и начальным состоянием $S^0$.

Поскольку $\mathcal{A}$ детерминированная система и множество ее глобальных состояний конечно, то траектория $\tau( \mathcal{A} ,S^0)$ является периодической. Следовательно, хотя $\tau( \mathcal{A} ,S^0)$ задает бесконечную модель, ее можно свернуть в некоторую конечную псевдомодель. Проблема проверки истинности FLTL-формул на таких псевдомоделях разрешима. Непосредственная реализация стандартного алгоритма проверки на модели потребовала бы явного представления всей псевдомодели и, следовательно, используемая память по меньшей мере равнялась бы суммарному размеру всех глобальных состояний этой модели. Однако, как показано ниже, в нашем случае существует более эффективный способ проверки правильности формул, который просматривает псевдомодель ``поточечно''. Это позволяет получить существенно лучшие верхние оценки сложности для проблемы AGENT_BEHAVIOR.

Назовем траекторию $\tau= S^0,S^1,...,S^t,... $ периодической, если найдутся два числа $k$ и $N$ такие, что для всякого $t \geq k, $ справедливо равенство $ S^t= S^{t+N}$. Обозначим через $F^\tau$ функцию-оракул, которая по любому моменту времени $t.$ возвращает состояние $F^\tau(t)=S^t$ траектории $\tau$.

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

Лемма 2   Существует алгоритм, который по заданным числам $k$ и $N$ и FLTL-формуле $\Phi$ проверяет условие $ \tau, S^0 \models \Phi $ для периодической траектории $\tau$ с параметрами $k$ и $N,$ используя $F^\tau$ в качестве оракула, с емкостью памяти $pol(\vert\Phi\vert+\log (k+N)+ \max\{\vert S^t\vert \vert 0\leq t\leq k+N\}) $ для некоторого полинома $pol$.

Оракул $F^\tau$ из этой леммы можно эффективно вычислять для траекторий $\tau,$ порождаемых системами агентов.

Лемма 3   Существует алгоритм, который по системе агентов $\mathcal{A}$ , начальному состоянию $S^0$ и моменту времени $t\geq 0$ вычисляет состояние $S^t$ траектории $\tau( \mathcal{A} ,S^0)$ с емкостью памяти $pol(\vert \mathcal{A} \vert+ \max\{\vert S^r\vert \vert 0\leq r\leq t\}) $ для некоторого полинома $pol$.

Следующая лемма показывает, что траектории систем агентов являются периодическими и дает оценки параметров этих траекторий.

Лемма 4   Для всякой системы агентов $\mathcal{A}$ и ее начального состояния $S^0$ траектория $\tau( \mathcal{A} ,S^0)$ является периодической с параметрами $k( \mathcal{A} ,S^0)$ и $N( \mathcal{A} ,S^0)$. Если $\mathcal{A}$ базисная, то $k( \mathcal{A} ,S^0) + N( \mathcal{A} ,S^0)\leq 2^{\vert \mathcal{A} \vert+\vert S^0\vert}.$ В общем случае $k( \mathcal{A} ,S^0) + N( \mathcal{A} ,S^0)\leq 2^{2^{\vert \mathcal{A} \vert+\vert S^0\vert}}.$

Из лемм  2, 3 и 4 можно извлечь верхние оценки сложности проверки свойств поведения систем агентов, выразимых в FLTL.

Предложение 1   Пусть для системы агентов $\mathcal{A}$ и ее начального состояния $S^0$ $k=k( \mathcal{A} ,S^0) $ и $ N=$ $N( \mathcal{A} ,S^0)$. Тогда существует алгоритм, проверяющий истинность произвольной FLTL-формулы $\Phi$ на траектории $\tau( \mathcal{A} ,S^0)$ с емкостью памяти $pol(\vert\Phi\vert+\log(k+N))+\vert \mathcal{A} \vert+$ $\max\{\vert S^t\vert $ $\vert 0\leq t\leq k+N\}) $ для некоторого полинома $pol$.


Сложность разрешения свойств поведения

В этом разделе мы формулируем ряд результатов, характеризующих сложность проверки FLTL-свойств на траекториях, задаваемых системами агентов. Эта сложность существенно зависит от типа рассматриваемой системы. Выделим некоторые естественные подклассы систем. Система агентов $\mathcal{A}$ является
- базисной, если программы ее агентов не содержат переменных;
- расширяющей, если в действиях ее агентов не допускаются удаления из баз данных;
- позитивной, если в программах ее агентов нет отрицаний;
- $m$-агентной, если число ее агентов не превосходит $m$;
- $k$ -сигнальной, если сигнатура сообщений ${\bf P}_m$ содержит не более $k$ пропозициональных символов (сигналов).
Укажем вначале два случая, в которых проблема AGENT_BEHAVIOR допускает решение за полиномиальное время. В обоих случаях проверяемые свойства принадлежат LTL, а входящие в системы базисные агенты могут лишь аккумулировать информацию в своих внутренних базах данных.

Теорема 1   Проблема AGENT_BEHAVIOR разрешима за полиномиальное время для выразимых в LTL свойств

1) в классе базисных, расширяющих, позитивных систем агентов;

2) в классе базисных, расширяющих, $m$-агентных, $k$-сигнальных систем агентов $\mathcal{A}$ таких, что $m*k = O(\log \vert \mathcal{A} \vert)$.

Если ослабить ограничения в классе из пункта (2) этой теоремы, то временная сложность увеличивается, но требуемая память остается линейной.

Теорема 2   Проблема AGENT_BEHAVIOR является LIN-SPACE-полной (относительно сводимости за полиномиальное время и с линейным растяжением) для свойств, выразимых в LTL,

1) в классе базисных, расширяющих, $m$-агентных систем агентов (для каждого фиксированного $m$);

2) в классе базисных, расширяющих, $k$-сигнальных систем агентов (для каждого фиксированного $k$).

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

Теорема 3   В классе базисных, расширяющих систем агентов, как и в классе базисных систем агентов, проблема AGENT_BEHAVIOR является PSPACE-полной.

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

Теорема 4  

1) В общем случае проблема AGENT_BEHAVIOR является EXPSPACE-полной.

2) В классе расширяющих, позитивных систем агентов проблема AGENT_BEHAVIOR является EXPTIME-полной.

3) В случае, когда арности всех предикатов в сигнатурах ${\bf P}_e$ и ${\bf P}_m$ ограничены некоторой (произвольной) константой, проблема AGENT_BEHAVIOR является PSPACE-полной .


Заключение

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

Хотя используемая нами модель агентов несколько проще, чем модель предложенная в [12], наши основные результаты могут быть легко распространены и на эту более общую модель, поскольку различные семантики для выполнения одного шага, предложенные в этой монографии, могут быть вычислены с использованием памяти полиномиального размера (см. [7]).

В этой работе рассмотрен класс автономных, синхронных и детерминированных систем агентов. В будущем мы предполагаем изучить также поведение недетерминированных, асинхронных и реактивных систем агентов.

Литература

1
Araragi T., Attie P., Keidar I., et al., On Formal Modeling of Agent Computations. In NASA Workshop on Formal Approaches to Agent-Based Systems. April, 2000.

2
Barringer H., Fisher M., Gabbay D., Gough G., and Owens R. METATEM: An Introduction. Formal Aspects of Computing, 7:533-549, 1995.

3
Clarke E.M., Grumberg O. and Peled D. Model Checking, MIT Press, 2000.

4
Dekhtyar M.I., Dikovsky A.Ja.   Dynamic Deductive Data Bases with Steady Behavior. In Proc. of the 12th International Conf. on Logic Programming, (Ed. L. Sterling), The MIT Press, 183-197, 1995.

5
Dekhtyar M.I., Dikovsky A.Ja.   On Homeostatic Behavior of Dynamic Deductive Data Bases. In: Proc. 2nd Int. A.P.Ershov Memorial Conference "Perspective of Systems Informatics", Lect. Notes in CS, N 1181, 1996, 420-432.

6
Dekhtyar M.I., Dikovsky A.Ja., Valiev M.K. Applying temporal logic to analysis of behavior of cooperating logic programs. Lect. Notes in CS, N 1755, 2000, 228-234.

7
Eiter T., Subrahmanian V.S. Heterogeneous Active Agents, II: Algorithms and Complexity. Artificial Intelligence, 108(1-2), 1999, 257-307.

8
Emerson E.A. Temporal and modal logic. In "Handbook of Theor. Comput. Sci.", Ed. J. van Leeuwen, Elsewier Sci. Publishers, 1990.

9
Fisher M., Dixon C., Peim M. Clausal temporal resolution, ACM Transactions on computational logic, 2001, 2(1).

10
Manna Z., Pnueli A. The temporal logic of reactive and concurrent systems: Specification. Springer Verlag, 1991.

11
Sistla A.P., Clarke E.M. The complexity of propositional linear temporal logic. J.ACM, 32(3), 1985, 733-749.

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

Примечание

... агентов 1
Эта работа выполнена при поддержке РФФИ (гранты 01-01-00278 и 00-01-00254)
Ваши комментарии
[SBRAS]
[Головная страница]
[Конференции]
[СО РАН]

© 2001, Сибирское отделение Российской академии наук, Новосибирск
© 2001, Объединенный институт информатики СО РАН, Новосибирск
© 2001, Институт вычислительных технологий СО РАН, Новосибирск
© 2001, Институт систем информатики СО РАН, Новосибирск
© 2001, Институт математики СО РАН, Новосибирск
© 2001, Институт цитологии и генетики СО РАН, Новосибирск
© 2001, Институт вычислительной математики и математической геофизики СО РАН, Новосибирск
© 2001, Новосибирский государственный университет
Дата последней модификации Monday, 10-Sep-2001 21:26:14 NOVST