Курс лекций–семинаров на тему «Модальные логики и многоагентные системы»
Каждый вторник начиная с 10.09.2019 с 16:40 до 19:30, в аудитории 506, Таллинская, д 34. известный специалист в области верификации и логики Юрий Глебович Карпов прочтет в МИЭМ НИУ ВШЭ курс лекций – семинаров на тему «Модальные логики и многоагентные системы». Аналоги этого курса также читаются в Стенфорде, MIT, МФТИ.
План курса "Модальные логики и многоагентные системы"
1. Мотивация
Необходимость использования модальной логики для решения проблем в новой парадигме существования общества - социальные системы, в которых и люди,
и машины являются членами коллективов взаимодействующих агентов.
2. Примеры
"Сильные" и "слабые" характеризации истины. Модальности. Примеры задач, формулировка и решение которых использует разнообразные модальности.
3. Модальная логика
Синтаксис и семантика модальной логики. Модели и шкалы Крипке.
Теория корреспонденции. Аксиоматические системы модальных логик.
4. Конкретные модальные логики и их приложения
4.1. Модальная эпистемическая логика - логика знаний MEL
а) формализация проблем с помощью эпистемических моделей;
б) рассуждения 'с точки зрения другого' и социальное взаимодействие;
в) знания в группе агентов, "групповое" и "общее" знание;
г) "общее" знание и социальная координация.
4.2. Темпоральные логики - логики времени
а) линейное и ветвящееся время, темпоральные логики LTL, CTL*, CTL.
б) формализация требований к поведению программных и аппаратных систем;
в) верификация программных и аппаратных систем;
г) синтез супервизорного управления координированным поведением систем.
4.3. Деонтические логики - логики законов и норм
а) деонтическая логика: формализация 'нормативных' рассуждений;
б) проблемы и парадоксы деонтической логики SDL;
в) электронные контракты;
г) нормативная темпоральная логика NTL; анализ и синтез коллективов агентов с нормативным поведением.
5. Философская составляющая
Даже поверхностное изложение модальных логик не может не касаться глубоких философских проблем. Определяются ли все свойства знания аксиомами логики MEL? Что такое время? Почему логика столь необычайно эффективна в компьютерных науках? Что такое этика и мораль? Все эти вопросы так или иначе затрагиваются в курсе.
6. Курсовые (самостоятельные) работы
1) Принятие решений в карточных играх. Игра "тузы и восьмерки". MEL.
2) Спецификация требований и верификация аппаратных систем с памятью. LTL.
3) Верификация программных управляющих систем. CTL.
4) Синтез многоагентных систем с координированным поведением агентов. NTL.
Дополнительная информация доступна по ссылке.