О проблеме выполнимости логико-автоматных формул

Актуальность и цели. В теории конечных автоматов существует целый ряд способов определения конечных автоматов (конечно-автоматных функций). Среди них системы канонических уравнений, диаграммы Мура, информационные деревья, схемы из автоматных элементов, а также конечно-автоматные операции. Каждый из перечисленных способов обладает определенными достоинствами и находит применение в подходящих направлениях исследований. Довольно часто конечные автоматы используются в алгебре и логике. Так, например, хорошо известны результаты Дж. Бюхи о связи конечных автоматов с логикой второго порядка, а также результаты С. В. Алёшина по использованию групп конечно-автоматных перестановок в решении ослабленной проблемы Бернсайда. Одно из перспективных направлений в теории конечных автоматов - исследование автоматных уравнений различных типов. Помимо хорошо известных канонических уравнений, здесь могут быть функциональные уравнения, в которых переменными являются конечные автоматы, а связи между ними осуществляются с помощью алгебраических и логических средств. Самым естественным вариантом представляется вариант, когда на основе заданных автоматов и функциональных переменных для (многовходовых) автоматов определяются автоматные термы, затем - равенства термов (элементарные формулы) и в заключение из элементарных формул с помощью логических связок - произвольные логико-автоматные формулы. Для таких формул ставится «классическая» проблема выполнимости. Особенность ее состоит в том, что рассматривается существование конечных автоматов, выполняющих данную формулу, т.е. дающих истинное значение формулы при любых значениях предметных переменных (их значениями являются произвольные сверхслова в алфавите {0,1}). Цель работы - доказать алгоритмическую разрешимость данной проблемы, при этом определить разрешающий алгоритм в автоматных терминах и в конечном счете свести задачу к направленному перебору (возможно, частичных и недетерминированных) автоматов.
Материалы и методы. В построениях и доказательствах применяются логико-автоматные методы.
Результаты и выводы. Рассматриваются логико-автоматные формулы, построенные с помощью логических связок из равенств автоматных термов. Для формул данного типа формулируется проблема выполнимости по функциональным (автоматным) переменным. При этом предполагается, что все предметные переменные (по двоичным сверхсловам) находятся под кванторами общности. Строится алгоритм, основанный на переборе частичных недетерминированных автоматов, который решает данную проблему. Предложенный в работе подход к анализу и решению проблемы выполнимости для конечно-автоматных логических формул может быть использован при решении аналогичных алгоритмических проблем для логико-автоматных формул более сложных типов.