Математические модели последовательных вычислений

Обязательный курс для студентов 618 групп на 12 семестре обучения.

Лекционная нагрузка — 18 ч.

Курс читает профессор В. А. Захаров.

Лекции

Лекция 1. Сети Петри: происхождение, основные понятия, область применения, свойства вычислений.

Лекция 2. Проблемы ограниченности и безопасности для обыкновенных сетей Петри. Деревья покрытия разметок сетей Петри. Метод проверки свойства ограниченности вычислений обыкновенных сетей Петри при помощи деревьев покрытий разметок. Проблема достижимости для обыкновенных сетей Петри и ее варианты. Проблема живости для обыкновенных сетей Петри. Взаимная сводимость проблем живости и достижимости.

Лекция 3. Проблема R-эквивалентности для обыкновенных сетей Петри. Диофантовы уравнения и некоторые их свойства. Моделирование многочленов обыкновенными сетями Петри. Неразрешимость проблемы R-эквивалентности для обыкновенных сетей Петри. Языки, порождаемые сетями Петри. Примеры языков, порождаемых сетями Петри. Сравнение класса языков, порождаемых обыкновенными сетями Петри, и классов языков иерархии Хомского.

Лекция 4. Разнообразие классов сетей Петри. Ординарные сети Петри. Моделирование обыкновенных сетей Петри ординарными сетями. Автоматные сети Петри. Синхронизационные сети Петри. Сети потоков работ. Ингибиторные сети Петри. Моделирование счетчиковых машин Минского ингибиторными сетями Петри. Раскрашенные сети Петри. Вложенные сети Петри

Лекция 5. Проблема эквивалентности программ и трудности ее решения. Моделирование программ схемами программ. Стандартные схемы программ: синтаксис и семантика. Вычисления стандартных схем программ. Задачи анализа поведения стандартных схем программ - проблемы пустоты, тотальности, эквивалентности, свободы схем программ.

Лекция 6. Описание стандартных схем программ при помощи систем переходов и алгебры подстановок. Эрбрановские интерпретации для стандартных схем программ. Эквивалентность стандартных схем программ на эрбрановских интерпретациях. Неразрешимость проблем анализа поведения стандартных схем программ. Схемы программ Ляпунова-Янова. Взаимосвязь схем программ Ляпунова-Янова и конечных автоматов. Разрешимость проблемы эквивалентности для схем Ляпунова-Янова.

Лекция 7. Логико-термальная эквивалентность стандартных схем программ. Аппроксимируемость функциональной эквивалентности программ логико-термальной эквивалентностью схем программ. Граф совместных вычислений стандартных схем программ. Операция антиунификации подстановок и ее свойства. Алгоритм вычисления наиболее специального шаблона двух подстановок. Алгоритм разметки графа совместных вычислений. Разрешимость проблемы логико-термальной эквивалентности стандартных схем программ.

Лекция 8. Алгебраические модели систем взаимодействующих процессов. Алгебра процессов: синтаксис. Алгебра процессов: операционная семантика. Процессные графы и темпоральные логики. Отношение бисимуляции. Рекурсия. Абстракция и ветвящаяся бисимуляция. Применение алгебры процессов в задачах верификации распределенных систем.

Лекция 9. Особенности мобильной связи. π-исчисление мобильных процессов. Синтаксис π-исчисления. Операционная семантика π-исчисления. Моделирование криптографических протоколов. spi-исчисление и его особенности. Применение spi-исчисления в криптоанализе.

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

Сети Петри

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 с.