Чжибо Дэн

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