Математические модели последовательных вычислений — различия между версиями

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
(→‎Лекции)
м
 
(не показаны 23 промежуточных версий 3 участников)
Строка 1: Строка 1:
−
Обязательный курс для студентов 618 групп на 12 семестре обучения.
+
[[Категория:Лекционные курсы кафедры МК (архив)]]
  
−
Лекционная нагрузка — 18 ч.
+
Обязательный курс для студентов групп 618/1 и 618/2. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].
  
−
Курс читает профессор [[Захаров Владимир Анатольевич|В. А. Захаров]].
+
Актуальность информации: весенний семестр 2022/2023 учебного года.
  
−
[[Категория:Лекционные курсы кафедры МК]]
+
= Слайды лекций =
  
−
== Лекции ==
+
[[Media: MMSC_VP_01.pdf| Блок 1.]] О чём этот курс. Литература.
  
−
'''[[Media: Lecture_PM_1.pdf| Лекция 1.]]''' Сети Петри: происхождение, основные понятия, область применения, свойства вычислений.
+
[[Media: MMSC_VP_02.pdf| Блок 2.]] Сети Петри: происхождение, основные понятия.
  
−
'''[[Media: Lecture_PM_2.pdf| Лекция 2.]]''' Проблемы ограниченности и безопасности для обыкновенных сетей Петри. Деревья покрытия разметок сетей Петри. Метод проверки свойства ограниченности вычислений обыкновенных сетей Петри при помощи деревьев покрытий разметок. Проблема достижимости для обыкновенных сетей Петри и ее варианты. Проблема живости для обыкновенных сетей Петри. Взаимная сводимость проблем живости и достижимости.
+
[[Media: MMSC_VP_03.pdf| Блок 3.]] Сети Петри: примеры применения и свойства поведения.
  
−
'''[[Media: Lecture_PM_3.pdf| Лекция 3.]]''' Проблема R-эквивалентности для обыкновенных сетей Петри. Диофантовы уравнения и некоторые их свойства. Моделирование многочленов обыкновенными сетями Петри. Неразрешимость проблемы R-эквивалентности для обыкновенных сетей Петри. Языки, порождаемые сетями Петри. Примеры языков, порождаемых сетями Петри. Сравнение класса языков, порождаемых обыкновенными сетями Петри, и классов языков иерархии Хомского.
+
[[Media: MMSC_VP_04.pdf| Блок 4.]] Проблемы ограниченности и безопасности сетей Петри. Деревья покрытия разметок.
  
−
'''[[Media: Lecture_PM_4.pdf| Лекция 4.]]''' Разнообразие классов сетей Петри. Ординарные сети Петри. Моделирование обыкновенных сетей Петри ординарными сетями. Автоматные сети Петри. Синхронизационные сети Петри. Сети потоков работ. Ингибиторные сети Петри. Моделирование счетчиковых машин Минского ингибиторными сетями Петри. Раскрашенные сети Петри. Вложенные сети Петри
+
[[Media: MMSC_VP_05.pdf| Блок 5.]] Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.
  
−
'''[[Media: Lecture_PM_5.pdf| Лекция 5.]]''' Проблема эквивалентности программ и трудности ее решения. Моделирование программ схемами программ. Стандартные схемы программ: синтаксис и семантика. Вычисления стандартных схем программ. Задачи анализа поведения стандартных схем программ - проблемы пустоты, тотальности, эквивалентности, свободы схем программ.
+
[[Media: MMSC_VP_06.pdf| Блок 6.]] Проблемы достижимости и живости для сетей Петри.
  
−
'''[[Media: Lecture_PM_6.pdf| Лекция 6.]]''' Описание стандартных схем программ при помощи систем переходов и алгебры подстановок. Эрбрановские интерпретации для стандартных схем программ. Эквивалентность стандартных схем программ на эрбрановских интерпретациях. Неразрешимость проблем анализа поведения стандартных схем программ. Схемы программ Ляпунова-Янова. Взаимосвязь схем программ Ляпунова-Янова и конечных автоматов. Разрешимость проблемы эквивалентности для схем Ляпунова-Янова.
+
[[Media: MMSC_VP_07.pdf| Блок 7.]] Диофантовы уравнения.
  
−
'''[[Media: Lecture_PM_7.pdf| Лекция 7.]]''' Логико-термальная эквивалентность стандартных схем программ. Аппроксимируемость функциональной эквивалентности программ логико-термальной эквивалентностью схем программ. Граф совместных вычислений стандартных схем программ. Операция антиунификации подстановок и ее свойства. Алгоритм вычисления наиболее специального шаблона двух подстановок. Алгоритм разметки графа совместных вычислений. Разрешимость проблемы логико-термальной эквивалентности стандартных схем программ.
+
[[Media: MMSC_VP_08.pdf| Блок 8.]] Моделирование многочленов сетями Петри.
  
