WWW.DISSERS.RU

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

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

Pages:     || 2 | 3 |
САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

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

Бугайченко Дмитрий Юрьевич РАЗРАБОТКА И РЕАЛИЗАЦИЯ МЕТОДОВ ФОРМАЛЬНО-ЛОГИЧЕСКОЙ СПЕЦИФИКАЦИИ САМОНАСТРАИВАЮЩИХСЯ МУЛЬТИАГЕНТНЫХ СИСТЕМ С ВРЕМЕННЫМИ ОГРАНИЧЕНИЯМИ 05.13.11 Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

АВТОРЕФЕРАТ

диссертации на соискание ученой степени кандидата физико-математических наук

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

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

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

Официальные оппоненты: доктор физико-математических наук, профессор Баранов Сергей Николаевич кандидат физико-математических наук, доцент, Кознов Дмитрий Владимирович

Ведущая организация: Санкт-Петербургский институт информатики и автоматизации РАН

Защита диссертации состоится “ ” 2007 года в часов на заседании диссертационного совета Д212.232.51 по защите диссертаций на соискание ученой степени доктора наук при Санкт-Петербургском государственном университете по адресу 198504, Санкт-Петербург, Старый Петергоф, Университетский пр., д. 28, математико-механический факультет Санкт-Петербургского государственного университета.

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

Автореферат разослан “ ” 2007 г.

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

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

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

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

Кроме того, для подобных систем особенно остро стоит вопрос корректности их поведения.

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

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

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

CT L расширяет классическую логику высказываний темпоральными операторами “в следующий момент ” © и “когда-нибудь, а до тех пор ” U и кванторами “на любом пути...” A и “существует путь на котором...” E.

Для спецификации систем с временными ограничениями предложены различные расширения логики CT L. Например, логика RT CT L [22] расширяет CT L ограниченным оператором U, интерпретируеt мым как “не более чем через t шагов, а до тех пор ”. Основным достоинством RT CT L является сохранение билинейной сложности задачи верификации. Большей выразительной мощности, за счет увеличения вычислительной сложности, можно достичь введя переменные часов (x, y,...) и квантор фиксации (·) [12]: x · A U ((x t) ).

Основным ограничением CT L является отсутствие явных средств спецификации систем, состоящих из нескольких взаимодействующих сущностей. Это ограничение преодолевается в логике альтернированного времени AT L [13], позволяющей учитывать многокомпонентность системы в явном виде. AT L включает конечное множество игроковагентов P и заменяет кванторы CT L на квантор “для коалиция игроков C P существует такая стратегия, что на любом пути...” C.

Для AT L также были предложены методы спецификации ограничений на время реакции, например, с помощью подстрочного индекса [19] или с помощью переменных часов [18].

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

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

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

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

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

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

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

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

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

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

Методы исследования. В диссертации используются теория и методы современной математической логики, включая модальные и темпоСинтаксис логики линейного времени LT L включает те же темпоральные операторы, что и логика ветвящегося времени CT L, но не включает кванторов путей, так как семантика LT L предполагает только один возможный вариант будущего.

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

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

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

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

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

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

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

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

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

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

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

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

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

1. Конференция Технологии Microsoft в теории и практике, Россия, Санкт-Петербург, 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 наименований. Объем основной части работы страницы, полный объем работы 260 страниц.

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

Глава 1 начинается с введения основных понятий и рассмотрения основных свойств, присущих интеллектуальному агенту. В главе описана модель интеллектуального агента, представленного как набор ag = (S, A, env, see, IB, bel, brf, ID, des, drf, plan, prf), где • S есть непустое конечное множество состояний внешней среды;

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

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

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

• IB = Ibel 2P AP есть множество представлений агента;

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

• brf : IB A P IB есть функция обновления представлений;

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

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

• drf : ID P ID есть функция обновления желаний;

• plan = (P, A, Ipln, pln, ipln,0) есть текущий план агента, представленный конечным автоматом с входным алфавитом P, выходным алфавитом A, множеством состояний Ipln, отношением переходов pln и начальным состоянием ipln,0;

• prf : IB ID 2P lan P 2P lan есть функция обновления плана, где P lan есть множество всех возможных планов.

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

Pages:     || 2 | 3 |






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