Программа OSW для вычисления оптимального синхронизирующего слова для частичного детерминированного автомата.

Abstract

Программа направлена на поиск оптимального синхронизирующего слова для синхронизируемого частичного детерминированного автомата. Она проводит экспериментальное исследование до достижения оптимальности. В программе три подпрограммы, которые выполняются последовательно. Первая отвечает за случайную генерацию частичных детерминированных автоматов и представляет операцию автомата в виде вектора, а затем отправляет это вектор во вторую подпрограмму. Основной задачей второй подпрограммы является кодирование задачи проверки возможности синхронизации полученного автомата словом заданной длины в задачу выполнимости в формате DIMACS. После этого данные передаются в SAT-решатель. SAT-решатель дает положительный результат в том и только в том случае, если у автомата есть синхронизирующее слово заданной длины. Выходные данные решателя отправляются в последнюю подпрограмму, которая отвечает за накопление и последующую обработку результатов эксперимента. Тип реализующей ЭВМ: IBM PC-совмест. ПК; ОС: Windows, Unix, Linux и др.