Алгоритмические свойства формальных моделей параллельных и распределенных систем

• Автор: Кузьмин, Егор Владимирович
• Шифр специальности: 05.13.17
• Научная степень: Докторская
• Год защиты: 2011
• Место защиты: Переславль-Залесский
• Количество страниц: 312 с.

Содержание
Введение

Глава 1. Структурированные системы помеченных переходов

1.1. Мультимножество и квазипорядок

1.2. Структурированные системы помеченных переходов

1.2.1. Системы помеченных переходов

1.2.2. Структурированные системы помеченных переходов

1.2.3. Метод насыщения

1.2.4. Покрывающее дерево системы переходов

1.2.5. Совместимость по убыванию

Глава 2. Автоматные структурированные системы переходов

2.1. Определение
2.2. Семантические свойства
2.3. Темпоральные свойства
2.4. Заключение к главе
Глава 3. Взаимодействующие раскрашивающие процессы
3.1. Взаимодействующие процессы, независимые от данных
3.2. Взаимодействующие раскрашивающие процессы
3.3. Заключение к главе
Глава 4. Счетчиковые машины Минского
4.1. Счетчиковые машины Минского
4.2. Двухсчетчиковые машины
4.2.1. Неразрешимые проблемы
4.2.2. Проблема достижимости

4.2.3. Проблемы ограниченности
4.3. Однорегистровые машины
4.4. Односчетчиковые машины
4.4.1. Односчетчиковые машины
4.4.2. Свойства односчетчиковых машин
4.4.3. Алгоритм представления исполнения
4.4.4. Обоснование алгоритма и трудоемкость
4.4.5. Проблемы тотальности
4.5. Заключение к главе
Глава 5. Слабые счетчиковые машины
5.1. Счетчиковые машины с потерями
5.1.1. Отношения потери
5.1.2. Ограниченность для счетчиковых машин с потерями
5.1.3. Ограниченность для двухсчетчиковых машин
с обнулениями
5.2. Слабые счетчиковые машины
5.3. Заключение к главе
Глава 6. Автоматные счетчиковые машины
6.1. Автоматные счетчиковые машины
6.2. Проблема ограниченности
6.3. Проблемы включения и эквивалентности
6.4. Проблема достижимости
6.5. Автоматные счетчиковые машины малой размерности
6.5.1. Автоматная 3-счетчиковая машина с неполулинейным
множеством достижимости
6.5.2. Автоматные односчетчиковые машины

6.6. Автоматные счетчиковыс машины с ограничениями
6.7. Заключение к главе
Глава 7. Языки автоматных счетчиковых машин
7.1. Автоматная счетчиковая машина-распознаватель
7.2. Основные теоремы по проблемам пустоты
и распознавания слов
7.3. Свойства замкнутости
7.4. Проблемы включения и равенства языков
Глава 8. Моделирование, спецификация и верификация «автоматных» программ
8.1. Введение
8.2. Иерархическая модель автоматных программ
8.3. Автоматная модель системы управления кофеваркой
8.4. Спецификация и верификация автоматных моделей
8.5. Структура Крипке автоматной модели
8.6. Темпоральная логика LTL
8.7. Темпоральная логика CTL
8.8. Темпоральные свойства автоматных моделей
8.9. Редукция модели
8.10. Практическая реализация
8.11. Автоматные модели систем реального времени
8.12. Применение метода формальных утверждений о трассах
8.13. Заключение к главе
Заключение
Литература

Глава

Автоматные структурированные системы помеченных переходов
Ранее в первой главе были описаны два основных класса структурированных систем переходов: структурированные системы переходов с совместимостью по возрастанию и структурированные системы переходов с совместимостью по убыванию. Преимущественно существующие формализмы позволяют строить формальные модели, представляющие собой системы переходов одного из этих классов. Однако, исследователями совсем не уделяется внимание формализмам, модели в рамках которых удовлетворяли бы условию одновременной выполнимости свойств совместимости по возрастанию и совместимости по убыванию. Исходя из этого напрашивается вывод, что, возможно, допущение одновременного выполнения двух свойств совместимости по возрастанию и по убыванию отношения переходов с правильным квазипорядком на множестве состояний системы, приводит к вырожденной (весьма слабой по выразительной мощности) системе. В следующих главах будет показано, что это не так и такого рода формализмы могут быть весьма интересны, имея достаточную мощностью для построения осмысленных моделей прикладных систем. В частности, в третьей главе будет предложен нетривиальный формализм, порождающий вполне структурированные системы переходов с сильной совместимостью по возрастанию и убыванию, обладающий достаточной выразительной способностью, чтобы иметь прикладное значение.
В этой главе определяется новый класс структурированных систем переходов — вполне структурированные системы переходов автоматного типа. Доказывается, что этот класс систем переходов совпадает с классом вполне структурированных систем переходов, для которых свойство совместимости