О верификации динамических свойств систем взаимодействующих агентов

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

О верификации динамических свойств систем взаимодействующих агентов

М.Ю.Бурмистров, М.К.Валиев,

М.И.Дехтярь, А.Я.Диковский

Аннотация

верификация динамический интеллектуальный агент

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

Введение

Системы взаимодействующих между собой интеллектуальных программных агентов представляют собой одно из самых активно развивающихся направлений в искусственном интеллекте и прикладном программировании (см., например, [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 = {A1,...,An; P} состоит из конечного множества {A1,...,An} интеллектуальных агентов с общей предикатной сигнатурой и специального почтового агента P, моделирующего сеть связей между агентами Ai. У интеллектуального агента A имеется внутренняя база данных (БД) IA, содержащая конечное множество базисных атомов (т.е. выражений вида p(c1,…, ck), где p-предикатный символ, c1,…, ck - константы, причем множество используемых данной системой констант ограничено), и почтовый ящик MsgBoxA.

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

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

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

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

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

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

Oc :- Pa,Fb,p,

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

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

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

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

Для деонтической программы PrA семантическая (вообще говоря, недетерминированная) функция SemA носит более сложный характер и допускает различные формальные уточнения (см. [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 базисных атомов статуса действий называется допустимым относительно программы PrA и состояния state, если

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

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

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

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

Пусть ActDo (= ActDot) - множество фактически выполняемых на данном шаге t действий, выбранное в соответствии с SemA. Тогда все действия из ActDo выполняются параллельно следующим образом. Пусть ADDActDo равно объединению всех множеств ADDa(c1,…,cm) таких, что базисное имя a(c1,…, cm) из ActDo унифицируется с параметризованным именем a(X1,…, Xm). Аналогично определяются множества DELActDo и SENDActDo. Тогда следующее состояние внутренней БД агента A получается из текущего состояния удалением элементов из DELActDo и добавлением элементов из ADDActDo. Кроме того, к базе почтового агента добавляются все элементы из SENDActDo, а почтовый ящик агента A опустошается. Конечно, можно рассматривать и другие стратегии добавлений и удалений из внутренней БД и почтового ящика.

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

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

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

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

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

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

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

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

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