О ВЕРИФИКАЦИИ ДИНАМИЧЕСКИХ СВОЙСТВ СИСТЕМ ВЗАИМОДЕЙСТВУЮЩИХ АГЕНТОВ*

М.Ю.Бурмистров1, М.К.Валиев2, М.И.Дехтярь1, А.Я.Диковский2

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

Введение

Системы взаимодействующих между собой интеллектуальных программных агентов представляют собой одно из самых активно развивающихся направлений в искусственном интеллекте и прикладном программировании (см., например, [Fisher et al., 1993], [Subrahmanian et al., 2000], [Тарасов, 2002]). Состояния отдельных агентов в таких системах могут быть достаточно сложными, и эти состояния изменяются агентами по достаточно сложным правилам в зависимости от сообщений, получаемых ими от других агентов и внешней среды. Это делает поведение таких систем достаточно сложным и приводит к необходимости проверки соответствия их поведения требуемым условиям (верификации их динамических свойств). Конечно, в общем случае такая проблема неразрешима, поэтому мы рассматриваем эту проблему при разных ограничениях на вид агентов и класс проверяемых свойств. Вообще говоря, в литературе имеются различные варианты понятий агента и многоагентной (МА-) системы. Используемое нами здесь определение агента в значительной степени базируется на архитектуре IMPACT из [Subrahmanian et al., 2000], однако для облегчения исследования в него введены некоторые упрощения. В данной работе приводится краткий обзор полученных нами результатов (см. [Dekhtyar et al., 2003], [Dekhtyar et al., 2006], [Dekhtyar et al., 2002]) по оценке сложности решения проблемы верификации МА-систем при различных ограничениях; некоторые из этих оценок полиномиальны. В заключительном разделе обсуждаются некоторые возможности распространения полученных результатов на другой тип МА-систем.

Агенты и многоагентные системы

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

Агенты общаются между собой посредством передачи сообщений вида msg(Sender, Receiver, Msg), где Sender и Receiver – имена агентов (источника и адресата), a Msg - (передаваемый) базисный атом. Агент A посылает сообщения другим агентам системы, передавая их агенту P, и получает сообщения от агента P в свой почтовый ящик. При этом можно рассматривать два способа работы: 1) синхронный, когда предполагается, что P передает сообщение адресату сразу (в этом случае агент P фактически можно исключить из системы), и 2) асинхронный, когда передача сообщения от P к агентам может занять произвольное количество времени. Синхронные МА-системы больше подходят для описания практических систем, работающих в рамках локальной сети (или в отдельном компьютере), в асинхронных МА-системах лучше отражаются свойства сильно распределенных (например, в Интернете) систем.

Состояние агента P содержит все сообщения, полученные им и не отосланные до текущего момента. Текущие содержимые внутренней БД и почтового ящика агента A составляют его текущее локальное состояние IM_A = <I_A,MsgBox_A>. Глобальное состояние МА-системы A состоит из локальных состояний агентов A_i и состояния почтового агента.

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

Конкретный выбор этих действий для выполнения в зависимости от локального состояния агента определяется парой < Pr_A , Sem_A> . Здесь Pr_A – интеллектуальная компонента, определяющая совместно с фактами из локального состояния агента в текущий момент t набор фактов о потенциально возможных в данный момент действиях. В качестве таких компонент могут выступать обычные логические программы [Apt, 1990], в сигнатуру которых включены атомы действий. Правила таких программ имеют вид H :- L₁,...,L_n, где H – атом действия; литералы L_i – либо литералы действия, либо (экстенсиональные) литералы с предикатами из сигнатуры внутренней БД, либо литералы сообщений вида msg(Sender, A, Msg) или not msg(Sender, A, Msg), либо некоторые вычислимые в полиномиальное время встроенные предикаты. Такой вариант программ рассматривался нами в работах [Dekhtyar et al., 2003], [Dekhtyar et al., 2006].

