Алгебро-автоматні методи
проектування програмного забезпечення

Галузь знань: 12 Інформаційні технології
Спеціальність: 121 Інженерія програмного забезпечення
Освітня програма: Програмне забезпечення систем

Викладачі: Викладається: в 2-му семетрі магістратури.
Загальний обсяг: 144 год, з яких:
  • Лекції – 34 год.
  • Лабораторні роботи – 34 год.
  • Самостійна робота – 76 год.

Вимоги до знань та вмінь

Для вивчення курсу Алгебро-автоматні методи проектування програмного забезпечення студент повинен прослухати наступні курси:
  • дискретна математика,
  • алгебра та геометрія,
  • загальна алгебра,
  • теорія алгоритмів та математична логіка.
та повинен вміти:
  • виконувати аналіз проблеми, що виникає, побудову моделей відповідних систем,
  • створювати специфікації цих систем та виконувати верифікацію моделей, що виникли в результаті аналізу проблеми
  • розв'язувати задачі перевірки специфікацій на моделях.

Предмет дисципліни

Предмет навчальної дисципліни Алгебро-автоматні методи проектування програмного забезпечення включає в себе поглиблений розгляд методів теорії скінченних втоматів над скінченними словами, скінченних автоматів над нескінченними словами, часових автоматів, які широко застосовуються при побудові програмного забезпечення інформаційних систем. Зокрема, розглядаються способи моделювання скінченними автоматами різного роду дискретних систем та методи верифікації цих моделей шляхом використання властивостей мов, які акцептуються скінченними автоматами.

Мета та завдання дисципліни

Мета та завдання дисципліни – опанування методами розробки інформаційних систем на основі методів програмування з обмеженнями та їх застосування до розробки, аналізу і верифікації алгоритмів та програм.
В результаті вивчення навчальної дисципліни студент повинен
знати:
вміти:

Зв'язок з іншими дисциплінами.

Навчальна дисципліна Програмування з обмеженнями є базовою для вивчення таких спеціальних дисциплін як:

Програма курсу

Змістовий модуль 1: Задачі і проблематика теорії скінченних автоматів над словами скінченної довжини. Алгебра регулярних мов та її зв'язок з автоматами. Розв'язання основних задач теорії скінченних автоматів та застосування цієї теорії до моделювання систем.

Тема 1:
  • Предмет теорії автоматів та основні різно-видди скінченних автоматів над словами скінченної довжини.
  • Приклади.
  • Способи подання: автоматів: таблиці і графи перехо-дів і виходів.
Тема 2:
  • Еквівалентність скінченних автоматів, критерій еквівалентності.
  • Гомоморфізми та ізоморфізми скінченних автоматів Мілі, автоматів без виходів (акцепторів), теорема про існування мінімального автомата в класі автоматів еквівалентних даному.
Тема 3:
  • Основна теорема теорії скінченних автоматів: теореми синтезу та аналізу, алгоритми аналізу та синтезу скінченних автоматів.
Тема 4:
  • Практичні алгоритми аналізу та синтезу скінченних автоматів.
  • Приклади використання алгоритмів синтезу та аналізу.
Тема 5:
  • Задачі пошуку та обробки текстової інфор-мації на основі автоматів без виходів.
  • Ідентифікація слів.
  • Алгоритми Кнута-Моріса-Прата та Ахо-Ульмана.
Тема 6:
  • Розв'язання задач теорії скінченно породжуваних напівтруп: розпізнавання слів вілної напівтрупи, розв'язання задачі про перетин скінченно породжуваних напівтруп.
Тема 7:
  • Розв'язання задач теорії скінченно породжуваних груп.
  • Алгоритмічні проблеми теорії скінченно породжуваних груп.
  • Алгоритм побудови нільсенівського базиса.
  • Розв'язання задачі про перетин скінчено породжуваних підгруп вільної групи.
Тема 8:
  • Застосування в криптографії та іграх зі скінченним числом станів.
  • Застосування при моделюванні протоколів та їх верифікації.
Модульна контрольна робота 1

Змістовий модуль 2: Задачі і проблематика теорії скінченних автоматів над словами нескінченної довжини. Алгебра w-регулярних мов та її зв'язок з автоматами Б'юхі та Мюллера. Розв'язання основних задач теорії скінченних автоматів над словами нескінченної довжини та задач теорії часових автоматів.

Тема 9:
  • Скінченні автомати над нескінченними словами.
  • Автомати Б'юхі та автомати М'юлера.
  • Мови, які сприймаються автоматами Б'юхі та М'юлера.
Тема 10:
  • Детерміновані та не детерміновані автомати Б'юхі та Мюлера.
  • Основні властивості скінченних автоматів над словами нескін-ченної довжини: розв'язання задач про об'єднання, перетин та доповнення мов, які сприймаються автоматами Б'юхі та М'юлера. Приклади.
Тема 11:
  • Зв'язок автоматів з логікою.
  • Лінійна темпоральна логіка, аксіоматика та правила виведення.
Тема 12:
  • Основні властивості мови цієї логіки, метод семантичного табло.
  • Приклади застосування.
Тема 13:
  • Алгоритми трансляції моделей Кріпке та ЛТЛ-формул в автомати w-автомати.
Тема 14:
  • Розв'язання основних задач верифікації реактивних систем, які задаються специфікаціями в лінійній темпоральній логіці.
  • Приклади верифікації властивостей.
Тема 15:
  • Часові автомати.
  • Означення часового автомата і мови, яка акцептується цими автоматами.
Тема 16:
  • Часові автомати Б'юхі і М'юллера.
  • Розв'язання основних задач для часових регулярних мов: об'єднання та перевірка пустоти мови, що акцептується даним автоматом.
Тема 17:
  • Застосування до моделювання реальних дискретних інформаційних систем (електронні пристрої, робототехніка).
Модульна контрольна робота 2

Рекомендована література

Основна:

  1. Кривий С.Л. Дискретна математика: вибрані питання. – Вид. дім «Києво-Могилянська акдемія». – 2007. – 570 с.
  2. Лекции по дискретной математике. / Капитонова Ю.В., Кривой С.Л., Летичевский А.А., Луцкий Г.М., Санкт-Петербург. – БХВ. – 2005. – 634 с.
  3. Глушков В.М. Синтез цифровых автоматов. М: Наука. – 1962. – 509 с.
  4. Глушков В.М., Цейтлин Г.Е, Ющенко Е. Л. Алгебра, язики, программирование. К.: Наукова думка, 1989. – 376 с.
  5. Hopcroft J.E., Motwani R., Ullman J.D. Introduction to Automata Theory, Languages and Computations (second edition). – Addison-Wesley. – 2001. – 521 с.
  6. Perrin D. Finite Automata. Handbook of Theoretical and Computer Science. Ed by van Leeuven. – Elsevier Science Pablisherrs B.V. – 1990. – pp. 1-57.
  7. Perrin D., Pin J-E. Infinite words: Automata, Semigroup, Logic and Games. Elsevier Academic Press. – 2004. – 538 p.
  8. Трахтенброт Б.А., Барздинь Я.М. Конечные автоматы (поведение и синтез). – М.: Наука. – 1970. – 400 с.
  9. Thomas W. Automata on Infinite Objects. – Handbook of Theoretical and Computer Science. Ed by van Leeuven. – Elsevier Science Pablisherrs B.V. – 1990. – pp. 135-194.
  10. Кривий С.Л. Конспект лекцій 2011-2012 рр.
  11. Clarke E., Grumberg O., Peled D. Верификация моделей програм: Model checking. – The MIT Press. – Cambridge, Massachusetts, London, England. – 2001. – 376 p.
  12. Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных систем. С-Пб.:БХВ-Петербург. – 2010. – 560 с.

Додаткова:

  1. Глушков В.М., Летичевский А.А., Годлевский А.Б. Методы синтеза дискретных моделей биологических систем. – К.: Вища школа. – 1983. – 262 с.
  2. Лупанов О.Б. О сравнении двух типов конечних источников. – В кн.. «Проблемы кибернетики». – М.:Физматгиз. – 1963. – вып. 2. – С. 321-326.
  3. Bryant R.E. Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams. – School of Computer Science, Carnegi Mellon University. – Pittsburg. – 1992 (june). – 34 p.
  4. Анисимов А.В. О групповых язиках. // Кибернетика. – 1971. – N 4. – c. 18-24.
  5. Гилл А. Введение в теорию конечных автоматов. – М.: Наука. – 1966ю – 272 с.
  6. Мозговой М.В. Алгоритмы, языки, автоматы, компиляторы (практический поход). – С.-Пб. – Наука и техника. – 2006. – 320 с.