Лектор Герасимов Александр Сергеевич
Логика высказываний
Синтаксис логики высказываний.
Исчисление натуральных выводов для логики высказываний.
Правила, выводимые в исчислении натуральных выводов для логики высказываний.
Семантика логики высказываний.
Теорема о корректности исчисления натуральных выводов для логики высказываний.
Теорема о полноте исчисления натуральных выводов для логики высказываний.
Теорема о семантическом следствии для логики высказываний.
Построение КНФ по таблице истинности. Алгоритм проверки общезначимости КНФ. Связь выполнимости и общезначимости пропозициональных формул.
Алгоритм проверки выполнимости хорновских формул, теорема о его корректности.
Алгоритмы проверки выполнимости пропозициональных формул.
Логика предикатов
Язык первого порядка.
Свободные и связанные вхождения предметных переменных в предикатные формулы. Подстановки, свободные подстановки.
Исчисление натуральных выводов для логики предикатов.
Исчисление натуральных выводов с равенством.
Теорема о выводимо эквивалентных предикатных формулах.
Интерпретация языка первого порядка. Нормальная интерпретация. Истинностное значение формулы.
Примеры языков первого порядка и их интерпретаций.
Теорема о семантическом следствии для логики предикатов. Корректность и полнота исчисления натуральных выводов (с равенством) для логики предикатов. Некоторые неразрешимые проблемы для логики предикатов.
Верификация моделей
Синтаксис логики линейного времени LTL.
Семантика LTL.
Примеры LTL-формул, нахождение их истинностных значений.
Примеры LTL-спецификаций.
Эквивалентные LTL-формулы. Полные наборы темпоральных связок для LTL.
Две попытки моделирования взаимного исключения и верификации моделей.
Верификатор моделей NuSMV: простая программа, описываемая ею модель, верификация модели.
Верификатор моделей NuSMV: моделирование взаимного исключения и верификация модели.
Синтаксис логики деревьев вычислений CTL.
Семантика CTL.
Примеры CTL-формул, нахождение их истинностных значений.
Примеры CTL-спецификаций.
Эквивалентные CTL-формулы. Полные наборы темпоральных связок для CTL.
Обобщённая логика деревьев вычислений CTL*.
Сравнение выразительных возможностей CTL*, CTL и LTL.
Помечающий алгоритм верификации моделей для CTL.
Алгоритм верификации моделей для CTL: более эффективный алгоритм обработки EG.
Псевдокод алгоритма верификации моделей для CTL.
Монотонные функции. Неподвижные точки функций. Теорема о неподвижных точках монотонной функции.
Алгоритм верификации моделей для CTL: корректность алгоритма обработки EG.
Алгоритм верификации моделей для CTL: корректность алгоритма обработки EU.
Верификация моделей для CTL с ограничениями справедливости.
Алгоритм верификации моделей для LTL: базовая стратегия, пример.
Алгоритм верификации моделей для LTL: построение автомата, реализация заключительного этапа.
Двоичные разрешающие диаграммы и символьная верификация моделей
Булевы функции. Проблемы эффективности представлений булевых функций.
Двоичные разрешающие деревья. Двоичные разрешающие диаграммы (ДРД). Редукции ДРД.
Проверка выполнимости, общезначимости и выполнение булевых операций над булевыми функциями, представленными ДРД.
Упорядоченные двоичные разрешающие диаграммы (УДРД).
Алгоритм редукции УДРД.
Алгоритм применения булевой операции к УДРД.
Алгоритмы ограничения и квантификации УДРД.
Временная сложность построения УДРД.
Представление множеств состояний модели с помощью УДРД.
Представление отношения переходов модели с помощью УДРД. Построение УДРД, представляющей прообраз множества состояний при отношении переходов модели.
Синтез УДРД.