автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Разработка и реализация методов формально-логической спецификации самонастраивающихся мультиагентных систем с временными ограничениями

САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

На правах рукописи

Бугайченко Дмитрий Юрьевич

РАЗРАБОТКА И РЕАЛИЗАЦИЯ МЕТОДОВ

ФОРМАЛЬНО-ЛОГИЧЕСКОЙ

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

05 13 11 — Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

Санкт-Петербург 2007

003158 (Ига

003158792

Работа выполнена на кафедре информатики математико-механическо-го факультета Санкт-Петербургского государственного университета

Научный руководитель кандидат физико-математических наук,

доцент Соловьев Игорь Павлович

Официальные оппоненты доктор физико-математических наук,

профессор Баранов Сергей Николаевич

кандидат физико-математических наук, доцент, Кознов Дмитрий Владимирович

Ведущая организация Санкт-Петербургский институт инфор-

матики и автоматизации РАН

[ а " /2007 года в_часов нг

Защита диссертации состоится " "_/2007 года в_часов на

заседании диссертационного совета Д212 232 51 по защите диссертаций на соискание ученой степени доктора наук при Санкт-Петербургском государственном университете по адресу 198504, Санкт-Петербург, Старый Петергоф, Университетский пр , д 28, математико-механичес-кий факультет Санкт-Петербургского государственного университета

С диссертацией можно ознакомиться в Научной библиотеке Санкт-Петербургского государственного университета по адресу 199034, Санкт-Петербург, Университетская наб , д 7/9 4

Автореферат разослан " ^ "_2007 г

Ученый секретарь диссертационного совета доктор физико-математических наук, профессор

^ ^ Мартыненко

Общая характеристика работы

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

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

Частично проблему корректности помогает решить тщательное и обширное тестирование, но оно обладает тем же недостатком — поведение системы обычно проверяется только в тех условиях, которые запланированы человеком В случае действительно сложных систем полное тестирование, проверяющее все возможные комбинации условий, как правило, невозможно за разумное время

Представляется, что решение данной проблемы следует искать на пути применения методов формальной спецификации проектируемой системы с последующим автоматическим тестированием или верификацией (обычно это проверка модели или model checking)

Основу большинства методов формальной спецификации составляет некоторый вариант темпоральной логики Наиболее широкое распространение получила логика ветвящегося времени CTL [16], основным достоинством которой является билинейная относительно размера спецификации и размера модели системы сложность задачи верификации CTL расширяет классическую логику высказываний темпоральными

операторами "в следующий момент ф" ОФ и "когда-нибудь ф, а до тех пор ф" фЫф и кванторами "на любом пути " А и "существует путь на котором " Е

Для спецификации систем с временными ограничениями предложены различные расширения логики CTL Например, логика RTCTL [22] расширяет CTL ограниченным оператором ф U <t0, интерпретируемым как "не более чем через t шагов ф, а до тех пор ф' Основным достоинством RTCTL является сохранение билинейной сложности задачи верификации Большей выразительной мощности, за счет увеличения вычислительной сложности, можно достичь введя переменные часов (х, у, ) и квантор фиксации ( ) [12] х А ф U ((х < t) Л ф)

Основным ограничением CTL является отсутствие явных средств спецификации систем, состоящих из нескольких взаимодействующих сущностей Это ограничение преодолевается в логике альтернированного времени ATL [13], позволяющей учитывать многокомпонентность системы в явном виде ATL включает конечное множество игроков-агентов Р и заменяет кванторы CTL на квантор "для коалиция игроков С С Р существует такая стратегия, что на любом пути " ((C)) Для ATL также были предложены методы спецификации ограничений на время реакции, например, с помощью подстрочного индекса [19] или с помощью переменных часов [18]

Характерной чертой многих методов формальной верификации является комбинаторный взрыв пространства состояний верифицируемых систем Частично эту проблему позволяют решить так называемые символические (symbolic) алгоритмы, которые оперирует с множествами состояний, а не с отдельными состояниями Серьезный толчок к развитию символических алгоритмов дало введение ориентированных булевых разрешающих диаграмм (OBDD) [14], позволяющих относительно компактно представлять большие множества и эффективно выполнять над ними операции Было предложено множество различных модификаций концепции OBDD, среди которых можно выделить алгебраические разрешающие диаграммы (ADD) [11]

Для уменьшения времени реакции системы широко используется подход исполняемых планов [17] В этом случае до начала непосредственного взаимодействия с внешней средой система составляет план действий для достижения своих целей Существует множество различных алгоритмов планирования, используемых для мультиагентных систем, часть из которых базируется на классических алгоритмах поиска пути в графе А* [20] Однако подобные алгоритмы также подвержены проблеме комбинаторного взрыва пространства состояний, частично решить которую позволяют алгоритмы символического планирования [15]

Описанные выше алгоритмы позволяют строить планы для дости-

жения относительно простых целей, например, достижение системой определенного состояния при посещении только допустимых состояний В работе [21] были предложены алгоритмы для решения более сложной задачи — построения плана, удовлетворяющего спецификации, описанной с помощью логики линейного времени1 Подобный подход получил название "планирование с темпорально расширенными целями"

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

Из вышесказанного следует, что разработка и реализация методов формально-логической спецификации мультиагентных систем с ограничениями на время реакции, а также реализация алгоритмов планирования и накопления опыта для таких систем, является весьма актуальной задачей

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

• Метод формально-логической спецификации мультиагентных систем с временными ограничениями Далее соответствующий формализм именуется МАБЬ

• Алгоритм верификации систем по спецификации МАЯЬ

• Алгоритм построения мультиагентных планов с темпорально расширенными целями, выраженными в ограниченном варианте логики МАБЬ, обеспечивающем эффективную реализацию

• Метод накопления и анализа опыта для мультиагентных систем

Методы исследования. В диссертации используются теория и методы современной математической логики, включая модальные и темпо-

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

ральные логики, методы формально-логической спецификации, а также метод символических алгоритмов, основанных на представлении множеств с помощью разрешающих диаграмм

Научная новизна. Научная новизна работы заключается в следующем

• Предложена новая математическая модель интеллектуального агента, позволяющая описывать такие аспекты деятельности агента как неполнота информации, планирование, накопление опыта, управляемое целями поведение и взаимодействие с другими агентами

• Разработан новый логический формализм МАБЬ, позволяющий в удобном виде описывать свойства коалиций агентов и обладающий рядом преимуществ по сравнению с существующими формализмами

• Разработаны новые алгоритмы построения планов в ограничениях МАБЬ, позволяющие строить планы для случая нескольких потенциально конкурирующих агентов в условиях недетерминированного взаимодействия с внешней средой

• Предложены новые методы накопления и анализа опыта агентов, использующие символическое представление опыта в виде разрешающих диаграмм

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

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

• системы автоматического перемещения грузов,

• автономные исследовательские зонды,

• системы управления автоматизированным производством,

• системы автоматического поиска предметов и обхода территории

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

1 Конференция Технологии Microsoft в теории и практике, Россия, Санкт-Петербург, 2004

2 Конференция Технологии Microsoft в теории и практике, Россия, Санкт-Петербург, 2006

3 Международная конференция Процессы управления и устойчивость, Россия, Санкт-Петербург, 2006

4 Международной конференция Современные проблемы информатизации, Россия, Воронеж, 2006

5 Международная конференция Процессы управления и устойчивость, Россия, Санкт-Петербург, 2007

6 Семинар Санкт-Петербургской ассоциации искусственного интеллекта, Россия, Санкт-Петербург, 2007

7 Семинар Санкт-Петербурского института информатики и автоматизации РАН, 2007

8 The 5th International Central and Eastern European Conference on Multi-Agent Systems, Germany, Leipzig, 2007

9 Семинар кафедры информатики математико-механического факультета Санкт-Петербургского государственного университета, Россия, Санкт-Петербург, 2007

Структура и объем диссертации. Диссертация состоит из 8-ми глав, включая введение, заключение и приложение, а также списка литературы из 187 наименований Объем основной части работы — 172 страницы, полный объем работы — 260 страниц

Содержание работы

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

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

Глава 1 начинается с введения основных понятий и рассмотрения основных свойств, присущих интеллектуальному агенту В главе 2 описана модель интеллектуального агента, представленного как набор ад = (S,A,env,see,lB,bel, brf,lD,des,drf,plan,prf), где

• S есть непустое конечное множество состояний внешней среды,

• А есть непустое конечное множество действий агента,

• env S х А —» 2s есть функция поведения внешней среды, сопоставляющая текущему состоянию внешней среды и выбранному агентом действию множество возможных следующих состояний внешней среды Таким образом, действия агента могут влиять на окружающую среду, но не контролировать ее полностью,

• see С. S у. S есть корректное восприятие агентом состояний внешней среды, задающее множество Р классов эквивалентности на

S,

• 1в = Ibei х 2Ру'А/Р есть множество представлений агента,

• bel € 1в есть множество текущих представлений агента,

• brf 1в х А х Р —> 1в есть функция обновления представлений,

• Ip = I,ies х 2Coal есть множество желаний агента, где Goal есть множество всех возможных функций-критериев,

• des 6 Ip есть множество текущих желаний агента,

• drf Id х Р —> Id есть функция обновления желаний,

• plan = (Р, A, Ipin, (Jpin, ipin,o) есть текущий план агента, представленный конечным автоматом с входным алфавитом Р, выходным алфавитом А, множеством состояний Ivi„, отношением переходов apin и начальным состоянием гр(п,о,

• prf Ib^Id* 2plan х Р —» 2plan есть функция обновления плана, где Plan есть множество всех возможных планов

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

Ключевым понятием, введенным в главе 3, является понятие коалиции как набора совместно действующих агентов Формально коалиция моделируется как единый агент, возможные действия, представления, желания и намерения которого являются объединение соответствующих характеристик входящих в коалицию агентов Полученные в главах 2 и 3 результаты были опубликованы в работах [5, 6, 7, 2]

В главе 4 вводится формальная логика спецификации свойств интеллектуального агента, объединяющая возможности пропозициональной динамической логики PDL и логики ветвящегося времени RTCTL и расширенная следующими дополнительными операторами

• Bel ф — оператор, используемый для описания представлений агента Семантика этого оператора задается с помощью возможных миров, определяемых восприятием агента see С S х S и представлениями агента bel С Р х Ах. Р

• Des ф — оператор, используемый для описания желаний агента Семантика этого оператора задается относительно структуры желаний агента des

• Intend ф — оператор, используемый для описаний намерений агента Семантика этого оператора задается с помощью возможных миров, определяемых восприятием see, представлениями bel и планом plan агента

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

В главе 5 предлагаются символические алгоритмы верификации для логики спецификации интеллектуального агента, а также способы символического представления модели интеллектуального агента с использованием разрешающих диаграмм Доказаны корректность и полнота этих алгоритмов, а также то, что их алгоритмическая сложность не превосходит полинома от длины формулы и размера модели

В главе 6 работы предлагается формальная логика MASL, предназначенная для описания свойств мультиагентной системы с временными ограничениями способной к накоплению и анализу опыта Логика MASL расширяет логику спецификации интеллектуального агента для случай мультиагентной системы В этой логике вводится квантор коалиции ((A))ф, указывающий на то, что интерпретацию формулы ф следует проводить относительно формальной модели коалиции А как единого агента Полученные в главах 4 , 5 и 6 результаты были опубликованы в работах [8, 3, 9, 1, 10] Рассмотрим несколько примеров описания свойств мультиагентной системы

• {(А)) А Сф — коалиция А ведет себя таким образом, что на любом пути всегда выполнено свойство ф Такие свойства называют свойствами безопасности

• -ф => А О(Ф ((-В)}Bel (ip =>• Е Оф)) — если из состояния, удовлетворяющего ф, система перейдет в состояние, удовлетворяющее ф, то коалиция В будет знать, что такой переход возможен

• ((A)) A G (Des ф =>■ А Т <юф) — коалиция А ведет себя таким образом, что на любом пути всегда при возникновении у нее желания реализовать ф не более чем через 10 тактов ф будет реализовано Такие свойства называют свойствами живучести

• ((A))Des ф A Bel ЕТф => Intend ф — если коалиция А хочет реализовать свойство ф и считает, что существует путь, на котором оно может быть реализовано, то она будет пытаться реализовать это свойство

• А С(АТ<1вф)/\(АТ <1в~<ф) — система в целом ведет себя таким образом, что свойства ф и ф чередуются с периодом не более 16 тактов

• ((C))lntend ф ATф — если коалиция С решила реализовать свойство ф, то она этого когда-нибудь добьется

В главе 7 предлагаются символические алгоритмы мультиагентно-го планирования в ограничениях MASL Входными данными для алгоритма планирование являются описание модели мультиагентной системы и набор формул MASL Результатом алгоритма является план, представленный моделью взаимодействующих конечных автоматов2,

2 Модель взаимодействующих конечных автоматов является одним из возможных расширений модели конечных автоматов Для взаимодействующего конечного автомата, помимо входного и выходного алфавита, определены множества входящих и исходящих сигналов, а также каналы связи, перенаправляющие исходящие сигналы одного автомата во входящие сигналы другого автомата

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

Наиболее интересным является этап построения общего плана, на котором изначальный план, не накладывающий никаких ограничения на действия агента, постепенно уточняется для каждой из подформул формулы-цели через исключение действий, опровергающих эту подформулу Для уточнения плана используется техника аналогичная технике символической верификации через поиск неподвижной точки При этом, в отличии от алгоритмов верификации, после построения плана для формулы в целом производится уточнение плана для подформул с учетом ограничений, накладываемых общим планом Благодаря тому, что план может уточняться параллельно для нескольких формул, возможна распределенная реализация планирующего алгоритма Доказаны корректность и завершаемость предложенных алгоритмов, кроме того, доказано, что их алгоритмическая сложность не превосходит полинома от размера модели и экспоненты от длины формулы Полученные в главе 7 результаты были опубликованы в работе [4]

В главе 8 предлагается новый подход к решению задачи накопления опыта системой, использующий символическое представление данных в виде разрешающих диаграмм Опыт агента представляются в виде функции res S х ACS x S —> N (где ACS есть декартово произведение множеств действий всех агентов системы, а N есть множество натуральных чисел), представленной с помощью разрешающих диаграмм Результат функция res в точке (s, a, s') G Sx ACSx S описывает сколько раз результатом выполнения системой в состоянии s € S действия а € ACS являлось состояние s' s S

Для предложенного представления опыта описаны такие операции как добавления факта, интеграции опыта нескольких агентов, а также получение описания представлений агента bel С S х ACS x S, построенного с использованием порога отсечения в G [0,1] следующим образом bel = {(s, a, s') € S х ACS x S | res(s,a,s') > 9 maxres(s,a1s')}

s'€S

Кроме того, предложен ряд методов анализа опыта, оптимизации представления и построения обобщений проекция редукции разрешающей диаграммы bel на исходную разрешающую диаграмму res, расширенная редукция схожих относительно некоторого критерия ситуаций, а также объединение малознакомых схожих ситуаций

В заключении работы приведен список основных результатов и обзор потенциальной области применения предложенных методов Приложение А к работе содержит доказательства полноты и корректности

разработанных алгоритмов, а также анализ их алгоритмической сложности

Приложение Б содержит описание реализации алгоритмов планирования и верификации, их архитектуре, формате входных файлов, а также тестов, использовавшихся для проверки их работоспособности Алгоритмы верификации и планирования реализованы в виде консольных приложению В качестве способа описания моделей системы и их свойств используется диалект XML, заданный с помощью XSD-схемы, используемой для автоматической проверки корректности входных файлов Для преобразования входных файлов в дерево объектов используется платформа NET 2 0 и язык программирования На основе полученного дерева строится дерево объектов С++, которые используются для проведения основных вычислений Использование гибридного С#/С++ решения позволяет использовать богатый набор классов NET Framework для анализа и разбора XML, не потеряв при этом в производительности основного алгоритма В качестве пакета разрешающих диаграмм используется пакет университета Колорадо CUDD, портированный под операционную систему Windows с использованием набора библиотек и компиляторов MinGW Все использованные в разработке программы, библиотеки и пакеты свободно распространяются для научных целей и некоммерческого использования

Основные результаты. В рамках диссертации получены следующие результаты

1 Разработана математическая модель интеллектуального агента, описывающая такие аспекты деятельности агента, как взаимодействие с внешней средой, неполнота информации, способность к анализу и накоплению опыта, ограничения на время реакции, управляемое целями поведение и планирование действий

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

3 Разработан логический формализм для спецификации свойств интеллектуального агента, позволяющий описывать свойства математической модели интеллектуального агента

4 Разработан логический формализм для спецификации мультиагентной системы с временными ограничениями MASL, включающий логику спецификации интеллектуального агента и расширяющий ее средствами описания свойств определенных групп агентов (коалиций)

5 Разработаны и реализованы алгоритмы верификации ("проверки модели", model checking) систем по спецификациям MASL, имеющие полиномиальную сложность и использующие технику символической верификации Корректность, завершаемость и полнота алгоритмов доказаны, кроме того, доказано, что их алгоритмическая сложность не превосходит полинома от размера модели и длины формулы

6 Разработаны и реализованы алгоритмы построения мультиагент-ных планов, удовлетворяющих спецификации MASL и использующие технику символического планирования Корректность и завершаемость алгоритмов доказаны, кроме того, доказано, что их алгоритмическая сложность не превосходит полинома от размера модели и экспоненты от длины формулы

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

Работы автора по теме диссертации

[1] Бугайченко, Д Ю Верификация распределенных систем реального времени по спецификации MASL // Вестник СПбГУ, Серия 1, - 2007 - №, Июль С 65-74

[2] Бугайченко, Д Ю Математическая модель интеллектуального агента / / Сборник трудов международной конференции «Процессы управления и устойчивость» — Санкт-Петербург Издательство СПбГУ, 2006 С 9-19

[3] Бугайченко, Д Ю Математическая модель и спецификация интеллектуальных агентных систем I¡Системное программирование - 2006 - №2 С 94-115

[4] Бугайченко, Д Ю Символическое планирование в ограничениях CTL / / Сборник трудов международной конференции «Процессы управления и устойчивость» — Санкт-Петербург Издательство СПбГУ, 2007 С 335-341

[5] Бугайченко, Д Ю , Соловьев, И П Абстрактная архитектура интеллектуального агента и методы ее реализации // Системное программирование — 2005 — №1 С 36—67

[6] Бугайченко, Д Ю, Соловьев, И П Архитектура Изолированного Интеллектуального Агента / / Сборник трудов международной конференции «Современные проблемы информатизации» — Воронеж Издательство «Научная книга», 2006 С 220—222

[7] Бугайченко, Д Ю, Соловьев, И П Методы решения некоторых инфраструктурных задач, возникающих при разработке мультиа-гентных систем // Материалы конференции «Технологии Microsoft в теории и практике» — Санкт-Петербург Издательство СПбГПУ, 2006 С 177-178

[8] Бугайченко, Д Ю , Соловьев, И П Разработка методики проектирования интеллектуальных систем реального времени с использованием интеллектуальных агентов // Материалы конференции «Технологии Microsoft в теории и практике» — Санкт-Петербург Издательство СПбГПУ, 2004 С 77—78

[9] Бугайченко, Д Ю , Соловьев, И П Формально-логическая спецификация мультиагентных систем реального времени // Вестник СПбГУ, Серия 1, - 2007 - №2, Апрель С 49-57

[10] Bugaychenko, D Y, Solomev, I Р MASL A Logic for the Specification of Multiagent Real-Time Systems // Proc of the 5tfl International Central and Eastern European Conference on Multi-Agent Systems — Leipzig (Germany) 2007 Pp 183—192

По теме диссертации опубликовано 10 научных работ [1, 2, 3, 4, 5, 6, 7, 8, 9, 10] Работы [5, 6, 7, 8, 9, 10] опубликованы в соавторстве с научным руководителем В работе [5] автором разработана формальная модель интеллектуального агента, а также приведен обзор возможных способов ее реализации В работах [6, 7, 8] автором предложены способы организации распределенной интеллектуальной системы, а также методы решения некоторых возникающих при разработке таких систем задач В работах [9, 10] автором предложен формально-логический метод спецификации мультиагентных систем Работы [1, 9] опубликованы в издании, рекомендованном ВАК

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

[11] Algebraic Decision Diagrams and Their Applications // IEEE /АСМ Proc of the International Conference on CAD — Santa Clara, California IEEE Computer Society Press, 1993 - Pp 188-191

[12] Alur, R A really temporal logic / R Alur, T A Henzinger //J ACM - 1994 - Vol 41, no 1 - Pp 181-203

[13] Alur, R Alternating-time temporal logic / R Alur, T A Henzmger, О Kupferman // J ACM - 2002 - Vol 49, no 5 - Pp 672-713

[14] Bryant, R E Graph-based algorithms for Boolean function manipulation /RE Bryant // IEEE Transactions on Computers — 1986 — Vol C-35, no 8 - Pp 677-691

[15] Cimatti, A Automatic OBDD-based generation of universal plans in non-deterministic domains // AAAI/IAAI — 1998 — Pp 875-881

[16] Emerson, E A Temporal and modal logic / Б A Emerson // Handbook of Theoretical Computer Science, Volume В Formal Models and Sematics (B) - North-Holland Pub Co , 1990 - Pp 995-1072

[17] Haigh, К Z High-level planning and low-level execution towards a complete robotic agent // Proc of the first international conference on Autonomous agents — New York, NY, USA ACM Press, 1997 — Pp 363-370

[18] Henzmger, T A Timed alternating-time temporal logic 11 Proc of the 4th International Conference on Formal Modelling and Analysis of Timed Systems — Vol 4202 of Lecture Notes m Computer Science — Paris, France Springer, 2006 —September — Pp 1-17

[19] Laroussime, F Model checking timed ATL for durational concurrent game structures // Proc of the 4th International Conference on Formal Modelling and Analysis of Timed Systems — Vol 4202 of Lecture Notes in Computer Science — Paris, France Springer, 2006 —September — Pp 245-259

[20] Pearl, J Heuristics intelligent search strategies for computer problem solving / J Pearl — Boston, MA, USA Addison-Wesley Longman Publishing Co , Inc , 1984

[21] Pistore, M Symbolic techniques for planning with extended goals m non-determimstic domains // Proc of the 6th European Conference on Planning — 2001

[22] Quantitative temporal reasoning / E A Emerson, А К Мок, A P Sistla, J Srmivasan // Real-Time Systems — 1992 — Vol 4, no 4 - Pp 331-352

Подписано в печать^ $%007 г Формат бумаги 60x841/16 Бумага офсетная Печать цифровая Объем 1 уел п л Тираж 100 экз Заказ №4005 Отпечатано в отделе оперативной полиграфии НИИХ СПбГУ с оригинал-макета заказчика 198504, Санкт-Петербург, Старый Петергоф, Университетский пр, 26

Введение

Глава 1. Основные понятия.

1.1. Понятие агент.

1.2. Интеллектуальный агент.

Глава 2. Модель интеллектуального агента

2.1. Формальные модели распределенных систем.

2.2. Модель интеллектуального агента.

2.3. Зиания и представления агента

2.4. Цели и желания агента.

2.5. Планирование

2.6. В01-агент.

Глава 3. Модель мультиагентной системы

3.1. Коммуникация агентов

3.2. Расширенные представления.

3.3. Коалиции.

Глава 4. Логика спецификации интеллектуального агента

4.1. Спецификация поведения системы

4.2. Спецификация ментальных состояний

4.3. Логика спецификации интеллектуального агента

Глава 5. Алгоритмы верификации для логики спецификации интеллектуального агента.

5.1. Символические алгоритмы.

5.2. Алгоритмы верификации.

Глава 6. Логика спецификации мультиагентной системы.

6.1. Синтаксис

6.2. Семантика

6.3. Алгоритмы верификации.

6.4. Пример

Глава 7. Планирование в ограничениях.

7.1. Существующие подходы к планированию.

7.2. Постановка задачи.

7.3. Основная структура алгоритма

7.4. Построение планов для формул

Глава 8. Накопление и анализ опыта.

8.1. Символическое представление опыта и операции с ним.

8.2. Методы анализа и построения обобщений

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

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

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

Представляется, что решение данной проблемы следует искать на пути применения методов формальной спецификации проектируемой системы с последующим автоматическим тестированием или верификацией (обычно это проверка модели или model checking).

Основу большинства методов формальной спецификации составляет некоторый вариант темпоральной логики. Наиболее широкое распространение получила логика ветвящегося времени CTL [56], основным достоинством которой является билинейная относительно размера спецификации и размера модели системы сложность задачи верификации. CTL расширяет классическую логику высказываний темпоральными операторами "в следующий момент ф" ОФ и "когда-нибудь ф, а до тех пор ф" ф U ф и кванторами "на любом пути ." А и "существует путь на котором ." Е.

Для спецификации систем с временными ограничениями предложены различные расширения логики CTL. Например, логика RTCTL [150] расширяет CTL ограниченным оператором ф U <(</>, интерпретируемым как "не более чем через t шагов ф, а до тех пор ф". Основным достоинством RTCTL является сохранение билинейиой сложности задачи верификации. Большей выразительной мощности, за счет увеличения вычислительной сложности, можно достичь введя переменные часов (х, у,.) и квантор фиксации (•) [24]: х-Аф U ((х < £)Аф).

Основным ограничением CTL является отсутствие явных средств спецификации систем, состоящих из нескольких взаимодействующих сущностей. Это ограничение преодолевается в логике альтернированного времени ATL [25], позволяющей учитывать многокомпонентность системы в явном виде. ATL включает конечное множество игроков-агентов Р и заменяет кванторы CTL на квантор "для коалиция игроков ССР существует такая стратегия, что на любом пути ." {(С)). Для ATL также были предложены методы спецификации ограничений на время реакции, например, с помощью подстрочного индекса [108] или с помощью переменных часов [73].

Характерной чертой многих методов формальной верификации является комбинаторный взрыв пространства состояний верифицируемых систем. Частично эту проблему позволяют решить так называемые символические (symbolic) алгоритмы, которые оперирует с множествами состояний, а не с отдельными состояниями. Серьезный толчок к развитию символических алгоритмов дало введение ориентированных булевых разрешающих диаграмм (OBDD) [41], позволяющих относительно компактно представлять большие множества и эффективно выполнять над ними операции. Было предложено множество различных модификаций концепции OBDD, среди которых можно выделить алгебраические разрешающие диаграммы (ADD) [18].

Для уменьшения времени реакции системы широко используется подход исполняемых плаиов [66]. В этом случае до начала непосредственного взаимодействия с внешней средой система составляет план действий для достижения своих целей. Существует множество различных алгоритмов планирования, используемых для мультиагентных систем, часть из которых базируется на классических алгоритмах поиска пути в графе А* [141]. Однако подобные алгоритмы также подвержены проблеме комбинаторного взрыва пространства состояний, частично решить которую позволяют алгоритмы символического планирования [47].

Описанные выше алгоритмы позволяют строить планы для достижения относительно простых целей, например, достижение системой определенного состояния при посещении только допустимых состояний. В работе [145] были предложены алгоритмы для решения более сложной задачи — построения плана, удовлетворяющего спецификации, описанной с помощью логики линейного времени1. Подобный подход получил название "планирование с темпорально

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

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

Одной из значимых тенденций в современных информационных системах является параллелизация вычислений и интеграция отдельных информационных систем в более мощные вычислительные комплексы. Влияние этих тенденций на развитие самонастраивающихся систем привело к формированию концепции социальных агентов и мультиагентных систем. Первые работы, предлагающие декомпозицию системы в виде набора автономных взаимодействующих сущностей, появились в 70-х годах 20-го века [69, 75, 111], однако термин агент впервые появился лишь спустя десять лет [61].

Исторически первым методом реализации распределенных интеллектуальных систем является метод классной доски, впервые примененный в системе HEARSAY [69], предназначенной для распознавания речи. Метод включает следующие основные архитектурные элементы:

• Глобальную структуру данных, называемую классной доской (blackboard)-,

• несколько параллельно работающих носителей знаний, экспертов (knowledge source), которые постоянно видят содержимое классной доски;

• центральный контролирующий механизм (control algorithm) или протокол, определяющий порядок доступа экспертов к классной доске.

В данном случае эксперты выступают как основные участники процесса решения задачи. Они не общаются между собой напрямую, а взаимодействуют с контролирующим механизмом и помещают информацию на доску. Эксперты постоянно сканируют содержимое доски или получают уведомления о его изменении. Изначально на доске формулируется задача, которую необходимо решить. Если один из экспертов знает способ решения задачи или хотя бы информацию, которая, по его мнению, может помочь решению задачи, он запрашивает контролирующий механизм получения доступа на запись к классной доске. Когда доступ будет получен, эксперт записывает информацию па доску, и она становится видима всем остальным экспертам.

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

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

Для проверки концепции существ Ленат разработал приложение PUP6 [111], где каждое существо моделировалось на LISP в виде фрейма с двадцатью семью слотами (в терминологии Лената частями (parts)), представлявшими вопросы, на которое существо могло ответить. При приходе сообщения, существо сравпивало его со своими слотами, что могло привести к широковещательной посылке нового сообщения. Опыт, полученный при разработке PUP6, Ленат использовал в своем известном проекте Artificial Mathematician (АМ) [112].

Концепция существ лучше подходит для моделирования агентов и мульти-агентных систем, чем классная доска. Большим плюсом концепции является отсутствие централизованного механизма управления и полноценная распределенность. Однако существа в концепции Лената не являются самообучающимися и не способны к накоплению и анализу опыта. Набор их знаний фиксирован, и они не обладают возможностью их расширять.

Первые наработки концепции акторов [14, 75] появились практически одновременно с работами Лената по существам. Концепция была основана на объектно-ориентированном подходе к моделированию и могла рассматриваться как метод проектирования параллельных объектно-ориентированных систем. В отличие от существ, концепция акторов по сей день активно развивается как в теории, так и на практике в различных распределенных системах.

Система состоит из набора акторов, которые остаются пассивными до тех пор, пока не получат сообщение. Когда сообщение получено, актор пытается выбрать соответствующее сообщению поведение (behavior) (в ранних работах поведение называлось сценарием (script)). Реакция актора на сообщения могла быть трех видов:

• посылка нового сообщения себе или другим агентам;

• создание дополнительных акторов;

• определение замещения (replacement) поведения.

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

Большим плюсом концепции акторов является её высокий параллелизм, ограниченный исключительно возможностями ЭВМ. Однако актора еще нельзя считать полноценным агентом, так как он представляет достаточно простую вычислительную единицу, все еще не обладающую возможностями к самообучению.

Multi-Agent Computing Environment или MACE исторически является первой полноценно распределенной интеллектуальной системой, описание которой было впервые опубликовано в 1987 году Гессером [61]. Система состоит из следующих пяти компонент:

• набор прикладных агентов (application agents), которые являлись основными вычислительными единицами системы;

• набор предопределенных системных агентов (system agents), предоставлявших сервис пользователю;

• набор средств общего назначения, доступных все агентам (facilities);

• база данных с описаниями (description databases), которая содержала описания агентов и могла произвести исполняемый код па основе описания;

• набор ядер (kernels), по одному на каждую физическую машину, которые обеспечивали коммуникацию и маршрутизацию сообщений.

Гессер выделил три аспекта деятельности агентов: они содержат знания, они ощущают окружающую среду, они выполняют действия. Агенты M АСЕ имели два типа знания: специализированные (domain knowledge), ориентированные на предметную область, и ознакомительные знания (acquaintance knowledge) — знания о других агентах системы. Агент хранил следующую информацию о других агентах.

• Класс (class) - агенты организовывались в группы, называемые классами и идентифицируемые по имени класса.

• Имя (пате) - каждому агенту присваивалось уникальное в классе имя, таким образом, в рамках системы агента можно было идентифицировать парой строк (класс, имя).

• Роль (roles) - описание роли, выполняемой агентом в своем классе.

• Навыки (skills) - множество возможностей описываемого агента по сведениям описывающего агента.

• Цели (goals) - множество целей, которых описываемый агент хочет достичь по сведениям описывающего агента.

• Планы (plans) - представление описывающего агента о том, как описываемый агент будет достигать свои целей.

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

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

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

На сегодняшний день мультиагентные системы используются для разработки широкого спектра информационных систем2, среди которых, условно, можно выделить три основных класса.

Открытые системы. Системы, структура которых может изменяться в процессе их функционирования. Самая большая и самая открытая на сегодняшний день система — Интернет. Социальность и автономность агента позволяют эффективно применять его в качестве элемента открытой системы.

Сложные распределенные системы. Наилучшими современными методами борьбы со сложностью, являются модульность и абстракция. Благодаря высокой степени автономности, агент позволяет уменьшить количество зависимостей между частями системы и, следовательно, упростить её проектирование и реализацию.

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

В промышленности мультиагентные системы наиболее распространены в следующих областях.

2Более подробное описание областей применения мультиагснтных систем можно найти и работах [91] и [137]

Автоматизация управления сложными системами. Область, в которой давно и эффективно применяются интеллектуальные агенты. В качестве примеров можно привести платформу ARCHON [171], систему управления производством YAMS [136] и систему управления воздушным движением OASIS [117].

Сбор и обработка информации. Агенты часто используются для реализации систем, собирающих и обрабатывающих информацию из всемирной сети Интернет. Большинство современных поисковых машин реализовано с использованием агентов.

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

Хороший обзор современных теоретических и практических подходов к построению мультиагентных систем можно найти в работе [183]. Работа [126] содержит более критический анализ, а также задается вопросом, почему агентно-ориентированные методы не столь популярны, как могли бы быть.

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

• Международная конференция по автономным агентам и мультиагентным системам (AAMAS, www. aamas-conference. org) является одной из наиболее популярных и значимых конференций, рассматривающей все аспекты разработки мультиагентных систем.

• Международная конференция по мультиагентным системам центральной и восточной Европы (CEEMAS, www.ceemas.org). Эта конференция, в отличии от ежегодной AAMAS, проводится раз в два года на территории центральной или восточной Европы.

• Международный симпозиум по агентам и мультиагентным системам (KES AMSTA, ELmsta-07.kesinternational.org). Относительно молодое мероприятия, так же охватывающее практически весь спектр возникающих при разработке и проектировании MAC задач.

• Семинар по автономным интеллектуальным системам и применению агентов для извлечения знаний (AIS-ADM, space.iias.spb.su/ais07). Проводимый в России семинар, посвященный стыку двух активно развивающихся направлений: применения мултиагеитпых систем для решения задачи извлечения знаний (data mining).

Кроме того, существует несколько сообществ и организаций, занимающихся разработкой, обобщением и стандартизацией подходов к разработке мультиаген-тых систем. Одним из наиболее значимых среди них является FIPA (Foundation for Intelligence Physical Agent) [59].

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

Gaia. Основанная на концепции роли методология предложенная Майклом Вулдриджем и Николасом Дженнингсом [184]. Методология предлагает разработку нескольких типов моделей. На этапе анализа системы разрабатываются модель ролей и модель взаимодействий, которые на этапе проектирования уточняются в моделях агентов, сервисов и осведомленности (acquaintance).

SODA. Методология, ориентированная на разработку приложений для сети

Интернет [133], ключевым понятием которой является понятие задачи. Основное внимание в данной методологии уделяется социальности агентов и связанным с ней особенностям проектирования.

Tropos. Методология [44], основное внимание которой уделяется организации мультиагентной системы. Основными понятиями методологии являются понятия актора (агента), цели и зависимости. Фундаментом методологии является система моделей i* [187].

В последнее время достаточно активно развиваются методологии и платформы для разработки мультиагентных систем с использованием формально-логических методов. Одним из первых агентно-ориентированных языков, основанных на формально-логических методах, является язык 3APL [13], получивший очень широкое распространение. Кроме того, в этой области можно выделить языки Dribble [179] и платформу DESIRE [52], а одним из последних достижений в этой области является язык MABEL [128]. Подобные подходы представляют наибольший интерес в контексте данной работы.

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

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

• Алгоритм верификации систем по спецификации MASL.

• Алгоритм построения мультиагентных планов с темпорально расширенными целями, выраженными в ограниченном варианте логики MASL, обеспечивающем эффективную реализацию.

• Метод накопления и анализа опыта для мультиагентных систем.

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

Основные результаты

В рамках диссертации получены следующие результаты.

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

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

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

4. Разработан логический формализм для спецификации мультиагентной системы с временными ограничениями MASL, включающий логику спецификации интеллектуального агента и расширяющий её средствами описания свойств определенных групп агентов (коалиций).

5. Разработаны и реализованы алгоритмы верификации ("проверки модели", model checking) систем по спецификациям MASL, имеющие полиномиальную сложность и использующие технику символической верификации. Корректность, завершаемость и полнота алгоритмов доказаны, кроме того, доказано, что их алгоритмическая сложность не превосходит полинома от размера модели и длины формулы.

6. Разработаны и реализованы алгоритмы построения мультиагентных планов, удовлетворяющих спецификации MASL и использующие технику символического планирования. Корректность и завершаемость алгоритмов доказаны, кроме того, доказано, что их алгоритмическая сложность не превосходит полинома от размера модели и экспоненты от длины формулы.

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

Заключение

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

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

• системы автоматического перемещения грузов;

• автономные исследовательские зонды;

• системы управления автоматизированным производством;

• системы автоматического поиска предметов и обхода территории.

1. Бугайченко, Д. Ю. Математическая модель интеллектуального агента. // Сборник трудов международной конференции «Процессы управления и устойчивость». — Санкт-Петербург: Издательство СПбГУ, 2006. — С. 9-19.

2. Бугайченко, Д. Ю. Математическая модель и спецификация интеллектуальных агентных систем. / Д. Ю. Бугайченко // Системное программирование. 2006. - № 2. - С. 94-115.

3. Бугайченко, Д. Ю. Верификация распределенных систем реального времени по спецификации MASL / Д. Ю. Бугайченко // Вестник СПбГУ, Серия 1. 2007. - № 3. - С. 65-74.

4. Бугайченко, Д. Ю. Символическое планирование в ограничениях CTL. // Сборник трудов международной конференции «Процессы управления и устойчивость». — Санкт-Петербург: Издательство СПбГУ, 2007. — С. 335-341.

5. Бугайченко, Д. Ю. Абстрактная архитектура интеллектуального агента и методы ее реализации. / Д. Ю. Бугайченко, И. П. Соловьев // Системное программирование. — 2005. — № 1. — С. 36-67.

6. Бугайченко, Д. Ю. Архитектура изолированного интеллектуального агента. // Сборник трудов международной конференции «Современные проблемы информатизации».— Воронеж: Издательство «Научная книга», 2006.-С. 220-222.

7. Бугайченко, Д. Ю. Методы решения некоторых инфраструктурных задач, возникающих при разработке мультиагентных систем. // Сборник трудов конференции «Технологии Microsoft в теории и практике». — Санкт-Петербург: Издательство СПбГПУ, 2006.- С. 177-178.

8. Бугайченко, Д. Ю. Формально-логическая спецификация мультиагентных систем реального времени. / Д. Ю. Бугайченко, И. П. Соловьев // Вестник СПбГУ, Серия 1. 2007. - № 3. - С. 49-57.

9. Марков, А. А. Элементы математической логики / А. А. Марков.— Москва: Издательство МГУ, 1984.

10. Мендельсон, Э. Введение в математическую логику / Э. Мендельсон. — Москва: Наука, 1984.

11. Agent programming in 3APL / К. V. Hindriks, F. S. D. Boer, W. V. der Hoek, J.-J. C. Meyer // Autonomous Agents and Multi-Agent Systems. — 1999. — Vol. 2, no. 4.-Pp. 357-401.

12. Agha, G. Actors: a model of concurrent computation in distributed systems / G. Agha. Cambridge, MA, USA: MIT Press, 1986.- 190 pp.

13. Agotnes, T. On the logic of coalitional games // Proc. Fifth International Joint Conference on Autonomous Agents and Multiagent Systems / Ed. by P. Stone, G. Weiss. New York (USA): ACM Press, 2006,- P. 153-160.

14. Agotnes, T. Temporal qualitative coalitional games // Proc. Fifth International Joint Conference on Autonomous Agents and Multiagent Systems / Ed. by P. Stone, G. Weiss. New York (USA): ACM Press, 2006.- Pp. 177-184.

15. Akers, S. Binary decision diagrams / S. Akers // IEEE Transactions on Computers.- 1978.-June. Vol. C-27, no. 6,- Pp. 509-516.

16. Algebraic Decision Diagrams and their applications // Proc. IEEE/ACM International Conference on CAD. — Santa Clara (California): IEEE Computer Society Press, 1993.- Pp. 188-191.

17. Alur, R. Timed automata // Proc. 11th International Conference on Computer Aided Verification. London (UK): Springer-Verlag, 1999. - Pp. 8-22.

18. Ahr, R. A theory of timed automata / R. Alur, D. L. Dill // Theoretical Computer Science. 1994. - Vol. 126, no. 2. - Pp. 183-235.

19. Alur, R. The benefits of relaxing punctuality / R. Alur, T. Feder, T. A. Hen-zinger // J. ACM.- 1996.- Vol. 43, no. 1,- Pp. 116-146.

20. Ahr, R. Logics and models of real time: A survey // Proc. Real-Time: Theory in Practice, REX Workshop. — London (UK): Springer-Verlag, 1992.— Pp. 74-106.

21. Ahr, R. Real-time logics: complexity and expressiveness / R. Alur, T. A. Hen-zinger // Inf. Comput.- 1993,- Vol. 104, no. 1.- Pp. 35-77.

22. Alur, R. A really temporal logic / R. Alur, T. A. Henzinger // J. ACM.— 1994.- Vol. 41, no. 1.- Pp. 181-203.

23. Alur, R. Alternating-time temporal logic / R. Alur, T. A. Henzinger, O. Kupferman // J. ACM. 2002. - Vol. 49, no. 5. - Pp. 672-713.

24. Alur, R. Reactive modules / R. Alur, T. Henzinger // Formal Methods in System Design. 1999. - July. - Vol. 15, no. 11.- Pp. 7-48.

25. Andreka, H. Handbook of Philosophical Logic / H. Andreka, I. Nemeti, I. Sain // Handbook of Philosophical Logic / Ed. by D. Gabbay. — Kluwer, 1997.

26. Antoniotti, M. Synthesis and verification of discrete controllers for robotics and manufacturing devices with temporal logic and the Control-D system: Ph.D. thesis / New York University. — New York, NY, USA: New York University, 1995.

27. Austin, J. L. How to do things with words / J. L. Austin. — Oxford, England: Oxford University Press, 1962.

28. Aziz, A. BDD variable ordering for interacting finite state machines // Proc. 31st annual conference on Design automation.— San Diego (USA): ACM Press, 1994.-Pp. 283-288.

29. Bacchus, F. Planning for temporally extended goals / F. Bacchus, F. Kaban-za // Annals of Mathematics and Artificial Intelligence. — 1998.— Vol. 22, no. 1-2. Pp. 5-27.

30. Baeten, J. C. M. A brief history of process algebra / J. C. M. Baeten // Theor. Comput. Sci. 2005. - Vol. 335, no. 2-3. - Pp. 131-146.

31. Baier, C. Approximate symbolic model checking of continuous-time markov chains // Proc. 10th International Conference on Concurrency Theory. — London (UK): Springer-Verlag, 1999.- Pp. 146-161.

32. Biere, A. ABCD: a compact BDD library (http: / / www.inf.ethz.ch / personal/biere / projects/abed/).

33. Bonet, B. Heuristic search planner 2.0 / B. Bonet, H. Geffner // The AI Magazine. 2001. - Vol. 22, no. 1. - Pp. 77-80.

34. Bonet, B. Planning as heuristic search / B. Bonet, H. Geffner // Artificial Intelligence. 2001. - Vol. 129, no. 1-2. - Pp. 5-33.

35. Borgo, S. Coalitions in action logic // Proc. Twentieth International Joint Conference on Artificial Intelligence. — Hyderabad (India): 2007. — January. — Pp. 1822-1827.

36. Brand, D. On communicating finite-state machines / D. Brand, P. Zafiropu-lo // J. ACM. 1983. - Vol. 30, no. 2.- Pp. 323-342.

37. Bratman, M. E. Intention, plans, and practical reason / M. E. Bratman.— Cambridge, MA: Harvard University Press, 1987.

38. Bratman, M. E. Plans and resource-bounded practical reasoning / M. E. Bratman, D. Israel, M. Pollack // Philosophy and AI: Essays at the Interface / Ed. by R. Cummins, J. L. Pollock. — Cambridge, Massachusetts: The MIT Press, 1991.-Pp. 1-22.

39. Bryant, R. E. Graph-based algorithms for boolean function manipulation / R. E. Bryant // IEEE Transactions on Computers.- 1986.- Vol. C-35, no. 8.-Pp. 677-691.

40. Bryant, R. E. Symbolic boolean manipulation with ordered binary-decision diagrams / R. E. Bryant 11 ACM Computing Surveys.— 1992.— Vol. 24, no. 3.- Pp. 293-318.

41. Bugaychenko, D. Y. MASL: A logic for the specification of multiagent real-time systems. // Proc. 5th International Central and Eastern European Conference on Multi-Agent Systems. — Leipzig (Germany): Springer-Verlag, 2007.-Pp. 183-192.

42. Castro, J. Towards requirements-driven information systems engineering: the Tropos project / J. Castro, M. Kolp, J. Mylopoulos // Information Systems. — 2002. Vol. 27, no. 6. - Pp. 365-389.

43. Chellas, B. F. Modal logic: an introduction / B. F. Chellas. — Cambridge University Press, 1980. Vol. 316.

44. Chen, Y. X. Temporal planning using subgoal partitioning and resolution in SGPlan / Y. X. Chen, B. W. Wah, C. W. Hsu // Journal of Artificial Intelligence Research. — 2006.

45. Cimatti, A. Automatic OBDD-based generation of universal plans in non-deterministic domains // AAAI/IAAI. 1998. - Pp. 875-881.

46. Clarke, E. Model checking / E. Clarke. MIT Press, 1999. - P. 330.

47. Cohen, P. R. Intention is choice with commitment / P. R. Cohen, H. J. Levesque // Artificial Intelligence.— 1990.— Vol. 42, no. 2-3.— Pp. 213-261.

48. Combining test case generation and runtime verification / C. Arthoa, H. Bar-ringerb, A. Goldbergc et al. // Theoretical Computer Science. — 2005. — Vol. 336, no. 2-3. Pp. 209-234.

49. Dean, T. A model for reasoning about persistence and causation / T. Dean, K. Kanazawa // Computational Intelligence. — 1989. — Vol. 5, no. 3. — Pp. 142-150.

50. DESIRE: Modelling multi-agent systems in a compositional formal framework / F. M. T. Brazier, B. M. Dunin-Keplicz, N. R. Jennings, J. Treur // Int Journal of Cooperative Information Systems. — 1997.— Vol. 6, no. 1.— Pp. 67-94.

51. Drusinky, D. Real-time, on-line, low impact, temporal pattern matching 11 Proc World Multiconference on Systemics, Cybernetics and Informatics (SCI 2003).-2003.

52. Drusinky, D. Verification of timing properties in rapid system prototyping // Proc. 14th IEEE International Workshop on Rapid System Prototyping (RSP'03).- Washington DC (USA): IEEE Computer Society, 2003,- P. 47.

53. Duff, I. Direct methods for sparse matrices / I. Duff, A. Erisman, J. Reid // A CM Transactions on Mathematical Software. — 1986. — Vol. 15. — Pp. 1-14.

54. Emerson, E. A. Temporal and modal logic. / E. A. Emerson // Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B) / Ed. by J. van Leeuwen. North-Holland Pub. Co., 1990,- Pp. 995-1072.

55. Estelle: Formal protocol specification and testing, http://www.eecis.udel. edu/~amer/PEL/estelle/.

56. FIPA. Fipa agent communication specifications (http://www.fipa.org/ repository/aclspecs. html).

57. Foundation for Intelligent Physical Agent (http://www.fipa.org).

58. Fujita, M. Multi-terminal binary decision diagrams: An efficient datastructure for matrix representation / M. Fujita, P. C. McGeer, J. C.-Y. Yang // Form. Methods Syst. Des. 1997. - Vol. 10, no. 2-3. - Pp. 149-169.

59. Gasser, L. MACE: A flexible testbed for distributed AI research. / L. Gasser, C. Braganza, N. Hermann. // Distributed Artificial Intelligence. — 1987. — Pp. 119-152.

60. Gill, A. Introduction to the theory of finite-state machines / A. Gill. — McGraw-Hill, 1962.

61. Goldblatt, R. Logics of time and computation / R. Goldblatt. — Stanford, CA, USA: Center for the Study of Language and Information, 1987.

62. Goranko, V. Coalition games and alternating temporal logics // Proc. Eighth Conference on Theoretical Aspects of Rationality and Knowledge (TARKVI-II) / Ed. by J. van Benthem.- 2001.- P. 259-272.

63. Guestrin, C. Planning under uncertainty in complex structured environments: Ph.D. thesis / Computer Science Department, Stanford University. — 2003.

64. Haigh, K. Z. High-level planning and low-level execution: towards a complete robotic agent // Proc. first international conference on Autonomous agents. — Marina del Rey (USA): ACM Press, 1997.- Pp. 363-370.

65. Halpern, J. Y. A guide to completeness and complexity for modal logics of knowledge and belief / J. Y. Halpern, Y. Moses // Artificial Intelligence.— 1992. Vol. 54, no. 3. - Pp. 319-379.

66. Harel, D. Dynamic logic / D. Harel, D. Kozen, J. Tiuryn // SIGACT News. -2001. Vol. 32, no. 1. - Pp. 66-69.

67. The Hearsay-I speech understanding system: An example of the recognition process / D. Reddy, L. Erman, R. Fennell, R. Neely // Transactions on Computers. 1976. - April. - no. 4. - Pp. 422-431.

68. Hennessy, M. A process algebra for timed systems / M. Hennessy, T. Regan // Inf. Comput.- 1995,- Vol. 117, no. 2.- Pp. 221-239.

69. Henzinger, T. A. It's about time: Real-time logics reviewed // Proc. 9th International Conference on Concurrency Theory. — London (UK): Springer-Verlag, 1998. Pp. 439-454.

70. Henzinger, T. A. HYTECH: A model checker for hybrid systems // Proc. 9th International Conference on Computer Aided Verification. — London (UK): Springer-Verlag, 1997. Pp. 460-463.

71. Hett, A. MORE: an alternative implementation of BDD packages by multi-operand synthesis // Proc. conference on European design automation. — Geneva (Switzerland): IEEE Computer Society Press, 1996.- Pp. 164-169.

72. Hewitt, C. A universal modular ACTOR formalism for AI // Proc. Third International Joint Conference on Artificial Intelligence (IJCAI-73). — 1973. — Pp. 235-245.

73. Hintikka, J. Impossible possible worlds vindicated / J. Hintikka // Journal of Philosophical Logic. — 1975. —August. — Vol. 4, no. 3.— Pp. 475-484.

74. Hoare, C. A. R. An axiomatic basis for computer programming / C. A. R. Hoare // Communications of the ACM. — 1969. — Vol. 12, no. 10. — Pp. 576-580.

75. Hoare, C. A. R. Communicating sequential processes / C. A. R. Hoare // Commun. A CM. 1978. - Vol. 21, no. 8.- Pp. 666-677.

76. Hoffmann, J. The FF planning system: Fast plan generation through heuristic search / J. Hoffmann, B. Nebel // Journal of Artificial Intelligence Research. 2001. - Vol. 14. - Pp. 253-302.

77. Holzmann, G. The SPIN model checker / G. Holzmann // IEEE Transactions on Software Engineering. — 1997. May. - Vol. 23, no. 5.— Pp. 279-295.

78. Hsiung, P.-A. A state graph manipulator tool for real-time system specification and verification // Proc. 5th International Conference on Real-Time Computing Systems and Applications. — Washington DC (USA): IEEE Computer Society, 1998.-P. 181.

79. Implicit state enumeration of finite state machines using BDD's // Proc. IEEE International Conference on Computer-Aided Design. — Santa Clara (USA): 1990. November. - Pp. 130-133.

80. International conference on automated planning and scheduling (http: //www. icaps-conference.org/) // International Conference on Automated Planning and Scheduling. — 2007.

81. Ishiura, N. Minimization of binary decision diagrams based on exchanges of variables // Proc. IEEE International Conference on Computer-Aided Design. Santa Clara (USA): 1991. - November. - Pp. 472-475.

82. ITU-T. Specification and description language (SDL): Tech. rep. / ITU-T: International Telecommunication Union Standardization Sector, 1999.

83. Jamroga, W. Do agents make model checking explode (computationally)? / W. Jamroga, J. Dix // Multi-Agent Systemsand Applications.— 2005.— no. IV.

84. Janssen, G. Design of a pointerless BDD package // Proc. IEEE 10th International Workshop on Logic & Synthesis. — Tahoe City (USA): 2001. —June.

85. Janssen, G. A consumer report on BDD packages // Proc. 16th symposium on Integrated circuits and systems design. — Washington DC (USA): IEEE Computer Society, 2003.- P. 217.

86. Jenings, N. R. Applications of intelligent agents. — 2000.

87. Jenings, N. R. Multiagent Systems / N. R. Jenings, M. J. Wooldridge // Multiagent Systems / Ed. by G. Weiss. MIT Press, 2001. - Pp. 377-421.

88. Jennings, N. R. On being responsible // Proc. Third European Workshop on Modelling Autonomous Agents in a Multi-Agent World (MAAMAW 91) / Ed. by E. Werner, Y. Demazeau. — Elsevier Science Publishers B.V.: Amsterdam, The Netherlands, 1992. Pp. 93-102.

89. Jensen, R. M. A comparison study between the CUDD and BuDDy OBDD package applied to Al-planning problems: Tech. rep. / R. M. Jensen: Computer Science Department, Carnegie Mellon University, 2002. CMU-CS-02-173.

90. Jensen, R. M. Efficient BDD-based planning for non-deterministic, fault-tolerant, and adversarial domains: Ph.D. thesis / Carnegie Mellon University. — 2003.-June.

91. Jensen, R. M. OBDD-based universal planning: Specifying and solving planning problems for synchronized agents in non-deterministic domains / R. M. Jensen, M. M. Veloso // Lecture Notes in Computer Science. — 1999. — Vol. 1600.-Pp. 213-223.

92. Jensen, R. M. ASET: a multi-agent planning language with non-deterministic durative tasks for BDD-based fault tolerant planning // Proc. 15th International Conference on Automated Planning and Scheduling (ICAPS-05).— 2005.

93. Jensen, R. M. Fault tolerant planning: Toward probabilistic uncertainty models in symbolic non-deterministic planning // Proc. 14th International Conference on Automated Planning and Scheduling ICAPS-04. — 2004.

94. Jensen, R. OBDD-based deterministic planning using the UMOP planning framework // Proc. Workshop on Model-Theoretic Approaches to Planning (AIPS 00).-2000.-Pp. 26-31.

95. Jiang, S. Supervisory control of discrete event systems with CTL* temporal logic specifications / S. Jiang, R. Kumar / / SI AM J. Control Optim. — 2006. — Vol. 44, no. 6.-Pp. 2079-2103.

96. Josephs, M. B. Receptive process theory / M. B. Josephs // Acta Inf.— 1992. Vol. 29, no. 1. - Pp. 17-31.

97. Kabanza, F. Search control in planning for temporally extended goals // Proc. 15th International Conference on Automated Planning and Scheduling (ICAP-S-05). — 2005. — Pp. 130-139.

98. Konolige, K. A deduction model of belief / K. Konolige. — London UK, San Mateo, CA: Pitman Publishing, Morgan Kaufmann, 1986.

99. Korf R. E. Real-time heuristic search / R. E. Korf 11 Artif. Intell. 1990. -Vol. 42, no. 2-3.-Pp. 189-211.

100. Kozen, D. Handbook of Theoretical Computer Science / D. Kozen, J. Tiuryn // Handbook of Theoretical Computer Science / Ed. by J. van Leeuwen. Amsterdam: North-Holland, 1990. - Vol. B. - Pp. 789-840.

101. Kripke, S. Semantical analysis of modal logic I: Normal modal propositional calculi / S. Kripke // Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik. 1963.- no. 9. - P. 67-96.

102. Kwiatkowska, M. Probabilistic symbolic model checking with PRISM: a hybrid approach / M. Kwiatkowska, G. Norman, D. Parker // Int. J. Softw. Tools Technol. Transf. 2004. - Vol. 6, no. 2. - Pp. 128-142.

103. Laroussinie, F. On the expressivity and complexity of quantitative branching-time temporal logics / F. Laroussinie, P. Schnoebelen, M. Turuani // Theor. Comput. Sci. 2003. - Vol. 297, no. 1-3. - Pp. 297-315.

104. Lee, C. Representation of switching circuits by binary-decision programs / C. Lee // Bell System Technical Journal— 1959.— July. — Vol. 38.— Pp. 985-999.

105. Lenat, D. BEINGs: knowledge as interacting experts // Proc. International Joint Conference on Artificial Intelligence. — 1975. — Pp. 126-133.

106. Lenat, D. AM: an artificial intelligence approach to discovery in mathematics as heuristic search.: Ph.D. thesis / Stanford University. — 1976.

107. Levesque, H. J. A logic of implicit and explicit belief // Proc. Fourth National Conference on Artificial Intelligence. Austin, TX: 1984. - P. 198-202.

108. Levesque, H. J. On acting together // Proc. Eighth National Conference on Artificial Intelligence. Boston, MA: 1990. - Pp. 94-99.

109. Lhotâk, O. Jedd: a BDD-based relational extension of Java / O. Lhotâk, L. Hendren // SIGPLAN Not. 2004. - Vol. 39, no. 6. - Pp. 158-169.

110. Lind-Niels en, J. BuDDy — a Binary Decision Diagram package (http://sourceforge.net/projects/buddy).

111. Ljunberg, M. The OASIS air trafic management system // Proc. Second Pacific Rim International Conference on AI. — 1992.

112. Majercik, S. M. MAXPLAN: A new approach to probabilistic planning // Artificial Intelligence Planning Systems. — 1998. — Pp. 86-93.

113. May field, J. Evaluating KQML as an agent communication language / J. May-field, Y. Labrou, T. Finin // Intelligent Agents II.- 1996,- Vol. 1037. — P. 347-360.

114. MBP: a model based planner // Proc. Workshop on Planning under Uncertainty and Incomplete Information (IJCAI 01).— 2001.

115. McDermott, D. Using regression-match graphs to control search in planning / D. McDermott // Artif. IntelL- 1999.- Vol. 109, no. 1-2.- Pp. 111-159.

116. McMillan, K. L. Symbolic model checking / K. L. McMillan. — Dordrecht,The Netherlands: Kluwer Academic Publishers, 1993.

117. Meyer, J.-J. C. A logical approach to the dynamics of commitments / J.-J. C. Meyer, W. van der Hoek, B. van Linder // Artif. IntelL— 1999. — Vol. 113, no. 1-2.-Pp. 1-40.

118. Milner, R. A calculus of communicating systems / R. Milner. — Secaucus, NJ, USA: Springer-Verlag New York, Inc., 1982.

119. Milvang-Jensen, K. BDDNOW: A parallel BDD package // Proc. Second International Conference on Formal Methods in Computer-Aided Design. — London (UK): Springer-Verlag, 1998.- Pp. 501-507.

120. Miraftabi, R. Agents on the loose: An overview of agent technologies. — University of Joensuu. — 2000.

121. MOCHA: Modularity in model checking / R. Alur, T. Henzinger, F. Mang et al. // Lecture Notes in Computer Sciense. — 1998. — Vol. 1427. — P. 521-525.

122. Model checking for multiagent systems: The MABLE language and its applications / M. J. Wooldridge, M.-P. Huget, M. Fisher, S. Parsons // International Journal on Artificial Intelligence Tools.— 2006.— Vol. 15, no. 2.— Pp. 195-225.

123. Model checking multi-agent systems with MABLE // Proc. first international joint conference on Autonomous agents and multiagent systems. — Bologna (Italy): ACM Press, 2002. Pp. 952-959.

124. Moore, R. C. Reasoning about knowledge and action: Tech. rep. / R. C. Moore. — Menlo Park, CA (USA): SRI International, Artificial Intelligence Center, 1980. — October.

125. M.Ryan. Agents and roles: refinement in alternating-time temporal logic // Proc. Eighth International Workshop on Agent Theories, Architectures, and Languages / Ed. by J.-J. C. Meyer, M.Tambe.- Vol. 2333.- 2001. — P. 100-114.

126. NUSMV: A new symbolic model verifier // Proc. 11th International Conference on Computer Aided Verification.— London (UK): Springer-Verlag, 1999. Pp. 495-499.

127. Omicini, A. SODA: societies and infrastructures in the analysis and design of agent-based systems // Proc. First international workshop on Agent-oriented software engineering. — Secaucus (USA): Springer-Verlag New York, Inc., 2001,-Pp. 185-193.

128. On the use of MTBDDs for performability analysis and verification of stochastic systems / H. Hermannsa, M. Kwiatkowskab, G. Normanb et al. // Journal of Logic and Algebraic Programming. — 2003. — May-August. — Vol. 56, no. 1-2. Pp. 23-67.

129. Parker, D. Implementation of symbolic model checking for probabilistic system: Ph.D. thesis / University of Birmingham. — 2002.

130. Parunak, H. V. D. Foundations of Distributed Artificial Intelligence / H. V. D. Parunak // Foundations of Distributed Artificial Intelligence. — Wiley Inter-Science, 1994.

131. Parunak, H. V. D. Multiagent Systems / H. V. D. Parunak // Multiagent Systems / Ed. by G. Weiss. MIT Press, 2001.- Pp. 377-421.

132. Pauly, M. Logical for social software: Ph.D. thesis / University of Amsterdam. 2001.

133. Pauly, M. A modal logic for coalitional power in games / M. Pauly // Journal of Logic for Computation. — 2002. — no. 12. — Pp. 146-166.

134. Pauly, M. Logic for mechanism design — a manifesto // Proc. Workshop on Game Theory and Decision Theory in Agent Systems. — 2003.

135. Pearl, J. Heuristics: intelligent search strategies for computer problem solving / J. Pearl.— Boston, MA, USA: Addison-Wesley Longman Publishing Co., Inc., 1984.

136. Perlis, D. Languages with self-reference I: foundations (or: we can have everything in first-order logic) / D. Perlis // Artificial Intelligence. — 1985. — Vol. 25, no. 3. Pp. 301-322.

137. Perlis, D. Languages with self-reference II: knowledge, belief and modality / D. Perlis 11 Artificial Intelligence.- 1988. -Vol. 34, no. 2.- Pp. 179-212.

138. Perlis, D. Meta in logic / D. Perlis // Meta-Level Architectures and Reflection. 1988. - Pp. 37-49.

139. Pistore, M. Symbolic techniques for planning with extended goals in non-deterministic domains // Proc. 6th European Conference on Planning (ECP 01). — 2001.

140. Pistore, M. The planning spectrum one, two, three, infinity // Proc. 18th Annual IEEE Symposium on Logic in Computer Science. — Washington DC (USA): IEEE Computer Society, 2003. — P. 234.

141. Pratt, V. R. A near-optimal method for reasoning about actions / V. R. Pratt // Computer Systems Sciense. — 1980. — Vol. 2, no. 20. — Pp. 231-254.

142. Program monitoring with LTL in EAGLE // Proc. 18th International Parallel and Distributed Processing Symposium. — Manchester (UK): 2004. — April. — Pp. 264-281.

143. Puterman, M. L. Markov decision processes: Discrete stochastic dynamic programming / M. L. Puterman // Operational Research Society.— 1995.— Vol. 46, no. 6. P. 792.

144. Quantitative temporal reasoning / E. A. Emerson, A. K. Mok, A. P. Sistla, J. Srinivasan // Real-Time Systems. 1992. - Vol. 4, no. 4,- Pp. 331-352.

145. Rao, A. S. Modeling rational agents within a BDI-architecture // Proc. Proceedings of Knowledge Representation and Reasoning (KR&R 91) / Ed. by R. Fikes, E. Sandewall. — San Mateo (USA): Morgan Kaufmann Publishers, 1991.-April.-Pp. 473-484.

146. Rao, A. S. BDI agents: from theory to practice // Proc. First International Conference on Multi-Agent Systems. — San Francisco (USA): 1995. — June. — Pp. 312-319.

147. Rao, A. S. Decision procedures for BDI logics / A. S. Rao, M. P. Georgeff // Journal of Logic and Computation. — 1998. — Vol. 8, no. 3. — Pp. 293-343.

148. Rao, A. S. Modeling rational agents with a BDI-architecture / A. S. Rao, M. P. Georgeff 11 Readings in agents. 1998. - Pp. 317-328.

149. Reasoning about action and cooperation // Proc. Fifth International Joint Conference on Autonomous Agents and Multiagent Systems / Ed. by P. Stone, G. Weiss. New York (USA): ACM Press, 2006. - Pp. 185-192.

150. Reasoning about agents in the KARO framework // Proc. Eighth International Symposium on Temporal Representation and Reasoning (TIME'01).— Washington DC (USA): IEEE Computer Society, 2001.- P. 206.

151. Rule-based runtime verification // Proc. Fifth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI04). — 2004. — January.

152. Sanner, S. Affine algebraic decision diagrams (AADDs) and their application to structured probabilistic inference // Proc. International Joint Conference On Artificial Intelligence. 2005. - Pp. 1384-1391.

153. SatPlan: Planning as satisfiability // Abstracts of the 5th International Planning Competition. — 2006.

154. Searle, J. R. Speech acts: an essay in the philosophy of language / J. R. Sear-le. — Cambridge University Press, 1969. — P. 203.

155. Shannon, C. A symbolic analysis of relay and switching circuits / C. Shannon // Transactions of the AIEE. 1938. - Vol. 57. - Pp. 713-723.

156. SHOP2: An HTN planning system / D. S. Nau, T. C. Au, O. Ilghami et al. // Journal of Artificial Intelligence Research. — 2003. — december. — Vol. 20. — Pp. 379-404.

157. Singh, M. P. A critical examination of the cohen-levesque theory of intentions // Proc. 10th European conference on Artificial intelligence. — Vienna (Austria): John Wiley k Sons, Inc., 1992.- Pp. 364-368.

158. Somenzi, F. CUDD: Colorado University Decision Diagram package (http://vlsi.colorado.edu/ fabio/CUDD/).

159. STeP: The Stanford temporal prover: Tech. rep. / Z. Manna, A. Anuchitanukul, N. Bjorner et al. Stanford, CA, USA: Stanford University, 1994.

160. Thati, P. Monitoring algorithms for metric temporal logic specications // Proc. 4th Intl Workshop on Runtime Verication / Ed. by K. Havelund, G. Rou. 2004.

161. The tool KRONOS // Proc. Workshop on Hybrid systems III : verification and control (DIMACS/SYCON).- New Brunswick (USA): Springer-Verlag New York, Inc., 1996,- Pp. 208-219.

162. UPPAAL — a tool suite for automatic verification of real-time systems // Proc. Workshop on Hybrid systems III : verification and control (DIMACS/SYCON). New Brunswick (USA): Springer-Verlag New York, Inc., 1996. - Pp. 232-243.

163. Wagner, F. Modeling software with finite state machines: a practical approach / F. Wagner. — Auerbach Publications, 2006.

164. Wooldridge, M. J. The logical modeling of computational multi-agent systems: Ph.D. thesis / University of Manchester. — 1992.— September. — P. 153.

165. Wooldridge, M. J. Reasoning about rational agents / M. J. Wooldridge.— Cambridge, MA: The M. I. T. Presss, 2000.

166. Wooldridge, M. J. Intelligent agents: Theory and practise / M. J. Wooldridge, N. R. Jennings // The Knowledge Engineering Review. — 1995.

167. Wooldridge, M. J. The Gaia methodology for agent-oriented analysis and design / M. J. Wooldridge, N. R. Jennings, D. Kinny // Autonomous Agents and Multi-Agent Systems. 2000. - Vol. 3, no. 3. - Pp. 285-312.

168. Yin, G. G. Continuous-time markov chains and applications: a singular perturbation approach / G. G. Yin. — Springer, 1998.

169. Yin, G. G. Discrete-time markov chains: two-time-scale methods and applications / G. G. Yin, Z. Qing. Springer, 2005. - P. 347.

170. Yu, E. Modelling strategic relationships for process reengineering: Ph.D. thesis / University of Toronto, Department of Computer Science. — 1995.