WWW.DISSERS.RU

БЕСПЛАТНАЯ ЭЛЕКТРОННАЯ БИБЛИОТЕКА

загрузка...
   Добро пожаловать!

Pages:     | 1 || 3 |

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

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

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

• Des оператор, используемый для описания желаний агента.

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

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

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

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

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

• A A G коалиция A ведет себя таким образом, что на любом пути всегда выполнено свойство. Такие свойства называют свойствами безопасности.

• A ©( B Bel ( E ©)) если из состояния, удовлетворяющего, система перейдет в состояние, удовлетворяющее, то коалиция B будет знать, что такой переход возможен.

• A A G (Des A F ) коалиция A ведет себя таким образом, что на любом пути всегда при возникновении у нее желания реализовать не более чем через 10 тактов будет реализовано. Такие свойства называют свойствами живучести.

• A Des Bel E F Intend если коалиция A хочет реализовать свойство и считает, что существует путь, на котором оно может быть реализовано, то она будет пытаться реализовать это свойство.

• A G (A F ) (A F ¬) система в целом ведет себя таким 16 образом, что свойства и ¬ чередуются с периодом не более тактов.

• C Intend A F если коалиция C решила реализовать свойство, то она этого когда-нибудь добьется.

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

следуя которому система будет удовлетворять требуемым свойствам.

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

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

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

В главе 8 предлагается новый подход к решению задачи накопления опыта системой, использующий символическое представление данных в виде разрешающих диаграмм. Опыт агента представляются в виде функции res : S ACS S N (где ACS есть декартово произведение множеств действий всех агентов системы, а N есть множество натуральных чисел), представленной с помощью разрешающих диаграмм.

Результат функция res в точке (s, a, s ) S ACS S описывает сколько раз результатом выполнения системой в состоянии s S действия a ACS являлось состояние s S.

Для предложенного представления опыта описаны такие операции как добавления факта, интеграции опыта нескольких агентов, а также получение описания представлений агента bel S ACS S, построенного с использованием порога отсечения [0, 1] следующим образом: bel = {(s, a, s ) S ACS S | res(s, a, s ) · max res(s, a, s )}.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

[5] Бугайченко, Д. Ю., Соловьев, И. П. Абстрактная архитектура интеллектуального агента и методы ее реализации. // Системное программирование. 2005. №1. C. 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., Soloviev, I. P. MASL: A Logic for the Specification of Multiagent Real-Time Systems. // Proc. of the 5th 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 /ACM 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. Henzinger, O. Kupferman // J. ACM. 2002. Vol. 49, no. 5. Pp. 672–713.

[14] 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.

[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. / E. A. Emerson // Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B). North-Holland Pub. Co., 1990. Pp. 995–1072.

[17] Haigh, K. 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] Henzinger, T. A. Timed alternating-time temporal logic // 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. 1–17.

Pages:     | 1 || 3 |






© 2011 www.dissers.ru - «Бесплатная электронная библиотека»