Другой более общий вариант интеллектуальных компонент агентов представляют так называемые деонтические логические программы (ср. [Subrahmanian et al., 2000]). Такие программы отличаются от обычных логических программ тем, что они вместо обычных атомов действий используют атомы статусов действий вида Da(t₁,…,t_m) (содержательно, статусы действий – это “действие разрешено”, “действие обязательно”и т.д.). Здесь D – некоторая деонтическая модальность одного из видов Do, P (“permitted”), F (“forbidden”), O (“obliged”), W (“waived”), a – имя действия, t₁,…,t_m – либо константы, либо переменные.

Приведем в качестве примера следующее простое правило:

Oc :- Pa,Fb,p,

смысл которого выражается как “если локальная база содержит факт p, действие a разрешено и действие b запрещено, то действие c обязательно”.

Агент называется позитивным, если его программа не содержит отрицаний.

Мы предполагаем, что программы агентов безопасны в том смысле, что 1) любая переменная, встречающаяся в левой части некоторого правила, имеет положительное вхождение в правую часть соответствующего правила, и 2) программа Pr_A^state, полученная добавлением к Pr_A фактов из локального состояния state (внутренней БД и почтового ящика) агента A, является стратифицированной [Apt, 1990].

При указанных условиях любая деонтическая (как и обычная) программа определяет однозначно множество Facts, состоящее из фактов о действиях, которые выводятся по ее правилам из фактов локального состояния агента. Для обычных программ факты из Facts – это базисные имена действий, и Sem_A выбирает (детерминированно или недетерминированно) из Facts подмножество ActDo фактически выполняемых на данном шаге действий.

Для деонтической программы Pr_A семантическая (вообще говоря, недетерминированная) функция Sem_A носит более сложный характер и допускает различные формальные уточнения (см. [Subrahmanian et al., 2000]). Все они опираются на понятие непротиворечивого и замкнутого множества базисных атомов статуса действий, определяемого, исходя из интуитивного смысла деонтических модальностей.

Множество S базисных атомов статуса действий называется деонтически непротиворечивым, если выполнены условия: 1) если Oa содержится в S, то Wa не содержится в S, 2) если Pa содержится в S, то Fa не содержится в S

Множество S базисных атомов статуса действий называется деонтически замкнутым, если выполнены условия: 1) если Oa содержится в S, то Do a содержится в S, 2) если Do a содержится в S, то Pa содержится в S.

Множество S базисных атомов статуса действий называется допустимым относительно программы Pr_A и состояния state, если

1) S замкнуто относительно оператора, задаваемого однократным применением правил из Pr_A^state;

2) S деонтически замкнуто и непротиворечиво.

Для данной программы Pr_A и состояния state может быть как одно, так и несколько множеств S, допустимых относительно них (может быть и ни одного). Не все из них осмысленны. Разные определения семантики Sem_A соответствуют разным осмысленным вариантам (если возможно) выбора допустимых множеств S и множества ActDo как множества действий a таких, что Do a принадлежит S. Если выбирается несколько допустимых множеств, мы имеем недетерминированную семантику. Недетерминированность в семантику можно ввести и другими способами.

К сожалению, определение этих вариантов семантики довольно громоздко, и мы не можем их привести здесь. Для наших целей здесь достаточно указать, что все эти семантики вычислимы в полиномиальной емкости, а некоторые – за полиномиальное время.

Пусть ActDo (= ActDo_t) - множество фактически выполняемых на данном шаге t действий, выбранное в соответствии с Sem_A. Тогда все действия из ActDo выполняются параллельно следующим образом. Пусть ADD_ActDo равно объединению всех множеств ADD_a(c₁,…,c_m) таких, что базисное имя a(c₁,…, c_m) из ActDo унифицируется с параметризованным именем a(X₁,…, X_m). Аналогично определяются множества DEL_ActDo и SEND_ActDo. Тогда следующее состояние внутренней БД агента A получается из текущего состояния удалением элементов из DEL_ActDo и добавлением элементов из ADD_ActDo. Кроме того, к базе почтового агента добавляются все элементы из SEND_ActDo, а почтовый ящик агента A опустошается. Конечно, можно рассматривать и другие стратегии добавлений и удалений из внутренней БД и почтового ящика.

