О проблеме эквивалентности для нисходящих детерминированных древесных автоматов

Поступила: 18.04.2025

Принята к публикации: 04.05.2025

Ключевые слова: древесный автомат, древесный язык, проблема эквивалентности, языковое уравнение

DOI: 10.55959/MSU/0137–0782–15–2025–49–4–38–45

Для цитирования статьи

Захаров В.А., Чжибо Дэн О проблеме эквивалентности для нисходящих детерминированных древесных автоматов // Вестник Московского университета. Серия 15. Вычислительная математика и кибернетика. 2025. № 4. С. 38-45 https://doi.org/10.55959/MSU/0137–0782–15–2025–49–4–38–45.

Это произведение доступно по лицензии Creative Commons «Attribution-NonCommercial» («Атрибуция-Некоммерчески») 4.0 Всемирная

Захаров В.А. (Университет МГУ-ППИ в Шэньчжэне)
Чжибо Дэн (Университет МГУ-ППИ в Шэньчжэне)

Аннотация

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

Литература

C o m o n H., D a u c h e t M., G i l l e r o n R., J a c q u e m a r d F., L u g i e z D., L ö d i n g C., T i s o n S., To m m a s i M. Tree automata techniques and applications (Электронный ресурс). URL: https://jacquema.gitlabpages.inria.fr/files/tata.pdf
E n g e l f r i e t J. Tree automata and tree grammars // arXiv preprint arXiv:1510.02036. 2015.
H o s o y a H. Foundations of XML Processing: The Tree-Automata Approach. Cambridge University Press, 2010.
K o l l e r A., K u h l m a n n M. A generalized view on parsing and translation // Proc. Int. Conf. on Parsing Technologies. Dublin, Ireland: Association for Computational Linguistics, 2011. P. 2–13.
H a b e r m e h l P., I o s i f R., Vo j n a r T. Automata-based verification of programs with tree updates // Acta Informatica. 2010. 47. N 1. P. 1–31.
C h e n Y.-F., C h u n g K.-M., L e n g б l O., L i n J.-A., Ts a i W.-L., Ye n D.-D. An automatabased framework for verification and bug hunting in quantum circuits // Proc. ACM on Programming Languages. 2023. 7. Issue PLDI. P. 1218–1243.
S e i d l H. Deciding equivalence of finite tree automata // SIAM Journal on Computing. 1990. 19. N 3. P. 424–437.
E l M a n s s o u r R. A., C h e v a l V., S h i r m o h a m m a d i M., Wo r r e l l J. On Tree Automata, Generating Functions, and Differential Equations // arXiv e-prints. 2024. P. arXiv:2407.
F ü l ö p Z., V a g v ö l g y i S. Minimization of deterministic top-down tree automata // Acta Cybernetica. 2017. 23. N 1. P. 379–401.
B r a i n e r d W. S. The minimalization of tree automata // Information and Control. 1968. 13. N 5. P. 484–491.
F u C., D e n g Y., J a n s e n D. N., Z h a n g L. On equivalence checking of nondeterministic finite automata // Proc. Int. Symp. SETTA. 2017. P. 216–231.
Z a k h a r o v V. A. Equivalence checking of prefix-free transducers and deterministic two-tape automata // Proc. Int. Conf. Language and Automata Theory and Applications (LATA). Lecture Notes in Computer Science. Vol. 11417. Springer, 2019. P. 146–158.
Z a k h a r o v V. A. Efficient equivalence checking technique for some classes of finite-state machines // Automatic Control and Computer Sciences. 2021. 55. N 7. P. 670–701.
B e n - A m r a m A. M., G a l i l Z. On pointers versus addresses // Journal of the ACM. 1992. 39. N 3. P. 617–648.