−
8. Алгебраические модели систем взаимодействующих процессов. Алгебра процессов: синтаксис. Алгебра процессов: операционная семантика. Процессные графы и темпоральные логики. Отношение бисимуляции. Рекурсия. Абстракция и ветвящаяся бисимуляция. Применение алгебры процессов в задачах верификации распределенных систем.
+
[[Media: MMSC_VP_09.pdf| Блок 9.]] Проблемы R-включения и R-эквивалентности для сетей Петри.
  
−
9. Особенности мобильной связи. π-исчисление мобильных процессов. Синтаксис π-исчисления. Операционная семантика π-исчисления. Моделирование криптографических протоколов. spi-исчисление и его особенности. Применение spi-исчисления в криптоанализе.
+
[[Media: MMSC_VP_10.pdf| Блок 10.]] Языки сетей Петри.
  
−
== Программа курса == 
+
[[Media: MMSC_VP_11.pdf| Блок 11.]] Другие виды сетей Петри.
  
−
=== Сети Петри ===
+
[[Media: MMSC_VP_12.pdf| Блок 12.]] Проблема эквивалентности программ. Схемы программ.
 +
 
 +
[[Media: MMSC_VP_13.pdf| Блок 13.]] Схемы Ляпунова-Янова.
 +
 
 +
[[Media: MMSC_VP_14.pdf| Блок 14.]] Стандартные схемы программ.
 +
 
 +
[[Media: MMSC_VP_15.pdf| Блок 15.]] Подстановки. Системы переходов стандартных схем программ.
 +
 
 +
[[Media: MMSC_VP_16.pdf| Блок 16.]] Проблемы функциональной эквивалентности, пустоты и свободы для стандартных схем программ.
 +
 
 +
[[Media: MMSC_VP_17.pdf| Блок 17.]] Двухголовочные автоматы.
 +
 
 +
[[Media: MMSC_VP_18.pdf| Блок 18.]] Эрбрановские интерпретации для стандартных схем программ.
 +
 
 +
[[Media: MMSC_VP_19.pdf| Блок 19.]] Неразрешимость основных проблем для стандартных схем программ
 +
 
 +
[[Media: MMSC_VP_20.pdf| Блок 20.]] Алгебра процессов. Базовая алгебра процессов (BPA).
 +
 
 +
[[Media: MMSC_VP_21.pdf| Блок 21.]] Алгебра процессов с параллелизмом (PAP).
 +
 
 +
[[Media: MMSC_VP_22.pdf| Блок 22.]] Алгебра взаимодействующих процессов (ACP).
 +
 
 +
[[Media: MMSC_VP_23.pdf| Блок 23.]] Бисимуляция процессов.
 +
 
 +
[[Media: MMSC_VP_24.pdf| Блок 24.]] Консервативные расширения систем процессов.
 +
 
 +
[[Media: MMSC_VP_25.pdf| Блок 25.]] Рекурсия в системах процессов.
 +
 
 +
''Слайды будут появляться по мере проведения занятий''
 +
 
 +
== Прошлогодние слайды ==
 +
 
 +
[[Media: Lecture_PM_1.pdf| Лекция 1]].
 +
[[Media: Lecture_PM_2.pdf| Лекция 2]].
 +
[[Media: Lecture_PM_3.pdf| Лекция 3]].
 +
[[Media: Lecture_PM_4.pdf| Лекция 4]].
 +
[[Media: Lecture_PM_5.pdf| Лекция 5]].
 +
[[Media: Lecture_PM_6.pdf| Лекция 6]].
 +
[[Media: Lecture_PM_7.pdf| Лекция 7]].
 +
[[Media: Lecture_PM_8.pdf| Лекция 8]].
 +
[[Media: Lecture_PM_9.pdf| Лекция 9]].
 +
 
 +
= Программа курса =
 +
 
 +
== Сети Петри ==
 
<ol>
 
<ol>
 
<li> Сети позиций и переходов. Мультимножества и операции над ними. Разметки. Сети Петри.
 
<li> Сети позиций и переходов. Мультимножества и операции над ними. Разметки. Сети Петри.
Строка 39: Строка 83:
 
<li> Моделирование многочленов обыкновенными сетями Петри. Неразрешимость проблемы R-эквивалентности для обыкновенных сетей Петри.  
 