Действие называется расширяющим, если его удаляющее множество пусто. Агент называется расширяющим, если все его действия расширяющие.

Напомним, что глобальное состояние S^t МА-системы A в момент t определяется как n-ка локальных состояний ее агентов A₁,...,A_n совместно с состоянием почтового агента.

Приведенные определения одношаговой семантики отдельных агентов естественным образом расширяются до семантики Sem_A всей МА-системы A, определяющей преобразования ее глобальных состояний. А именно, на каждом шаге работы системы все агенты изменяют свои внутренние состояния в соответствии со своей одношаговой семантикой и передают свои сообщения почтовому агенту. Кроме того, из состояния почтового агента удаляются некоторые (или все) сообщения вида msg(sender,receiver,msg), которые добавляются к почтовым ящикам соответствующих агентов-адресатов.

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

В соответствии с вышеприведенными определениями любая МА-система A с каждым начальным глобальным состоянием S⁰ связывает дерево T_A(S⁰) возможных траекторий системы (в детерминированном случае – одну траекторию). Узлы этого дерева помечены глобальными состояниями системы, причем каждый узел, находящийся на (t+1)-ом уровне и помеченный состоянием S, связан с узлом на t-ом уровне, из пометки которого есть переход в состояние S по семантике Sem_A.

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

Наличие реляционной структуры в состояниях агентов и определение переходов с помощью логических программ делает естественным рассмотрение предикатных расширений временных логик в качестве языков описания динамических свойств МА-систем.

Мы используем некоторые варианты предикатных расширений следующих пропозициональных логик: логики линейного времени LTL, простых подмножеств ALTL и ELTL классической логики ветвящегося времени, существенно более богатого mu-исчисления (Mu) и его подмножеств с ограничениями на глубину альтернирования (Mu_r|r=1,2,…) [Clarke et al., 2000]. Для предикатного расширения логики L будем использовать обозначение FO-L (FO - “first order”).

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

Базис-ные	Расшир.	Параметры	Логика	Сложность
Да	Да	m^2 ·r = O(log |A|)	$LTL	NP –полна
			"LTL	CoNP-полна
		m агентов, фиксир. m > 1	FO-m1	EXPTIME-полна
		r сигналов, фиксир. r > 0	FO-m1	EXPTIME-полна
	Нет		FO-md фиксир. d	EXPTIME-полна
			FO-m	в NEXPTIME Ç coNEXPTIME
Нет	Да	r сигналов, фиксир. r > 0	$LTL	NEXPTIME-полна
			"LTL	CoNEXPTIME-полна
	Нет	k-мерна, фиксир. k	FO-m	EXPTIME-полна
			FO-md фиксир. d	EXPEXPTIME-полна
			FO-m	в NEXPEXPTIME Ç coNEXPEXPTIME

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

В детерминированном случае сложность соответствующих проблем существенно ниже. В частности, в [Dekhtyar et al., 2003] установлены полиномиальные оценки временной сложности проблемы MA-Behavior при определенных ограничениях на тип МА-систем и используемую логику.

Моделирование AgentSpeak-агентов IMPACT-агентами

В литературе известны и другие архитектуры агентов и МА-систем. У многих из них интеллектуальные компоненты устроены по принципу разделения информации на части, связанные с понятиями «убеждения», «желания» и «намерения» (так называемые BDI-агенты). Такие агенты используются в системе AgentSpeak [Rao, 1996].

Такой агент состоит из программы (набора планов) и 3 функций вы- бора (статическая часть). Состояние агента на каждом шаге задается множеством событий, набором стеков намерений, набором убеждений (фактов внутренней БД) и набором выполняемых действий.

