Исследование свойств класса вполне структурированных систем переходов

• Автор: Кузьмин, Егор Владимирович
• Шифр специальности: 01.01.09
• Научная степень: Кандидатская
• Год защиты: 2004
• Место защиты: Ярославль
• Количество страниц: 149 с.

1 Предварительные сведения

1.1 Мультимножества

1.2 Квазиупорядоченные множества

1.2.1 Свойство вполне упорядочиваемости

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

1.3.1 Определение

1.3.2 Вполне структурированные системы переходов

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

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

1.3.5 Системы переходов с совместимостью по убыванию

1.4 Счётчиковые машины

1.5 Темпоральные логики и проверка модели
1.5.1 Логики ветвящегося времени
1.5.2 Логики линейного времени
1.5.3 Сравнение логик
2 Темпоральные свойства вполне структурированных систем переходов
2.1 Системы переходов автоматного типа
2.1.1 Разрешимые темпоральные свойства
2.1.2 Неразрешимые темпоральные свойства
2.2 Вполне структурированные системы
переходов
2.2.1 Разрешимые темпоральные свойства
2.2.2 Неразрешимые темпоральные свойства
2.3 Дерево логик
3 Взаимодействующие раскрашивающие процессы
3.1 Взаимодействующие процессы
независимые от данных
3.2 Взаимодействующие раскрашивающие
процессы
3.3 ССР - вполне структурированная
система переходов
3.4 Пример
4 Недетерминированные счётчиковые машины
4.1 Введение
4.2 Недетерминированные счётчиковые машины
4.3 Проблема ограниченности
4.4 Проблемы включения и эквивалентности
4.4.1 Слабое вычисление
4.4.2 Проблема включения
4.4.3 Проблема эквивалентности
4.5 Проблема достижимости
Заключение
Литература

Список иллюстраций
1.1 Автомат Бюхи для формулы <р U ф • (А) V ijj2 - (£2)
состояния автомата финальные (замкнутый w-автомат)
1.2 Конечный автомат для формулы 2.1 Конечный автомат Af с алфавитом Е = Ех U Е2, где Ei = {(Pj,incj), (pf,decj), (pj,nulj); j'=l,2}, E2 ={(pj,^aZt/),
cpj,haltj), (pr,halt$y,j=1,2}
2.2 Автомат Бюхи A^c с алфавитом E ={(pj,incj), (pj , decj),
(pj,nulj) j=l, 2}
2.3 Автомат Бюхи Аш с алфавитом Е = {(true, incj), (pj~, decj),
(true,nulj); j=l,... ,m}
2.4 Граница разрешимости логики CTLA для класса вполне
структурированных систем переходов автоматного типа
2.5 Граница разрешимости логики LTLA для класса вполне
структурированных систем переходов автоматного типа
2.6 Граница разрешимости логики CTLA для класса вполне
структурированных систем переходов
2.7 Граница разрешимости логики LTLA для класса вполне
структурированных систем переходов
3.1 Схема взаимодействия компонентов А и Л2

“releases”), и интерпретируется над системами с тотальным отношением переходов. Формулы логики CTL строятся по следующей грамматике:
р ::= true | р | -I ip

A(pU где p € P - элементарное высказывание, определённое над множеством состояний системы переходов.
Отношение выполнимости 1= для состояния s системы переходов S = (S, Т, —>s, So) и формулы <р логики CTL индуктивно определяется следующим образом:
• s f= true и s false;
• s |= р для р Е Р 4=Ф- р Е L(s);
• s (= -><р -<=> s ^ (р;
• s [= <р А ф -Ф=Ф- s [= р и s = ф;
• s |= s 1= (р или s (= ф;
• s |= {)р 3s's —> s' и s' = (р;
• S [= [ }tp -4=^- Vs's —> s' следует s' |= р
• s (= А(р11ф) для каждого пути 7Г, выходящего из состояния s = 7г(0), существует такое j > О, ЧТО 7r(j) (= ф и при этом для всех г, 0 < г < j, ж (г) = р
• S = Е(р11ф) 4=Ф- ДЛЯ некоторого пути 7Г, выходящего из состояния s = 7Г(0) существует такое j > 0, что 7r(j) |= ф и при этом для всех
i,0