Введение
1 Гибридное направление исследования непрерывно-дискретных систем 15
1.1 Дискретный темпоральный подход 15
1.2 Математические модели дискретного темпорального подхода 18
1.3 Классификация и спецификация свойств поведения в дискретном темпоральном подходе, темпоральная логика 32
1.4 Метод символьной верификации и система HyTech . 40
1.5 Два примера символьной верификации 51
1.6 Условия сходимости метода символьной верификации . 60
1.7 Алгоритмы линейной аппроксимации гибридных автоматов 64
1.7.1 Таймер-преобразование 64
1.7.2 Алгоритм 6-аппроксимации по производной . 67
1.7.3 Пример: термостат 69
1.7.4 Недостатки алгоритмов линейной аппроксимации 74
2 Алгоритм обобщенного таймер-преобразования для гибридных систем с линейными системами ОДУ с по стоянными коэффициентами 77
2.1 Гибридный автомат с линейными системами ОДУ . 77
2.2 Обобщенное таймер-преобразование 80
2.2.1 Схема алгоритма 81
2.2.2 Описание алгоритма 82
2.3 Теоремы об алгоритме обобщенного таймер-преобразования 91
2.4 Метод покоординатных оценок. Функция "Cauchy" . 98
2.4.1 Постановка задачи и обоснование решения . 98
2.4.2 Описание метода покоординатных оценок . 100
2.4.3 Функция "extrems" для метода покоординатных оценок 104
2.4.4 Теорема о точности метода покоординатных оценок 112
2.4.5 Замечание о методе покоординатных оценок . 114
2.5 Метод оценки временного интервала. Функция "Cauchyl" 115
2.5.1 Постановка задачи и описание метода 115
2.5.2 Теорема о точности метода оценки временного интервала 126
Заключение 128
Список литературы 131
Приложение


