Алгебраические и логические методы в компьютерных науках

Последнее изменение: 07/05/2015 20:00:00

Обязательный курс для 1-го курса магистратуры-КН. Рекомендуется как специальный курс для 1-го курса магистратуры-МТ и для студентов старших курсов бакалавриата. В весеннем семестре 2011/12 учебного года читается по четвергам с 14:30 в ауд. 622.

Литература для дополнительного чтения

  • Jean-Éric Pin. Varieties of formal languages. North Oxford, London & Plenum, New-York, 1986.
  • Howard Straubing. Finite automata, formal logic, and circuit complexity. Birkhäuser Boston Inc., Boston, MA, 1994.

Краткое содержание курса

  • Алгебраическая теория формальных языков
    • Теоремы Щютценберже и Саймона
    • Теория Эйленберга и ее современные обобщения
  • Логическая теория формальных языков
    • Монадическая логика второго порядка. Результаты Бюхи
    • Теорема Макнотона
    • Соответствие между логическими и алгебраическими иерархиями
  • Линейная темпоральная логика
  • Верификация программных систем

Конспект лекций осеннего семестра

Лекция 1: Постановка задачи. Отношения Грина

Лекция 2: Строение D-классов. Лемма Грина

Лекция 3: Регулярные D-классы. D-строение моноида преобразований

Лекция 4: Алгоритм вычисления регулярных D-классов в полугруппах преобразований

Вопросы к зачету по итогам осеннего семестра

  1. Отношения Грина и их основные свойства. Лемма Грина
  2. Идемпотенты. Существование идемпотентов в конечных полугруппах. Совпадение отношений D и J в конечных полугруппах.
  3. Теорема Миллера-Клиффорда. Регулярные D-классы.
  4. D-строение моноида преобразований
  5. Алгоритм вычисления регулярных D-классов в полугруппах преобразований
  6. Рисовские полугруппы матричного типа. Теорема Риса-Сушкевича.
  7. Характеризация J-тривиальных, R-тривиальных и H-тривиальных полугрупп.
  8. Кусочно тестируемые языки. Отношение равноподсловности. Формулировка теоремы Саймона.
  9. Первые две леммы из доказательства теоремы Саймона.
  10. Доказательство достаточности условия теоремы Саймона (кусочно тестируемый язык распознается J-тривиальным моноидом).
  11. Основная комбинаторная лемма из доказательства теоремы Саймона.
  12. Доказательство необходимости теоремы Саймона (язык, распознаваемый J-тривиальным моноидом, кусочно тестируем).
  13. Беззвездные языки. Формулировка теоремы Щютценберже. Произведение Щютценберже.
  14. Доказательство достаточности условия теоремы Щютценберже (беззвездный язык распознается H-тривиальным моноидом).
  15. Доказательство необходимости теоремы Щютценберже (язык, распознаваемый H-тривиальным моноидом, беззвездный).

Вопросы к зачету по итогам весеннего семестра

  1. Логика первого порядка. Монадическая логика второго порядка. Задание языков формулами первого и второго порядка.
  2. Теорема Бюхи о логической характеризации регулярных языков. Доказательство необходимости условия теоремы Бюхи (язык, распознаваемый конечным автоматом, задается формулой монадической логики второго порядка).
  3. V-слова и (V_1,V_2)-слова. Интерпретация формул первого и второго порядка, содержащих свободные переменные. Доказательство достаточности условия теоремы Бюхи (язык, задаваемой формулой монадической теории второго порядка, распознается конечным автоматом).
  4. Регулярные предикаты. Примеры определимых и неопределимых предикатов. Характеризация предикатов, определимых в монадической логике второго порядка.
  5. Языки бесконечных слов. Распознаваемость языков бесконечных слов по Бюхи. Детерминированные и недетерминированные автоматы Бюхи.
  6. Теорема Бюхи для языков бесконечных слов. Доказательство необходимости условия теоремы Бюхи (язык, распознаваемый автоматом Бюхи, задается формулой монадической логики второго порядка).
  7. Характеризация языков бесконечных слов, распознаваемых автоматом Бюхи, через регулярные языки конечных слов.
  8. Теорема Рамсея. Замкнутость класса языков бесконечных слов, распознаваемых автоматом Бюхи, относительно дополнения. Доказательство достаточности условия теоремы Бюхи для языков бесконечных слов.
  9. Игры Эренфойхта-Фрессе.
  10. Игровое доказательство того, что язык слов четной длины не может быть задано формулой теории FO(<).
  11. Локально барьерно тестируемые языки. Пример языка, задаваемого формулой теории FO(<), но не задаваемого формулой теории FO(x=y+1).
  12. Теорема Макнотона.

Смотрите также: