Версия 10:30, 6 апреля 2023

Обязательный курс для студентов групп 618/1 и 618/2. Курс читает В. В. Подымов.

Актуальность информации: весенний семестр 2022/2023 учебного года.

Слайды лекций

Блок 1. О чём этот курс. Литература.

Блок 2. Сети Петри: происхождение, основные понятия.

Блок 3. Сети Петри: примеры применения и свойства поведения.

Блок 4. Проблемы ограниченности и безопасности сетей Петри. Деревья покрытия разметок.

Блок 5. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.

Блок 6. Проблемы достижимости и живости для сетей Петри.

Блок 7. Диофантовы уравнения.

Блок 8. Моделирование многочленов сетями Петри.

Блок 9. Проблемы R-включения и R-эквивалентности для сетей Петри.

Блок 10. Языки сетей Петри.

Блок 11. Другие виды сетей Петри.

Блок 12. Проблема эквивалентности программ. Схемы программ.

Блок 13. Схемы Ляпунова-Янова.

Блок 14. Стандартные схемы программ.

Блок 15. Подстановки. Системы переходов стандартных схем программ.

Блок 16. Проблемы функциональной эквивалентности, пустоты и свободы для стандартных схем программ.

Блок 17. Двухголовочные автоматы.

Блок 18. Эрбрановские интерпретации для стандартных схем программ.

Блок 19. Неразрешимость основных проблем для стандартных схем программ

Блок 20. Алгебра процессов. Базовая алгебра процессов (BPA).

Блок 21. Алгебра процессов с параллелизмом (PAP).

Блок 22. Алгебра взаимодействующих процессов (ACP).

Блок 23. Бисимуляция процессов.

Слайды будут появляться по мере проведения занятий

Прошлогодние слайды

Лекция 1. Лекция 2. Лекция 3. Лекция 4. Лекция 5. Лекция 6. Лекция 7. Лекция 8. Лекция 9.

Программа курса

Сети Петри

1. Сети позиций и переходов. Мультимножества и операции над ними. Разметки. Сети Петри.
2. Условия срабатывания переходов. Отношение срабатывания переходов. Вычисления обыкновенных сетей Петри. Достижимые и тупиковые разметки. Граф достижимых разметок обыкновенной сети Петри.
3. Сравнение разметок. Теорема о свойстве монотонности вычислений обыкновенных сетей Петри.
4. Свойства ограниченности, безопасности и консервативности сетей Петри.
5. Свойства живости и устойчивости сетей Петри.
6. Проблемы достижимости и R-эквивалентности для сетей Петри.
7. Моделирование многочленов обыкновенными сетями Петри. Неразрешимость проблемы R-эквивалентности для обыкновенных сетей Петри.
8. Языки, порождаемые сетями Петри. Примеры языков, порождаемых сетями Петри. Сравнение класса языков, порождаемых обыкновенными сетями Петри, и классов языков иерархии Хомского.
9. Ординарные сети Петри. Моделирование обыкновенных сетей Петри ординарными сетями.
10. Автоматные сети Петри. Моделирование конечных автоматов автоматными сетями Петри.
11. Синхронизационные сети Петри. Условия живости и консервативности для синхронизационных сетей Петри.
12. Сети потоков работ.
13. Ингибиторные сети Петри. Моделирование счетчиковых машин Минского ингибиторными сетями Петри.
14. Раскрашенные сети Петри.
15. Вложенные сети Петри

Схемы программ

16. Проблема эквивалентности программ и трудности ее решения. Моделирование программ схемами программ.
17. Стандартные схемы программ: синтаксис и семантика. Вычисления стандартных схем программ.
18. Задачи анализа поведения стандартных схем программ - проблемы пустоты, тотальности, эквивалентности, свободы схем программ.
19. Представление стандартных схем программ при помощи систем переходов и алгебры подстановок.
20. Эрбрановские интерпретации для стандартных схем программ. Эквивалентность стандартных схем программ на эрбрановских интерпретациях.
21. Неразрешимость проблем анализа поведения стандартных схем программ.
22. Схемы программ Ляпунова-Янова.
23. Взаимосвязь схем программ Ляпунова-Янова и конечных автоматов. Разрешимость проблемы эквивалентности для схем Ляпунова-Янова.
24. Логико-термальная эквивалентность стандартных схем программ. Аппроксимируемость функциональной эквивалентности программ логико-термальной эквивалентностью схем программ.
25. Граф совместных вычислений стандартных схем программ.
26. Операция антиунификации подстановок и ее свойства. Алгоритм вычисления наиболее специального шаблона двух подстановок.
27. Алгоритм разметки графа совместных вычислений. Разрешимость проблемы логико-термальной эквивалентности стандартных схем программ.

Алгебры процессов и Π-исчисление

28. Алгебра процессов: синтаксис и семантика.
29. Процессные графы и темпоральные логики. Отношение бисимуляции.
30. Рекурсия. Абстракция и ветвящаяся бисимуляция.
31. Применение алгебры процессов в задачах верификации распределенных систем
32. Особенности мобильной связи. π-исчисление процессов. Операционная семантика π-исчисления.
33. Криптографические протоколы. spi-исчисление: синтаксис и семантика. Применение spi-исчисления в криптоанализе.

Литература

1. Котов В.Е. Сети Петри - М.: Мир, 1984. - 160 с.
2. Питерсон Дж. Теория сетей Петри и моделирование систем. - М.: Мир, 1984.- 264 с.
3. Ломазова И.А. Вложенные сети Петри: моделирование м анализ распределенных систем с объектной структурой - М.: Научный мир, 2004. - 207 с.
4. Reisig W. Understanding Petri Nets: Modeling Techniques, Analysis Methods, Case Studies. - Springer, 2013. - 211 p.
5. Котов В.Е., Сабельфельд В.К. Теория схем программ - М.: Мир, 1983. - 270 с.