Алгоритм проверки пустоты пересечения множества автоматов на основе линейной алгебры

Георгием Беляниным был разработан алгоритм, фактически, проверяющий пустоту пересечения двух автоматов, основанный на операциях над разреженными булевыми матрицами. Хотя исходный алгоритм рассматривался в контексте выполнения запросов к графовым базам данных, задача о проверки пустоты пересечения встречается, например, в автоматных решателях, с которыми можно познакомиться, например, в работе [An Automata-Based Decision Procedure for Presburger Arithmetic] (https://excel.fit.vutbr.cz/submissions/2022/016/16.pdf). Но в подобных задачах есть своя специфика. Например, требуется работать сразу с множеством автоматов, а не с двумя. Предлагается

  • Обобщить алгоритм, предложенный Георгием, с двух до произвольного количества автоматов
  • Провести эксперименты на данных, релевантных для автоматных решателей
  • Опубликовать реализованный алгоритм в составе библиотеки LAGraph
  • Интегрировать полученный алгоритм в один из существующих решателей
Требования к студенту
  • Отличное знание языка программирования C и соответствующего инструментария для сборки, отладки, тестирования.
  • Отличное знание основ теории графов: различные типы графов (ориентированные, неориентированные, с метками на рёбрах и т.д.), способов представления графов (матрица смежности, список смежности и т.д.), алгоритмы обхода графов (в ширину, глубину), алгоритмы решения задачи достижимости, поиска путей и т.д.
  • Отличное знание основ теории формальных языков: регулярные языки, конечные автоматы, алгоритмы работы с ними (пересечение регулярных языков, детерминизация конечных автоматов и т.д.).
  • Знание основ линейной алгебры: матрицы, вектора, операции над ними (умножение, поэлементные операции), кольца, полукольца, свойства операций (коммутативность, идемпотентность и т.д.).
  • Отличное знание основ математической логики: разрешимость формул (в теории), SAT, SMT (постановка задачи, идеи решения).
Уровень

2 курс, 3 курс, Бакалаврская ВКР

Руководитель

Григорьев Семен Вячеславович

Консультант

Grigorev Semyon

Источник

Кафедра системного программирования СПбГУ