Докладчик: проф. Ю. Г. Карпов icon

Докладчик: проф. Ю. Г. Карпов


1 чел. помогло.
Смотрите также:
В. И. Голубев проф. А. А. Дюжиков чл корр. Рамн е. З. Голухова акад. Рамн и. И. Затевахин проф...
Учебник написан в полном соответствии с новой программой изучения дисциплины "Основы...
Десятая Казанская летняя школа-конференция «Теория функций...
1. Научный доклад «Возможности хирургического лечения ишемического инсульта в ранние сроки...
Программа чл корр. Ран соломенцев Ю. М. Заместители руководителя...
Отчет по результатам нир «Исследование вопросов реформирования деятельности мсэ и подготовка...
Отчет по диссертационной работе на соискание ученой степени кандидата технических наук на тему:...
О. Н. Громова д э. н., проф...
Экзаменационные задания к итоговой государственной аттестации выпускников огма по специальности...
Храпылина Л. П., д э. н., проф.; Щербаков А. И., к э. н., доц...
О. В. Иншаков Редакционная коллегия...
Воспалительные заболевания кишечника – диагностические и терапевтические стратегии”...



Загрузка...
скачать
Четыре семинара по верификации дискретных систем

Докладчик: проф. Ю.Г.Карпов
(Санкт-Петербургский политехнический университет)
karpov@dcn.infos.ru

Доклады семинара освещают новые результаты теоретической информатики, получившие множество применений на практике. Изложение материала доступно студентам младших курсов, знакомым с логикой и теорией конечных автоматов. Подготовка материала была поддержана грантом фирмы Intel № SPB/R&D/139/2006.


  1. Темпоральная логика и верификация реактивных систем (Model checking)

Темпоральная логика –модальная логика, позволяющая формализовать высказывания, зависящие от времени. В докладе рассматривается логика ветвящегося времени CTL* и ее подклассы – логики CTL и LTL. Истинность либо ложность формул этих логик определяется на структуре Крипке – одном из формализмов реактивных систем с конечным числом состояний. Структура Крипке К называется “моделью” темпоральной формулы Ф, если Ф истинна на К. Проверка модели (model checking) – это алгоритм, позволяющий для систем, представленных в форме структуры Крипке, проверить свойства их поведения, выраженные в виде формул темпоральной логики. Разработанная в конце прошлого века, темпоральная логика широко используется для формулировки свойств корректного поведения дискретных систем, взаимодействующих друг с другом и окружением. Моделью реактивных систем описываются параллельные программы, коммуникационные протоколы, дискретные схемы и т.п.


  1. Применения и расширения алгоритма “проверки модели”

Алгоритм “проверки модели” в последнее время нашел много новых применений в информатике. В докладе рассматриваются применения этого алгоритма для решения логических задач, для классической проблемы планирования в области искусственного интеллекта, при верификации криптографических протоколов, в анализе стохастических систем.


  1. Бинарные решающие диаграммы

Булевы функции широко применяются в течение многих десятков лет. Казалось бы, в этой области трудно придумать что-то радикально новое. Бинарные решающие диаграммы (Binary Decision Diagrams, BDD) – это новая экономная форма представления булевых функций. Поскольку базовые структуры данных (конечные множества и отношения) и операции над ними легко выражаются с помощью булевых функций и булевых операций, то многие алгоритмы на конечных структурах данных, представленных в форме BDD, становятся очень эффективными. BDD совершили революцию в представлении данных и алгоритмах работы с ними. Во многих областях на основе BDD строятся новые зффективные алгоритмы.


  1. Символьная верификация

Символьная верификация - один из самых удивительных примеров применения BDD для построения эффективных алгоритмов. Возможность повышения эффективности некоторого класса алгоритмов даже на 15-20%, обычно вызывает большой интерес. В докладе представлен алгоритм, позволяющий увеличить сложность систем, для которых возможно выполнить алгоритм Model checking, в миллионы миллионов раз. Это помогает преодолеть “проклятие размерности”, “проблему взрыва числа состояний”, возникающие при анализе параллельных систем, и выполнять с помощью этого подхода верификацию схем и параллельных программ, применяемых на практике.




оставить комментарий
Дата03.10.2011
Размер21,4 Kb.
ТипДоклад, Образовательные материалы
Добавить документ в свой блог или на сайт

не очень плохо
  1
отлично
  1
Ваша оценка:
Разместите кнопку на своём сайте или блоге:
rudocs.exdat.com

Загрузка...
База данных защищена авторским правом ©exdat 2000-2017
При копировании материала укажите ссылку
обратиться к администрации
Анализ
Справочники
Сценарии
Рефераты
Курсовые работы
Авторефераты
Программы
Методички
Документы
Понятия

опубликовать
Загрузка...
Документы

Рейтинг@Mail.ru
наверх