Работа агента, кратко говоря, выглядит так: возникают и накапливаются некоторые события (факты). Затем из множества событий выбирается одно для последующей обработки. Для этого события подбираются планы, которые можно применить для реакции на него. Затем из множества таких планов выбирается один, и на его основе производится обновление набора стеков намерений. Если событие было внешним, то создается новый стек, если оно внутреннее, то на вершину стека, соответствующего этому событию, помещается тело выбранного плана. Затем функция выбора намерения выбирает один стек для последующей обработки. Обработка состоит в исполнении части тела плана, находящейся на вершине стека. При этом может происходить возникновение нового события, обновление БД убеждений, изменение выбранного стека (в нем может произойти замена переменных на их значения из БД) и выполнение некоторого воздействия на среду.

Проблема верификации для AgentSpeak-систем рассматривалась в литературе. В частности, в [Bordini et al., 2003] было показано, как для этого может быть использована система SPIN [Holtzmann, 1997], изначально предназначенная для верификации параллельных и распределенных императивных программ. В [Валиев и др., 2004] мы рассмотрели возможность использования системы SPIN для верификации некоторых динамических свойств МА-систем рассмотренного выше типа IMPACT, выражаемых в логике линейного времени.

В выпускной работе первого из авторов (Тверской госуниверситет) построен алгоритм моделирования AgentSpeak-агентов IMPACT-агентами. Этот алгоритм имеет полиномиальную сложность, и размер результирующего агента линеен по отношению к размеру исходного. Это позволяет перенести некоторые результаты о сложности верификации, установленные в [Dekhtyar et al., 2003], [Dekhtyar et al., 2006], на AgentSpeak-системы. Отметим, что в работах других авторов по верификации AgentSpeak-систем вопросы сложности не рассматривались.

Список литературы

[Валиев и др., 2004] Валиев М.К., Китаев Е.Л., .Дехтярь М.И., .Голубков В.В., Молоканов Э.А. Использование системы SPIN для проверки динамических свойств многоагентных систем// Труды Международных научно-технических конференций "Интеллектуальные системы (IEEE AIS'04)" и "Интеллектуальные САПР (CAD-2004)", т. I., М., Физматлит, 2004.

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

[Apt, 1990] 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.

[Bordini et al., 2003] Bordini, R.H., Fisher, M., Pardavila, C., Wooldridge, M.: Model checking AgentSpeak.// Proc. of the Second International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS’03), 2003.

[Clarke et al., 2000] Clarke E.M., Grumberg O., and Peled D., Model Checking - MIT Press, 2000.

[Dekhtyar et al., 2003] Dekhtyar M., Dikovsky A., and Valiev M., On Feasible Cases of Checking Multi-Agent Systems Behavior// Theoretical Computer Science, Elsevier Science, 2003, vol. 303, no. 1.

[Dekhtyar et al., 2006] Dekhtyar M., Dikovsky A., and Valiev M.,On complexity of verification of interacting agents’ behavior// Annals of Pure and Applied Logic, 2006, v. 141, no 3.

[Dekhtyar et al., 2002] Dekhtyar M.I., Dikovsky A.Ja., Valiev M.K., Checking Multi-Agent Systems Behavior Properties// Proc. of IEEE Intern. Conf. On Artif. Intelligent Systems (ICAIS2002), Divnomorskoe, Russia, 2002, 5-10 Sept..

[Fisher et al., 1993] Fisher M., Wooldridge M., Specifying and Verifying Distributed Intelligent Systems// Lect. Notes in AI, no.727, 1993, Springer-Verlag: Berlin.

[Holtzmann, 1997] Holzmann G.J. The model checker SPIN// IEEE Transactions jn Software Engineering, 1997, v. 23, № 5.

[Rao, 1996] A.S. Rao. AgentSpeak (L): BDI agents speak out in a logical computable language// Lect. Notes in AI, no.1038, 1996, Springer-Verlag, Berlin.

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

---

* Эта работа выполнена при поддержке РФФИ (гранты 04-01-00565 и 04-01-00015).

1 170000, Тверь, ул. Желябова 33, ТвГУ, Michael.Dekhtyar@tversu.ru

2 125047, Москва, Миусская пл. 4, ИПМ РАН, valiev@keldysh.ru