Цель данного мини-курса – дать первое представление о двух больших разделах теории вычислений с бесконечными данными. Оба раздела активно развиваются, имеют богатую теорию и опыт практической реализации. Первый раздел изучает поведение автоматов на бесконечных словах и является теоретической основой для верификации систем, в которых нужно математически гарантировать, что система способна достигнуть выделенное состояние бесконечное/потенциально неограниченное число раз. К примеру, алгоритм работы светофоров на перекрестке должен гарантировать возможность неограниченное число раз перейти в состояние «зеленый» для пешеходов, для лифта должна быть гарантирована возможность неограниченное число раз переместиться на тот или иной этаж. Второй раздел, известный как вычислимый анализ, изучает вычисления на действительных числах и других объектах математического анализа (которые являются бесконечными) и задуман как теоретическое обоснование надежных численных методов. При изучении языков программирования, включающих типы данных integer и real, складывается впечатление, что работа с этими разными типами совершенно аналогична. Однако на самом деле надежные численные методы (гарантирующие вычисление выходных данных с любой наперед заданной точностью) основаны на тонких идеях теории вычислений, восходящих к Тьюрингу.

Мини-курс состоит из четырех лекций со следующими названиями:

1. Конечные автоматы на бесконечных словах.

2. Автоматы и логика.

3. Автоматы и бесконечные игры.

4. Представление о вычислимом анализе.

Время проведения лекций указано московское (GMT+3)