Ю. Г. Карпов (Санкт-Петербургский политехнический университет) karpov@dcn infos ru Доклад
| Вид материала | Доклад |
- Платонова Мария Валерьевна ( platonova m v@mail ru ), (495) 916-89-85 Карпов Валерий, 24.79kb.
- Статьи, 39kb.
- Программа международной научной конференции «коммуникация в поликодовом пространстве:, 304.38kb.
- Организационный взнос, 70.54kb.
- Министерство образования и науки РФ санкт-петербургский государственный политехнический, 63.7kb.
- Министерство образования Российской Федерации Санкт-Петербургский государственный политехнический, 2776.63kb.
- Санкт-петербургский государственный политехнический университет, 4180.96kb.
- Федеральное агентство по образованию, 47.63kb.
- Санкт-петербургский государственный политехнический университет, 555.89kb.
- Комплексная методика оценки налогового потенциала региона, 342.11kb.
Четыре семинара по верификации дискретных систем
Докладчик: проф. Ю.Г.Карпов
(Санкт-Петербургский политехнический университет)
karpov@dcn.infos.ru
Доклады семинара освещают новые результаты теоретической информатики, получившие множество применений на практике. Изложение материала доступно студентам младших курсов, знакомым с логикой и теорией конечных автоматов. Подготовка материала была поддержана грантом фирмы Intel № SPB/R&D/139/2006.
- Темпоральная логика и верификация реактивных систем (Model checking)
Темпоральная логика –модальная логика, позволяющая формализовать высказывания, зависящие от времени. В докладе рассматривается логика ветвящегося времени CTL* и ее подклассы – логики CTL и LTL. Истинность либо ложность формул этих логик определяется на структуре Крипке – одном из формализмов реактивных систем с конечным числом состояний. Структура Крипке К называется “моделью” темпоральной формулы Ф, если Ф истинна на К. Проверка модели (model checking) – это алгоритм, позволяющий для систем, представленных в форме структуры Крипке, проверить свойства их поведения, выраженные в виде формул темпоральной логики. Разработанная в конце прошлого века, темпоральная логика широко используется для формулировки свойств корректного поведения дискретных систем, взаимодействующих друг с другом и окружением. Моделью реактивных систем описываются параллельные программы, коммуникационные протоколы, дискретные схемы и т.п.
- Применения и расширения алгоритма “проверки модели”
Алгоритм “проверки модели” в последнее время нашел много новых применений в информатике. В докладе рассматриваются применения этого алгоритма для решения логических задач, для классической проблемы планирования в области искусственного интеллекта, при верификации криптографических протоколов, в анализе стохастических систем.
- Бинарные решающие диаграммы
Булевы функции широко применяются в течение многих десятков лет. Казалось бы, в этой области трудно придумать что-то радикально новое. Бинарные решающие диаграммы (Binary Decision Diagrams, BDD) – это новая экономная форма представления булевых функций. Поскольку базовые структуры данных (конечные множества и отношения) и операции над ними легко выражаются с помощью булевых функций и булевых операций, то многие алгоритмы на конечных структурах данных, представленных в форме BDD, становятся очень эффективными. BDD совершили революцию в представлении данных и алгоритмах работы с ними. Во многих областях на основе BDD строятся новые зффективные алгоритмы.
- Символьная верификация
Символьная верификация - один из самых удивительных примеров применения BDD для построения эффективных алгоритмов. Возможность повышения эффективности некоторого класса алгоритмов даже на 15-20%, обычно вызывает большой интерес. В докладе представлен алгоритм, позволяющий увеличить сложность систем, для которых возможно выполнить алгоритм Model checking, в миллионы миллионов раз. Это помогает преодолеть “проклятие размерности”, “проблему взрыва числа состояний”, возникающие при анализе параллельных систем, и выполнять с помощью этого подхода верификацию схем и параллельных программ, применяемых на практике.