ПРОГРАММИРОВАНИЕ, 2009, № 5, с. 37-56
■ ТЕСТИРОВАНИЕ, ВЕРИФИКАЦИЯ И ВАЛИДАЦИЯ ПРОГРАММ
УДК 004.92+004.94
СИСТЕМЫ АГЕНТОВ, УПРАВЛЯЕМЫХ ЛОГИЧЕСКИМИ ПРОГРАММАМИ: СЛОЖНОСТЬ ВЕРИФИКАЦИИ
© 2009 г. М. К. Валиев*, М. И. Дехтярь**, А. Я. Диковский***
* Институт прикладной математики им. М.В. Келдыша РАН 125047 Москва, Миусская пл., 4 ** Тверской государственный университет 170013 Тверь, ул. Желябова, 3 ***Нантский университет 2 rue de la Houssiniere, BP 92208, 44322 Nantes Cedex 3 France E-mail: valiev@spp.keldysh.ru, Michael.Dekhtyar@tversu.ru, Alexandre.Dikovsky@irin.univ-nantes.fr Поступила в редакцию 17.10.2008 г.
В статье рассматривается сложность проблемы верификации поведения (динамических свойств) систем взаимодействующих интеллектуальных агентов. Она продолжает наши публикации [1-3], в которых эта проблема в основном обсуждалась для детерминированных и недетерминированных систем, и больше концентрируется на асинхронных системах.
1. ВВЕДЕНИЕ
Понятия интеллектуального агента и системы взаимодействующих агентов (короче, мультиа-гентной системы, МА-системы или MAC) были введены более двух десятков лет назад, и их изучение и использование представляет собой одно из самых активно развивающихся направлений в искусственном интеллекте и прикладном программировании (см., например, [4-10]). Одним из существенных факторов, способствовавших проявлению такого интереса к агентам, явилось развитие сетевых технологий (в частности, связанных с Интернетом).
Понятие агента существенно обобщает понятие объекта из области объектно-ориентированного программирования за счет введения интеллектуальных компонент, определяющих политику выполнения действий агентом в зависимости от его состояния и сообщений, получаемых от других агентов системы и внешней среды. При этом состояние агента может иметь достаточно сложную структуру, например, включать в себя некоторую базу данных. Все это делает поведение таких систем достаточно сложным
и приводит к необходимости проверки соответствия их поведения требуемым условиям (верификации их динамических свойств). Конечно, в общем случае такая проблема неразрешима, поэтому мы рассматриваем эту проблему (мы называем ее MA-BEHAVIOR) при разных ограничениях на вид агентов и класс проверяемых свойств. Заметим, что, хотя понятия агентов и MAC активно изучались в течение ряда лет, работы по верификации их поведения были начаты сравнительно недавно [1, 11-15].
Мультиагентные системы имеют широкую сферу применений, включающую такие разные области, как управление бизнес-процессами, электронная торговля, Интернет-навигация, социальные и военные приложения и т.д. Такое разнообразие приложений привело к появлению многочисленных различных подходов к определению понятий агента и MAC (использующих, к тому же, разные уровни абстракции от конкретных систем). При этом разные архитектуры агентов отличаются в основном устройством их интеллектуальных компонент, которые могут использовать деревья решений, логические программы, выводы в различных ви-
дах модальной логики (эпистемической, деонтической и др.) и т.д. Обзоры многих из этих подходов даны в вышеупомянутых ссылках.
Используемое нами определение агента в значительной степени базируется на архитектуре IMPACT, введенной и подробно описанной в [9]1. Полное определение этой архитектуры весьма громоздко. Оно включает в себя различные довольно сложные механизмы и средства спецификации агентов, что делает их хорошо приспособленными к практическим приложениям. Однако, в то же время, такое обилие различных механизмов сильно усложняет формальное изучение свойств таких агентов. В частности, как показано в [9], семантика агентов архитектуры IMPACT, описанная в терминах переходов состояний, является в общем случае малоэффективной. Чтобы сделать семантику переходов вычислимой за полиномиальное время, в [17] (см. также [9]) были определены некоторые очень сложные ограничения на вид агентов. К сожалению, определение таких агентов становится совсем уж трудно воспринимаемым.
Мы предлагаем некоторые другие достаточно легко формулируемые ограничения на IMPACT-агенты, которые также ведут к семантике полиномиальной сложности. При этом мы фокусируемся на средствах, связанных с определением действий, политики принятия решений и коммуникации агентов. Таким образом, мы отвлекаемся от деталей IMPACT-архитектуры, связанных с агентизацией обычного программного кода, безопасностью, структурами метазнания, временными и вероятностными рассуждениями. Кроме того, в качестве состояний агентов мы рассматриваем базы фактов (аналог реляционных баз данных), в отличие от [9], где допускаются более общие структуры состояний. Заметим, что даже при этих ограничениях архитектура MAC остается достаточно представительной, и большая часть примеров из [9] укладывается в ограниченную таким образом архитектуру.
Агенты могут быть детерминированными или недетерминиронными, а взаимодействие агентов в MAC может быть синхронным или асинхрон-
1 Заметим, что рассматривемые здесь агенты существенно отличаются от агентов в смысле [16].
ным. Синхронные системы детерминированных агентов для каждого своего начального состояния определяют некоторую траекторию вычисления. В остальных трех случаях система для начального состояния определяет некоторое дерево возможных траекторий вычисления.
В первом случае для описания динамических свойств системы естественно использовать логику, основанную на линейности времени, а в остальных случаях - те или иные варианты логики ветвящегося времени.
Рассматриваемая нами проблема МА-ВЕНА-VIOR, которая состоит в проверке выполнимости некоторой формулы временной логики на траекториях данной MAC, фактически соответствует той проблеме, которая под названием model checking (проверка на моделях программ) изучается уже ряд лет для абстрактных систем (диаграмм) переходов (см. [18-24]). Однако имеется существенное различие между классической постановкой этого вопроса и рассматриваемым нами вариантом. Традиционно, сложностные результаты устанавливаются для диаграмм с неструктурированными состояниями и явно заданными переходами (или других аналогичных систем типа конечных автоматов или OBDD). В MAC же состояния могут иметь сложную структуру (у нас - это базы фактов), а переходы от одних состояний к другим определяются некоторыми программами. Это позволяет оценивать сложность проблемы верификации, основываясь на различных структурных и семантических свойствах систем.
MAC определяют компактное представление систем переходов. В частности, даже в случае базисных (т.е. не использующих переменных) MAC определяемая ею система переходов может иметь экспоненциальный размер относительно исходной MAC. Поэтому иногда наши нижние оценки выглядят более пессимистичными, чем для классического случая с теми же используемыми логиками. Что касается верхних оценок, иногда они более информативны и точны (в случаях, когда получены детерминированные или недетерминированные полиномиальные верхние оценки), или они получаются простой трансляцией классических оценок, принимая в расчет изменения размера при переходе от MAC к определяемой ею системе переходов.
Дальнейшая часть работы организована следующим образом. Раздел 2 содержит основные определения. В разделе 3 приводится некоторый пример, иллюстрирующий возможности рассматриваемых нами MAC. Раздел 4 содержит описание алгоритма верификации детерминированных MAC из [2], который используется в разделе 6 для построения недетерминированного алгоритма, решающего проблему верификации для некоторого класса асинхронных MAC за полиномиальное время. В разделе 5 дается обзор результатов из [2, 3], касающихся сложности верификации различных классов детерминированных и недетерминированных MAC (в виде таблиц 1 и 2). Раздел 6 содержит, кроме упомянутого выше результата, еще результаты о взаимном сведении проблемы MA-BEHAVIOR для недетерминированных и асинхронных MAC. Заключение содержит краткое резюме полученных результатов и некоторое обсуждение проблематики.
2. АГЕНТЫ И МНОГОАГЕНТНЫЕ СИСТЕМЫ
МА-система А = {ai,..., ап] Р} состоит из конечного множества {ai,...,ап} интеллектуальных агентов с общей предикатной сигнатурой и специального почтового агента Р, моделирующего сеть связей между агентами аг-. У интеллектуального агента А имеется внутренняя база данных (БД) 1а, содержащая конечное множество базисных атомов (т.е. выражений вида p(ci,..., Cjt), где р - предикатный символ, ci,...,cjt - константы, причем множество используемых данной системой констант ограничено), и почтовый ящик MsgBoxA-
Агенты общаются между собой посредством передачи сообщений вида msg (Sender, Receiver, Msg), где Sender и Receiver - имена агентов (источника и адресата), a Msg - (передаваемый) базисный атом. Агент А посылает сообщения другим агентам системы, передавая их агенту Р, и получает сообщения от агента Р в свой почтовый ящик. При этом можно рассматривать два способа работы: 1) синхронный, когда предполагается, что Р передает сообщение адресату сразу (в этом случае агент Р фактически можно исключить из системы), и 2) асинхронный, ко-
гда передача сообщения от Р к агентам может занять произвольное количество времени. Синхронные МА-системы больше подходят для описания практических систем, работающих в рамках локальной сети (или в отдельном компьютере), в асинхронных МА-системах лучше отражаются свойства сильно распределенных (например, в Интернете) систем.
Состояние агента Р содержит все сообщения, полученные им и не отосланные до текущего момента. Текущие содержимые внутренней БД и почтового ящика агента А составляют его текущее локальное состояние 1Ма = = <1а, М здВохдУ. Глобальное состояние МА-си-стемы А состоит из локальных состояний агентов аг- и состояния почтового агента.
С каждым агентом а связана его база АВа параметризованных действий вида < а(Ад,..., Хт), АВРа(Х I,.. .,Хт), РЕЬа(Х1,..., Хт), 8ЕХВа{Х1,...,Хт)>, где а{Хъ .. .,Хт) определяет параметризованное имя действия. АВВа(Х1,...,Хт) и ВЕЬа(Х1,...,Хт) - списки атомов вида р(Ь\,..., tk), где р - к-местный предикат из сигнатуры в
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.