<li> Моделирование многочленов обыкновенными сетями Петри. Неразрешимость проблемы R-эквивалентности для обыкновенных сетей Петри.  
 
<li> Языки, порождаемые сетями Петри. Примеры языков, порождаемых сетями Петри. Сравнение класса языков, порождаемых обыкновенными сетями Петри, и классов языков иерархии Хомского.  
 
<li> Языки, порождаемые сетями Петри. Примеры языков, порождаемых сетями Петри. Сравнение класса языков, порождаемых обыкновенными сетями Петри, и классов языков иерархии Хомского.  
−
<li> Ординарные сети Петри. Моделирование обыкновенных сетей Петри ординарными сетями. <li> Автоматные сети Петри. Моделирование конечных автоматов автоматными сетями Петри.
+
<li> Ординарные сети Петри. Моделирование обыкновенных сетей Петри ординарными сетями.
 +
<li> Автоматные сети Петри. Моделирование конечных автоматов автоматными сетями Петри.
 
<li> Синхронизационные сети Петри. Условия живости и консервативности для синхронизационных сетей Петри.
 
<li> Синхронизационные сети Петри. Условия живости и консервативности для синхронизационных сетей Петри.
 
<li> Сети потоков работ.  
 
<li> Сети потоков работ.  
 
<li> Ингибиторные сети Петри. Моделирование счетчиковых машин Минского ингибиторными сетями Петри.  
 
<li> Ингибиторные сети Петри. Моделирование счетчиковых машин Минского ингибиторными сетями Петри.  
 
<li> Раскрашенные сети Петри.  
 
<li> Раскрашенные сети Петри.  
−
<li> Вложенные сети Петри
 
 
</ol>
 
</ol>
  
−
=== Схемы программ ===
+
== Схемы программ ==
−
<ol start="16">
+
<ol start="15">
 
<li> Проблема эквивалентности программ и трудности ее решения. Моделирование программ схемами программ.  
 
<li> Проблема эквивалентности программ и трудности ее решения. Моделирование программ схемами программ.  
 
<li> Стандартные схемы программ: синтаксис и семантика. Вычисления стандартных схем программ.  
 
<li> Стандартные схемы программ: синтаксис и семантика. Вычисления стандартных схем программ.  
−
<li> Задачи анализа поведения стандартных схем программ - проблемы пустоты, тотальности, эквивалентности, свободы схем программ.  
+
<li> Задачи анализа поведения стандартных схем программ - проблемы пустоты, эквивалентности, свободы схем программ.  
 
<li> Представление стандартных схем программ при помощи систем переходов и алгебры подстановок.  
 
<li> Представление стандартных схем программ при помощи систем переходов и алгебры подстановок.  
 
<li> Эрбрановские интерпретации для стандартных схем программ. Эквивалентность стандартных схем программ на эрбрановских интерпретациях.  
 
<li> Эрбрановские интерпретации для стандартных схем программ. Эквивалентность стандартных схем программ на эрбрановских интерпретациях.  
Строка 57: Строка 101:
 
<li> Схемы программ Ляпунова-Янова.  
 
<li> Схемы программ Ляпунова-Янова.  
 
<li> Взаимосвязь схем программ Ляпунова-Янова и конечных автоматов. Разрешимость проблемы эквивалентности для схем Ляпунова-Янова.  
 
<li> Взаимосвязь схем программ Ляпунова-Янова и конечных автоматов. Разрешимость проблемы эквивалентности для схем Ляпунова-Янова.  
−
<li> Логико-термальная эквивалентность стандартных схем программ. Аппроксимируемость функциональной эквивалентности программ логико-термальной эквивалентностью схем программ. <li> Граф совместных вычислений стандартных схем программ.
 
−
<li> Операция антиунификации подстановок и ее свойства. Алгоритм вычисления наиболее специального шаблона двух подстановок.
 
−
<li> Алгоритм разметки графа совместных вычислений. Разрешимость проблемы логико-термальной эквивалентности стандартных схем программ.
 
 
</ol>
 
</ol>
  
