Дипломная работа студента 545 группы Сынтульского Сергея Научный Игорь Павлович Соловьев



страница1/15
Дата01.02.2013
Размер0.78 Mb.
ТипДиплом
  1   2   3   4   5   6   7   8   9   ...   15


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

УНИВЕРСИТЕТ

Математико-механический факультет

Кафедра системного программирования

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

Дипломная работа студента 545 группы Сынтульского Сергея
Научный руководитель, ____________ Игорь Павлович Соловьев

кфмн
Рецензент, ____________

1. Введение 4

1.1. Темпоральные логики 4

1.1.1. Представление времени в логиках 5

1.1.2. Темпоральные логики 7

1.1.3. Вероятностные темпоральные логики 10

1.2. Символьная реализация алгоритмов проверки модели 12

1.3. Представление вероятностных моделей с использованием языка PRISM 13

1.4. Оптимизация на основе марковской модели 16

2. Классы задач 18

2.1. Задачи мультиагентных систем 18

2.2. Задачи логик с альтернирующим временем 19

2.3. Задачи вероятностных логик 20

2.4. Области приложений PTATL 21

3. Вероятностная логика с альтернирующим временем и явными временными ограничениями 22

3.1. Вероятностная структура параллельной игры 22

3.1.1. Представление PCGS с помощью PRISM 23

3.1.2. Пример модели рынка 24

3.2. Внутренний язык 27

3.2.1. Синтаксис 27

3.2.2. Семантика 27

3.3. Синтаксис PTATL 28

3.3.1. Квантор возможности 30

3.3.2. Дополнительные операторы 31

3.4. Семантика PTATL 31

3.4.1. Стратегии и выходы 31

3.4.2. Семантика PTATLs 32

3.4.3. Время в PTATLc 33

3.4.4. Семантика PTATLc 34

4. Практическая часть. Методы проверки модели 35

4.1. Метод проверки модели для PTATLc 35

4.1.1. Проверка модели для формул, образованных нетемпоральными операторами 36

4.1.2. Проверка модели для утверждений о следующем состоянии 36

4.1.3. Проверка модели для формул, образованных оператором U 37

4.1.4. Проверка модели для формул, образованных оператором W 39

4.2. Алгоритм проверки модели для PTATLs 39

4.2.1. Преобразование PCGS в MDP 40

4.2.2. Пример преобразования PCGS в MDP 42

4.2.3. Служебные функции 44

4.2.4. Проверка модели для утверждений о следующем состоянии 45

4.2.5. Проверка модели для ограниченного оператора Until 46

5. Приложения 47

5.1. Моделирование производственных систем 47

5.2. Приложения в области финансов 50

5.2.1. Задача вывода инвестиций из разоряющегося предприятия 50

5.2.2. Оценка контрактов 52

5.3. Приложения в области медицины 56

6. Заключение 57

7. Литература 58

7.1. Моделирование производственных систем 60

7.2.
Формально-логические подходы в медицине 60

7.3. Финансовая математика 61

  1. Введение


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

В данной работе предлагается логический подход к спецификации систем, состоящих из нескольких агентов, действия которых могут оказывать недетерминированный (вероятностный) эффект на состояние системы в целом. А именно, автором предлагается логика PTATL (Probabilistic Timed Temporal Logic), позволяющая для модели системы описывать способность различных групп агентов повлиять на ее состояние.

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

Изложение имеет следующий план. Во введении описываются темпоральные логики, а также ключевые аспекты реализации инструментов проверки моделей. Глава 2 содержит описания ряда прикладных областей, для решения задач которых могла бы быть применена предлагаемая в данной работе логика PTATL. В главе 3 приводится описание синтаксиса и семантики PTATL. В главе 4 описываются алгоритмы проверки моделей. В заключительной главе 5 рассматриваются примеры решения конкретных задач некоторых из предложенных в главе 2 областей.
  1   2   3   4   5   6   7   8   9   ...   15

Похожие:

Дипломная работа студента 545 группы Сынтульского Сергея Научный Игорь Павлович Соловьев iconДипломная работа студента 5 курса группы №543 Наумова Сергея Сергеевича Научный
Применение распараллеливания для итерационной триангуляции с измельчением вблизи границы
Дипломная работа студента 545 группы Сынтульского Сергея Научный Игорь Павлович Соловьев iconДипломная работа студента 545 группы Расторгуева Алексея Сергеевича Научный руководитель Пименов А. А. /подпись
Стерео реконструкция – задача определения координат точек в трехмерном пространстве на основании их положения на кадрах видеоряда...
Дипломная работа студента 545 группы Сынтульского Сергея Научный Игорь Павлович Соловьев iconДипломная работа студента 545 группы
Исследование необходимости поддержки структурных изменений в источниках данных 35
Дипломная работа студента 545 группы Сынтульского Сергея Научный Игорь Павлович Соловьев iconДипломная работа студента 545 группы
Разработка технологии взаимодействия гетерогенных систем с использованием метапрограммирования
Дипломная работа студента 545 группы Сынтульского Сергея Научный Игорь Павлович Соловьев iconДипломная работа студента 545 группы Ромашкина Амира Сергеевича
Система анализа реконструктивных хирургических операций при помощи Microsoft Kinect
Дипломная работа студента 545 группы Сынтульского Сергея Научный Игорь Павлович Соловьев iconДипломная работа студента 545 группы
Следует заметить, что даже осциллограммы одинаковых звуковых фрагментов одного диктора, записанные в разное время с большой долей...
Дипломная работа студента 545 группы Сынтульского Сергея Научный Игорь Павлович Соловьев iconДипломная работа студента 545 группы
До недавнего времени, хирург при подготовке к пластической операции мог использовать либо дорогостоящий мрт сканер, либо производить...
Дипломная работа студента 545 группы Сынтульского Сергея Научный Игорь Павлович Соловьев iconДипломная работа студента 545 группы
Нужно заметить, что задача распознавания считается задачей классификации, в которой классы либо задаются дизайнером системы(в распознавании...
Дипломная работа студента 545 группы Сынтульского Сергея Научный Игорь Павлович Соловьев iconДипломная работа студента 545 группы
Такие инструменты автоматически порождают алгоритм, выполняющий синтаксически-управляемую трансляцию по заданной спецификации трансляции....
Дипломная работа студента 545 группы Сынтульского Сергея Научный Игорь Павлович Соловьев iconДипломная работа студента 544 группы Вахитова Александра Тимуровича Научный
Метод подстройки пользовательских приоритетов при поиске по коллекциям изображений 28
Разместите кнопку на своём сайте:
ru.convdocs.org


База данных защищена авторским правом ©ru.convdocs.org 2016
обратиться к администрации
ru.convdocs.org