Доставка любой диссертации в формате PDF и WORD за 499 руб. на e-mail - 20 мин. 800 000 наименований диссертаций и авторефератов. Все авторефераты диссертаций - БЕСПЛАТНО
Кузьмин, Егор Владимирович
01.01.09
Кандидатская
2004
Ярославль
149 с.
Стоимость:
499 руб.
1 Предварительные сведения
A(pU
где p € P - элементарное высказывание, определённое над множеством состояний системы переходов.
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 Конечный автомат для формулы
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
Отношение выполнимости 1= для состояния s системы переходов S = (S, Т, —>s, So) и формулы <р логики CTL индуктивно определяется следующим образом:
• s f= true и s false;
• s |= р для р Е Р 4=Ф- р Е L(s);
• s (= -><р -<=> s ^ (р;
• s [= <р А ф -Ф=Ф- s [= р и s = ф;
• s |= ? V ф -Ф=> 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
Название работы | Автор | Дата защиты |
---|---|---|
Некоторые задачи синтеза оптимального управления | Лизунова, Нина Александровна | 1985 |
Об условиях равномерности систем функций многозначной логики | Тарасов, Павел Борисович | 2016 |
Системы функциональных уравнений счетнозначной логики | Калинина, Инна Сергеевна | 2015 |