−
=== Алгебры процессов и &Pi;-исчисление ===
+
== Алгебра процессов ==
−
<ol start="28">
+
<ol start="23">
−
<li> Алгебра процессов: синтаксис и семантика.  
+
<li> Базовая алгебра процессов.
−
<li> Процессные графы и темпоральные логики. Отношение бисимуляции.
+
<li> Алгебра процессов с параллелизмом.
−
<li> Рекурсия. Абстракция и ветвящаяся бисимуляция.
+
<li> Алгебра взаимодействующих процессов.
−
<li> Применение алгебры процессов в задачах верификации распределенных систем
+
<li> Процессные графы.
−
<li> Особенности мобильной связи. &pi;-исчисление процессов. Операционная семантика &pi;-исчисления.
+
<li> Бисимуляция процессов.
−
<li> Криптографические протоколы. spi-исчисление: синтаксис и семантика. Применение spi-исчисления в криптоанализе.
+
<li> Консервативное расширение алгебры процессов.
 +
<li> Рекурсия в алгебре процессов.
 
</ol>
 
</ol>
  
−
=== Молекулярные модели вычислений ===
+
= Литература =
−
<ol start="32">
+
−
+
−
</ol>
+
−
 
+
−
=== Литература ===
+
  
 
<ol>
 
<ol>
−
<li> Котов В.Е. Сети Петри - М.: Мир, 1984. - 160 с.
+
<li> Котов В.Е. Сети Петри - М.: Мир, 1984.
−
<li> Питерсон Дж. Теория сетей Петри и моделирование систем. - М.: Мир, 1984.- 264 с.
+
<li> Питерсон Дж. Теория сетей Петри и моделирование систем. - М.: Мир, 1984.
−
<li> Ломазова И.А. Вложенные сети Петри: моделирование м анализ распределенных систем с объектной структурой - М.: Научный мир, 2004. - 207 с.
+
<li> Ломазова И.А. Вложенные сети Петри: моделирование м анализ распределенных систем с объектной структурой - М.: Научный мир, 2004.
−
<li> Reisig W. Understanding Petri Nets: Modeling Techniques, Analysis Methods, Case Studies. - Springer, 2013. - 211 p.
+
<li> Reisig W. Understanding Petri Nets: Modeling Techniques, Analysis Methods, Case Studies. - Springer, 2013.
−
<li> Котов В.Е., Сабельфельд В.К. Теория схем программ - М.: Мир, 1983. - 270 с.
+
<li> Котов В.Е., Сабельфельд В.К. Теория схем программ - М.: Мир, 1983.
 +
<li> Fokkink W. Introduction to process algebra. Springer Berlin, Heidelberg, 2000
 
</ol>
 
</ol>
−
 
−
== Правила проведения экзамена ==
 

Текущая версия на 23:08, 7 октября 2024


Обязательный курс для студентов групп 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. Бисимуляция процессов.

Блок 24. Консервативные расширения систем процессов.

Блок 25. Рекурсия в системах процессов.

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

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

Лекция 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. Раскрашенные сети Петри.

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

  1. Проблема эквивалентности программ и трудности ее решения. Моделирование программ схемами программ.
  2. Стандартные схемы программ: синтаксис и семантика. Вычисления стандартных схем программ.
  3. Задачи анализа поведения стандартных схем программ - проблемы пустоты, эквивалентности, свободы схем программ.
  4. Представление стандартных схем программ при помощи систем переходов и алгебры подстановок.
  5. Эрбрановские интерпретации для стандартных схем программ. Эквивалентность стандартных схем программ на эрбрановских интерпретациях.
  6. Неразрешимость проблем анализа поведения стандартных схем программ.
  7. Схемы программ Ляпунова-Янова.
  8. Взаимосвязь схем программ Ляпунова-Янова и конечных автоматов. Разрешимость проблемы эквивалентности для схем Ляпунова-Янова.

Алгебра процессов

  1. Базовая алгебра процессов.
  2. Алгебра процессов с параллелизмом.
  3. Алгебра взаимодействующих процессов.
  4. Процессные графы.
  5. Бисимуляция процессов.
  6. Консервативное расширение алгебры процессов.
  7. Рекурсия в алгебре процессов.

Литература

  1. Котов В.Е. Сети Петри - М.: Мир, 1984.
  2. Питерсон Дж. Теория сетей Петри и моделирование систем. - М.: Мир, 1984.
  3. Ломазова И.А. Вложенные сети Петри: моделирование м анализ распределенных систем с объектной структурой - М.: Научный мир, 2004.
  4. Reisig W. Understanding Petri Nets: Modeling Techniques, Analysis Methods, Case Studies. - Springer, 2013.
  5. Котов В.Е., Сабельфельд В.К. Теория схем программ - М.: Мир, 1983.
  6. Fokkink W. Introduction to process algebra. Springer Berlin, Heidelberg, 2000
Источник — «https://mk.cs.msu.ru/index.php?title=Математические_модели_последовательных_вычислений&oldid=11397»