Введение
1 Предварительные сведения 15
1.1 Мультимножества 15
1.2 Квазиупорядоченные множества 16
1.2.1 Свойство вполне упорядочиваемое 17
1.3 Системы помеченных переходов 22
1.3.1 Определение 22
1.3.2 Вполне структурированные системы переходов . 23
1.3.3 Покрывающее дерево системы переходов . 24
1.3.4 Метод насыщения 28
1.3.5 Системы переходов с совместимостью по убыванию 32
1.4 Счётчиковые машины 34
1.5 Темпоральные логики и проверка модели 44
1.5.1 Логики ветвящегося времени 48
1.5.2 Логики линейного времени 58
1.5.3 Сравнение логик 61
2 Темпоральные свойства вполне структурированных систем переходов 74
2.1 Системы переходов автоматного типа 74
2.1.1 Разрешимые темпоральные свойства 78
2.1.2 Неразрешимые темпоральные свойства 87
2.2 Вполне структурированные системы переходов 95
2.2.1 Разрешимые темпоральные свойства 95
2.2.2 Неразрешимые темпоральные свойства 97
2.3 Дерево логик 98
3 Взаимодействующие раскрашивающие процессы 100
3.1 Взаимодействующие процессы независимые от данных 103
3.2 Взаимодействующие раскрашивающие процессы 108
3.3 ССР - вполне структурированная система переходов 111
3.4 Пример 115
4 Недетерминированные счетчиковые машины 118
4.1 Введение 118
4.2 Недетерминированные счетчиковые машины 119
4.3 Проблема ограниченности 123
4.4 Проблемы включения и эквивалентности 127
4.4.1 Слабое вычисление 128
4.4.2 Проблема включения 130
4.4.3 Проблема эквивалентности 133
4.5 Проблема достижимости 134
Заключение 137
Литература 139
