Захаров В.А.

Задача унификации параметризованных автоматов-преобразователей состоит в том, чтобы для двух заданных автоматов найти такие значения их параметров, при которых эти автоматы будут вычислять одинаковые отношения трансдукции. В статье представлен квадратичный по времени алгоритм вычисления наиболее общих унификаторов конечных параметризованных детерминированных автоматов-преобразователей. Этот алгоритм построен на основе алгоритма Мартелли–Монтанари унификации термов и алгоритма проверки эквивалентности детерминированных автоматов-преобразователей.

Мы представляем эффективный алгоритм для проверки эквивалентности состояний детерминированных конечных нисходящих (top-down) древесных автоматов (DFTAs). В отличие от строковых автоматов, древесные автоматы работают с иерархическими структурами, и это обстоятельство осложняет алгоритмические задачи. Наш подход сводит проблему проверки эквивалентности к проверке разрешимости систем уравнений, которые определяют поведение DFTA. Эта проверка осуществляется при помощи правил равносильных преобразований, которые либо обнаруживают неразрешимость или несовместность уравнений, либо приводят систему к такому виду, который гарантирует существование решения. Доказаны корректность и завершение алгоритма и установлена верхняя оценка O(n²) времени его выполнения в модели вычислений RAM (Random Access Machine) с указателями.