maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2020-3-260-303mais-1349Research ArticleTheory of ComputingЭффективные алгоритмы проверки эквивалентности для некоторых классов автоматовEfficient Equivalence Checking Technique for Some Classes of Finite-State Machineshttps://orcid.org/0000-0002-3794-9565ЗахаровВладимир АнатольевичZakharovVladimir A.

Ул. Мясницкая, 20, Москва, 101000

Vladimir Anatolyevich Zakharov - Doctor of Science, Professor.

20 Myasnitskaya ulitsa, Moscow, 101000

 

Национальный исследовательский университет Высшая школа экономикиРоссияNational Research University Higher School of Economics (HSE)Russian Federation202020092020273260303Copyright © Захаров В.А., 20202020Захаров В.А.Zakharov V.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1349

Конечные преобразователи, двухленточные автоматы и биавтоматы — взаимосвязанные вычислительные модели, ведущие свое происхождение от концепции конечного автомата. В вычислениях этих машин проявляется много общих черт, и удивительно, что методы анализа, разработанные для одной из указанных моделей, не находят подходящего применения в других моделях. Целью данной статьи является разработка единой методики построения быстрых алгоритмов проверки эквивалентности для некоторых классов автоматов (конечных преобразователей, двухленточных автоматов, биавтоматов, магазинных автоматов), которые демонстрируют определенные черты детерминированного или однозначное поведение. Этот новый метод сводит проверку эквивалентности автоматов к проверке разрешимости систем уравнений над полукольцами языков или бинарных отношений. Как оказалось, такую проверку достаточно просто провести методом исключения переменных, используя некоторые комбинаторные и алгебраические свойства регулярных префиксных языков. Основные результаты, полученные в этой статье, таковы.

1

1.            При помощи алгебраического метода построен новый алгоритм проверки эквивалентности детерминированных конечных автоматов, имеющий сложность по времени O(n log n).

2

2.            Выделен новый класс префиксных конечных трансдьюсеров и показано, что проверка эквивалентности трансдьюсеров из этого класса может быть осуществлена новым методом за время, квадратичное (для префиксных трансдьюсеров реального времени) и кубическое (для префиксных трансдьюсеров с ɛ-переходами) относительно размеров анализируемых автоматов.

3

3.            Показано, что проблема эквивалентности для детерминированных двухленточных конечных автоматов сводится к задаче проверки эквивалентности префиксных конечных трансдьюсеров и может быть решена за время, кубическое относительно их размеров.

4

4.            Аналогичным образом установлена разрешимость проблемы эквивалентности для детерминированных конечных биавтоматов за время, кубическое относительно их размеров.

5

5.            При помощи нового метода построен алгоритм проверки эквивалентности для простых грамматик, соответствующих детерминированным магазинным автоматам с одним состоянием.

Finite transducers, two-tape automata, and biautomata are related computational models descended from the concept of Finite-State Automaton. In these models an automaton controls two heads that read or write symbols on the tapes in the one-way mode. The computations of these three types of automata show many common features, and it is surprising that the methods for analyzing the behavior of automata developed for one of these models do not find suitable utilization in other models. The goal of this paper is to develop a uniform technique for building polynomial-time equivalence checking algorithms for some classes of automata (finite transducers, two-tape automata, biautomata, single-state pushdown automata) which exhibit certain features of the deterministic or unambiguous behavior. This new technique reduces the equivalence checking of automata to solvability checking of certain systems of equations over the semirings of languages or transductions. It turns out that such a checking can be performed by the variable elimination technique which relies on some combinatorial and algebraic properties of prefix-free regular languages. The main results obtained in this paper are as follows:

1

1.            Using the algebraic approach a new algorithm for checking the equivalence of states of deterministic finite automata is constructed; time complexity of this algorithm is O(n log n).

2

2.            A new class of prefix-free finite transducers is distinguished and it is shown that the developed algebraic approach provides the equivalence checking of transducers from this class in quadratic time (for real-time prefix-free transducers) and cubic (for prefix-free transducers with ɛ-transitions) relative to the sizes of analysed machines.

3

3.            It is shown that the equivalence problem for deterministic two-tape finite automata can be reduced to the same problem for prefix-free finite transducers and solved in cubic time relative to the size of the analysed machines.

4

4.            In the same way it is proved that the equivalence problem for deterministic finite biautomata can be solved in cubic time relative to the sizes of analysed machines.

5

5.            By means of the developed approach an efficient equivalence checking algorithm for the class of simple grammars corresponding to deterministic single-state pushdown automata is constructed.

трансдьюсердвухленточный автоматбиавтоматпростая грамматикапроверка эквивалентностипрефиксный языкязыковое уравнениеразрешающая процедураtransducertwo-tape automatonbiatomatonsimple grammarequivalence checkingprefix-free languagelanguage equationdecision procedureРабота выполнена при финансовой поддержке гранта РФФИ N 18-01-00854This work was supported by the Russian Foundation for Basic Research, Grant N 18-01-00854ReferencesA. L. Rosenberg, "A machine realization of the linear context-free languages”, Information and Control, vol. 10, no. 2, pp. 175-188, 1967.A. L. Rosenberg, "A machine realization of the linear context-free languages”, Information and Control, vol. 10, no. 2, pp. 175-188, 1967.M. Mohri, "Finite-state transducers in language and speech processing”, Computational linguistics, vol. 23, no. 2, pp. 269-311, 1997.M. Mohri, "Finite-state transducers in language and speech processing”, Computational linguistics, vol. 23, no. 2, pp. 269-311, 1997.A. Roche-Lima and R. K. Thulasiram, "Bioinformatics algorithm based on a parallel implementation of a machine learning approach using transducers”, Journal of Physics: Conference Series, vol. 341, no. 1, p. 012 034, 2012.A. Roche-Lima and R. K. Thulasiram, "Bioinformatics algorithm based on a parallel implementation of a machine learning approach using transducers”, Journal of Physics: Conference Series, vol. 341, no. 1, p. 012 034, 2012.R. Alur and P. Cerny, "Streaming transducers for algorithmic verification of single-pass list-processing programs”, in Proceedings of 38-th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 2011, pp. 599-610.R. Alur and P. Cerny, "Streaming transducers for algorithmic verification of single-pass list-processing programs”, in Proceedings of 38-th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 2011, pp. 599-610.J. Thakkar and R. Kanade A.and Alur, "Transducer-based algorithmic verification of retransmission protocols over noisy channels”, in Proceedings of IFIP Joint International Conference on Formal Techniques for Distributed Systems, Springer, 2013, pp. 209-224.J. Thakkar and R. Kanade A.and Alur, "Transducer-based algorithmic verification of retransmission protocols over noisy channels”, in Proceedings of IFIP Joint International Conference on Formal Techniques for Distributed Systems, Springer, 2013, pp. 209-224.M. Veanes, P. Hooimeijer, B. Livshits, and et al., "Symbolic finite state transducers: Algorithms and applications”, in Proceedings of the 39-th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 2012, pp. 137-150.M. Veanes, P. Hooimeijer, B. Livshits, and et al., "Symbolic finite state transducers: Algorithms and applications”, in Proceedings of the 39-th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 2012, pp. 137-150.D. G. Kozlova and V. A. Zakharov, "On the model checking of sequential reactive systems”, in Proceedings of the 25-th International Workshop on Concurrency, Specification and Programming, Rostock, Germany, September 28-30, vol. 1698, 2016, p. 233.D. G. Kozlova and V. A. Zakharov, "On the model checking of sequential reactive systems”, in Proceedings of the 25-th International Workshop on Concurrency, Specification and Programming, Rostock, Germany, September 28-30, vol. 1698, 2016, p. 233.M. Mohri, "Minimization algorithms for sequential transducers”, Theoretical Computer Science, vol. 234, no. 2, pp. 177-201, 2000.M. Mohri, "Minimization algorithms for sequential transducers”, Theoretical Computer Science, vol. 234, no. 2, pp. 177-201, 2000.V. A. Zakharov and S. R. Jaylauova, "On the minimization problem for sequential programs”, Automatic Control and Computer Sciences, vol. 51, no. 7, pp. 689-700, 2017.V. A. Zakharov and S. R. Jaylauova, "On the minimization problem for sequential programs”, Automatic Control and Computer Sciences, vol. 51, no. 7, pp. 689-700, 2017.H. Tamm, M. Nykanen, and E. Ukkonen, "On size reduction techniques for multitape automata”, Theoretical computer science, vol. 363, no. 2, pp. 234-246, 2006.H. Tamm, M. Nykanen, and E. Ukkonen, "On size reduction techniques for multitape automata”, Theoretical computer science, vol. 363, no. 2, pp. 234-246, 2006.D. C. Luckham, D. M. Park, and M. S. Paterson, "On formalized computer programs”, Journal of Computer and System Sciences, vol. 4, no. 3, pp. 220-249, 1970.D. C. Luckham, D. M. Park, and M. S. Paterson, "On formalized computer programs”, Journal of Computer and System Sciences, vol. 4, no. 3, pp. 220-249, 1970.R. Loukanova, "Linear context free languages”, in International Colloquium on Theoretical Aspects of Computing, Springer, 2007, pp. 351-365.R. Loukanova, "Linear context free languages”, in International Colloquium on Theoretical Aspects of Computing, Springer, 2007, pp. 351-365.B. Bedregal, "λ-ALN: automatos lineares nao-deterministicos com λ-transicoes”, Tendencias em Matematica Aplicada e Computacional, vol. 12, no. 3, pp. 171-182, 2011.B. Bedregal, "λ-ALN: automatos lineares nao-deterministicos com λ-transicoes”, Tendencias em Matematica Aplicada e Computacional, vol. 12, no. 3, pp. 171-182, 2011.G. Jiraskova and O. Klima, "Deterministic Biautomata and Subclasses of Deterministic Linear Languages”, in International Conference on Language and Automata Theory and Applications, Springer, 2019, pp. 315-327.G. Jiraskova and O. Klima, "Deterministic Biautomata and Subclasses of Deterministic Linear Languages”, in International Conference on Language and Automata Theory and Applications, Springer, 2019, pp. 315-327.M. Holzer and S. Jakobi, "Nondeterministic biautomata and their descriptional complexity”, in International Workshop on Descriptional Complexity of Formal Systems, Springer, 2013, pp. 112-123.M. Holzer and S. Jakobi, "Nondeterministic biautomata and their descriptional complexity”, in International Workshop on Descriptional Complexity of Formal Systems, Springer, 2013, pp. 112-123.O. Klima and L. Polak, "On biautomata*”, RAIRO-Theoretical Informatics and Applications, vol. 46, no. 4, pp. 573-592, 2012.O. Klima and L. Polak, "On biautomata*”, RAIRO-Theoretical Informatics and Applications, vol. 46, no. 4, pp. 573-592, 2012.M. Holzer and S. Jakobi, "Minimization and characterizations for biautomata”, Fundamenta Informaticae, vol. 136, no. 1-2, pp. 113-137, 2015.M. Holzer and S. Jakobi, "Minimization and characterizations for biautomata”, Fundamenta Informaticae, vol. 136, no. 1-2, pp. 113-137, 2015.P. C. Fischer and A. L. Rosenberg, "Multitape one-way nonwriting automata”, Journal of Computer and System Sciences, vol. 2, no. 1, pp. 88-101,1968.P. C. Fischer and A. L. Rosenberg, "Multitape one-way nonwriting automata”, Journal of Computer and System Sciences, vol. 2, no. 1, pp. 88-101,1968.T. Griffiths, "The unsolvability of the equivalence problem for Λ-free nondeterministic generalized machines”, Journal of the ACM (JACM), vol. 15, no. 3, pp. 409-413, 1968.T. Griffiths, "The unsolvability of the equivalence problem for Λ-free nondeterministic generalized machines”, Journal of the ACM (JACM), vol. 15, no. 3, pp. 409-413, 1968.O. Ibarra, "The unsolvability of the equivalence problem for e-free NGSM’s with unary input (output) alphabet and applications”, SIAM Journal on Computing, vol. 7, no. 4, pp. 524-532, 1978.O. Ibarra, "The unsolvability of the equivalence problem for e-free NGSM’s with unary input (output) alphabet and applications”, SIAM Journal on Computing, vol. 7, no. 4, pp. 524-532, 1978.M. Blattner and T. Head, "Single-valued a-transducers”, Journal of Computer and System Sciences, vol. 15, no. 3, pp. 310-327, 1977.M. Blattner and T. Head, "Single-valued a-transducers”, Journal of Computer and System Sciences, vol. 15, no. 3, pp. 310-327, 1977.M. P. Schutzenberger, "Sur les relations rationnelles”, in Proceedings of the Conference on Automata Theory and Formal Languages, 1975, pp. 209-213.M. P. Schutzenberger, "Sur les relations rationnelles”, in Proceedings of the Conference on Automata Theory and Formal Languages, 1975, pp. 209-213.M. Blattner and T. Head, "The decidability of equivalence for deterministic finite transducers”, Journal of Computer and System Sciences, vol. 19, no. 1, pp. 45-49, 1979.M. Blattner and T. Head, "The decidability of equivalence for deterministic finite transducers”, Journal of Computer and System Sciences, vol. 19, no. 1, pp. 45-49, 1979.E. M. Gurari and O. Ibarra, "A note on finite-valued and finitely ambiguous transducers”, Mathematical systems theory, vol. 16, no. 1, pp. 61-66,1983.E. M. Gurari and O. Ibarra, "A note on finite-valued and finitely ambiguous transducers”, Mathematical systems theory, vol. 16, no. 1, pp. 61-66,1983.A. Weber, "On the valuedness of finite transducers”, Acta Informatica, vol. 27, no. 8, pp. 749-780,1990.A. Weber, "On the valuedness of finite transducers”, Acta Informatica, vol. 27, no. 8, pp. 749-780,1990.K. Culik and J. Karhumaki, "The equivalence of finite valued transducers (on HDT0L languages) is decidable”, Theoretical Computer Science, vol. 47, pp. 71-84,1986.K. Culik and J. Karhumaki, "The equivalence of finite valued transducers (on HDT0L languages) is decidable”, Theoretical Computer Science, vol. 47, pp. 71-84,1986.A. Weber, "A decomposition theorem for finite-valued transducers and an application to the equivalence problem”, in Proceedings of the 13-th International Symposium on Mathematical Foundations of Computer Science, Springer, 1988, pp. 552-562.A. Weber, "A decomposition theorem for finite-valued transducers and an application to the equivalence problem”, in Proceedings of the 13-th International Symposium on Mathematical Foundations of Computer Science, Springer, 1988, pp. 552-562.A. Weber, "Decomposing finite-valued transducers and deciding their equivalence”, SIAM Journal on Computing, vol. 22, no. 2, pp. 175-202, 1993.A. Weber, "Decomposing finite-valued transducers and deciding their equivalence”, SIAM Journal on Computing, vol. 22, no. 2, pp. 175-202, 1993.M.-P. Beal, O. Carton, C. Prieur, and J. Sakarovitch, "Squaring transducers: an efficient procedure for deciding functionality and sequentiality”, Theoretical Computer Science, vol. 292, no. 1, pp. 45-63, 2003.M.-P. Beal, O. Carton, C. Prieur, and J. Sakarovitch, "Squaring transducers: an efficient procedure for deciding functionality and sequentiality”, Theoretical Computer Science, vol. 292, no. 1, pp. 45-63, 2003.J. Sakarovitch and R. de Souza, "On the decomposition of Λ-valued rational relations”, in Proceedings of the 25-th International Symposium on Mathematical Foundations of Computer Science, 2008, pp. 588-600.J. Sakarovitch and R. de Souza, "On the decomposition of Λ-valued rational relations”, in Proceedings of the 25-th International Symposium on Mathematical Foundations of Computer Science, 2008, pp. 588-600.J. Sakarovitch and R. de Souza, "On the decidability of bounded valuedness for transducers”, in Proceedings of the 25-th International Symposium on Mathematical Foundations of Computer Science, 2008, pp. 588-600.J. Sakarovitch and R. de Souza, "On the decidability of bounded valuedness for transducers”, in Proceedings of the 25-th International Symposium on Mathematical Foundations of Computer Science, 2008, pp. 588-600.J. Sakarovitch and R. de Souza, "Lexicographic decomposition of ^-valued transducers”, Theory of Computing Systems, vol. 47, no. 3, pp. 758-785, 2010.J. Sakarovitch and R. de Souza, "Lexicographic decomposition of ^-valued transducers”, Theory of Computing Systems, vol. 47, no. 3, pp. 758-785, 2010.R. de Souza, "On the decidability of the equivalence for k-valued transducers”, in Proceedings of the 12-th International Conference on Developments in Language Theory, Springer, 2008, pp. 252-263.R. de Souza, "On the decidability of the equivalence for k-valued transducers”, in Proceedings of the 12-th International Conference on Developments in Language Theory, Springer, 2008, pp. 252-263.V. A. Zakharov, "Equivalence checking problem for finite state transducers over semigroups”, in Proceedings of the 6-th International Conference on Algebraic Informatics, Springer, 2015, pp. 208-221.V. A. Zakharov, "Equivalence checking problem for finite state transducers over semigroups”, in Proceedings of the 6-th International Conference on Algebraic Informatics, Springer, 2015, pp. 208-221.A. Weber, "On the lengths of values in a finite transducer”, Acta Informatica, vol. 29, no. 6-7, pp.663-687, 1992.A. Weber, "On the lengths of values in a finite transducer”, Acta Informatica, vol. 29, no. 6-7, pp.663-687, 1992.R. de Souza, "On the Decidability of the Equivalence for a Certain Class of Transducers”, in Proceedings of the 13-th International Conference on Developments in Language Theory, Springer, 2009, pp. 478-489.R. de Souza, "On the Decidability of the Equivalence for a Certain Class of Transducers”, in Proceedings of the 13-th International Conference on Developments in Language Theory, Springer, 2009, pp. 478-489.M. Bird, "The equivalence problem for deterministic two-tape automata”, Journal of Computer and System Sciences, vol. 7, no. 2, pp. 218-236, 1973.M. Bird, "The equivalence problem for deterministic two-tape automata”, Journal of Computer and System Sciences, vol. 7, no. 2, pp. 218-236, 1973.L. G. Valiant, "The equivalence problem for deterministic finite-turn pushdown automata”, Information and Control, vol. 25, no. 2, pp. 123-133, 1974.L. G. Valiant, "The equivalence problem for deterministic finite-turn pushdown automata”, Information and Control, vol. 25, no. 2, pp. 123-133, 1974.C. Beeri, "An improvement on Valiant’s decision procedure for equivalence of deterministic finite turn pushdown machines”, Theoretical Computer Science, vol. 3, no. 3, pp. 305-320,1976.C. Beeri, "An improvement on Valiant’s decision procedure for equivalence of deterministic finite turn pushdown machines”, Theoretical Computer Science, vol. 3, no. 3, pp. 305-320,1976.E. P. Friedman and S. A. Greibach, "A polynomial time algorithm for deciding the equivalence problem for 2-tape deterministic finite state acceptors”, SIAM Journal on Computing, vol. 11, no. 1, pp. 166-183, 1982.E. P. Friedman and S. A. Greibach, "A polynomial time algorithm for deciding the equivalence problem for 2-tape deterministic finite state acceptors”, SIAM Journal on Computing, vol. 11, no. 1, pp. 166-183, 1982.T. Harju and J. Karhumaki, "The equivalence problem of multitape finite automata”, Theoretical Computer Science, vol. 78, no. 2, pp. 347-355, 1991.T. Harju and J. Karhumaki, "The equivalence problem of multitape finite automata”, Theoretical Computer Science, vol. 78, no. 2, pp. 347-355, 1991.J. Worrell, "Revisiting the equivalence problem for finite multitape automata”, in Proceedings of the 40-th International Colloquium on Automata, Languages, and Programming, Springer, 2013, pp. 422-433.J. Worrell, "Revisiting the equivalence problem for finite multitape automata”, in Proceedings of the 40-th International Colloquium on Automata, Languages, and Programming, Springer, 2013, pp. 422-433.B. Bedregal, "Nondeterministic Linear Automata and a Class of Deterministic Linear Languages”, Preliminary Proceedings LSFA, pp. 183-196, 2015.B. Bedregal, "Nondeterministic Linear Automata and a Class of Deterministic Linear Languages”, Preliminary Proceedings LSFA, pp. 183-196, 2015.Y. Bar-Hillel, M. Perles, and E. Shamir, "On formal properties of simple phrase structure grammars”, Sprachtypologie und Universalienforschung, vol. 14, pp. 143-172, 1961.Y. Bar-Hillel, M. Perles, and E. Shamir, "On formal properties of simple phrase structure grammars”, Sprachtypologie und Universalienforschung, vol. 14, pp. 143-172, 1961.A. J. Korenjak and J. E. Hopcroft, "Simple deterministic languages”, in 7th Annual Symposium on Switching and Automata Theory (swat 1966), IEEE, 1966, pp. 36-46.A. J. Korenjak and J. E. Hopcroft, "Simple deterministic languages”, in 7th Annual Symposium on Switching and Automata Theory (swat 1966), IEEE, 1966, pp. 36-46.E. P. Friedman, "The inclusion problem for simple languages”, Theoretical Computer Science, vol. 1, no. 4, pp. 297-316, 1976.E. P. Friedman, "The inclusion problem for simple languages”, Theoretical Computer Science, vol. 1, no. 4, pp. 297-316, 1976.D. Caucal, "A fast algorithm to decide on simple grammars equivalence”, in International Symposium on Optimal Algorithms, Springer, 1989, pp. 66-85.D. Caucal, "A fast algorithm to decide on simple grammars equivalence”, in International Symposium on Optimal Algorithms, Springer, 1989, pp. 66-85.C. Bastien, J. Czyzowicz, W. Fraczak, and W. Rytter, "Prime normal form and equivalence of simple grammars”, in International Conference on Implementation and Application of Automata, Springer, 2005, pp. 78-89.C. Bastien, J. Czyzowicz, W. Fraczak, and W. Rytter, "Prime normal form and equivalence of simple grammars”, in International Conference on Implementation and Application of Automata, Springer, 2005, pp. 78-89.Y. Hirshfeld, M. Jerrum, and F. Moller, "A polynomial algorithm for deciding bisimilarity of normed context-free processes”, Theoretical Computer Science, vol. 158, no. 1-2, pp. 143-159,1996.Y. Hirshfeld, M. Jerrum, and F. Moller, "A polynomial algorithm for deciding bisimilarity of normed context-free processes”, Theoretical Computer Science, vol. 158, no. 1-2, pp. 143-159,1996.L. G. Valiant and M. S. Paterson, "Deterministic one-counter automata”, Journal of Computer and System Sciences, vol. 10, no. 3, pp. 340-350, 1975.L. G. Valiant and M. S. Paterson, "Deterministic one-counter automata”, Journal of Computer and System Sciences, vol. 10, no. 3, pp. 340-350, 1975.S. B5hm and S. Goller, "Language equivalence of deterministic real-time one-counter automata is NL-complete”, in International Symposium on Mathematical Foundations of Computer Science, Springer, 2011, pp. 194-205.S. B5hm and S. Goller, "Language equivalence of deterministic real-time one-counter automata is NL-complete”, in International Symposium on Mathematical Foundations of Computer Science, Springer, 2011, pp. 194-205.G. Senizergues, "The equivalence problem for t-turn dpda is co-NP”, in Proceedings of the 30-th International Colloquium on Automata, Languages, and Programming, Springer, 2003, pp. 478-489.G. Senizergues, "The equivalence problem for t-turn dpda is co-NP”, in Proceedings of the 30-th International Colloquium on Automata, Languages, and Programming, Springer, 2003, pp. 478-489.M. Linna, "Two decidability results for deterministic pushdown automata”, Journal of Computer and System Sciences, vol. 18, no. 1, pp. 92-107, 1979.M. Linna, "Two decidability results for deterministic pushdown automata”, Journal of Computer and System Sciences, vol. 18, no. 1, pp. 92-107, 1979.V. Y. Meytus, "The equivalence problem for real-time strict deterministic pushdown automata”, Cybernetics, vol. 25, no. 2, pp. 581-594, 1989.V. Y. Meytus, "The equivalence problem for real-time strict deterministic pushdown automata”, Cybernetics, vol. 25, no. 2, pp. 581-594, 1989.M. Oyamaguchi, "The equivalence problem for real-time DPDAs”, Journal of the ACM, vol. 34, no. 3, pp. 731-760, 1987.M. Oyamaguchi, "The equivalence problem for real-time DPDAs”, Journal of the ACM, vol. 34, no. 3, pp. 731-760, 1987.V. Y. Romanovskii, "Equivalence problem for real-time deterministic pushdown automata”, Cybernetics, vol. 22, no. 2, pp. 162-175, 1985.V. Y. Romanovskii, "Equivalence problem for real-time deterministic pushdown automata”, Cybernetics, vol. 22, no. 2, pp. 162-175, 1985.D. J. Rosenkrantz and R. E. Stearns, "Properties of deterministic top-down grammars”, Information and Control, vol. 17, no. 3, pp. 226-256, 1970.D. J. Rosenkrantz and R. E. Stearns, "Properties of deterministic top-down grammars”, Information and Control, vol. 17, no. 3, pp. 226-256, 1970.E. Tomita, "An extended direct branching algorithm for checking equivalence of deterministic pushdown automata”, Theoretical Computer Science, vol. 32, no. 1-2, pp. 87-120, 1984.E. Tomita, "An extended direct branching algorithm for checking equivalence of deterministic pushdown automata”, Theoretical Computer Science, vol. 32, no. 1-2, pp. 87-120, 1984.E. Ukkonen, "The equivalence problem for some non-real-time deterministic pushdown automata”, Journal of the ACM, vol. 29, no. 4, pp. 1166-1181, 1982.E. Ukkonen, "The equivalence problem for some non-real-time deterministic pushdown automata”, Journal of the ACM, vol. 29, no. 4, pp. 1166-1181, 1982.G. Senizergues, "The equivalence problem for deterministic pushdown automata is decidable”, in Proceedings of the 24-th International Colloquium on Automata, Languages, and Programming, Springer, 1997, pp. 671-681.G. Senizergues, "The equivalence problem for deterministic pushdown automata is decidable”, in Proceedings of the 24-th International Colloquium on Automata, Languages, and Programming, Springer, 1997, pp. 671-681.C. Stirling, "Deciding DPDA equivalence is primitive recursive”, in Proceedings of the 29-th International Colloquium on Automata, Languages, and Programming, Springer, 2002, pp. 821-832.C. Stirling, "Deciding DPDA equivalence is primitive recursive”, in Proceedings of the 29-th International Colloquium on Automata, Languages, and Programming, Springer, 2002, pp. 821-832.R. Madhavan, M. Mayer, S. Gulwani, and V. Kuncak, "Automating grammar comparison”, in Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2015, pp. 183-200.R. Madhavan, M. Mayer, S. Gulwani, and V. Kuncak, "Automating grammar comparison”, in Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2015, pp. 183-200.V. A. Zakharov, "Program equivalence checking by two-tape automata”, Cybernetics and Systems Analysis, vol. 46, no. 4, pp. 554-562, 2010.V. A. Zakharov, "Program equivalence checking by two-tape automata”, Cybernetics and Systems Analysis, vol. 46, no. 4, pp. 554-562, 2010.T. Olshansky and A. Pnueli, "A direct algorithm for checking equivalence of LL(k) grammars”, Theoretical Computer Science, vol. 4, no. 3, pp. 321-349, 1977.T. Olshansky and A. Pnueli, "A direct algorithm for checking equivalence of LL(k) grammars”, Theoretical Computer Science, vol. 4, no. 3, pp. 321-349, 1977.J. Karhumaki, "Equations over finite sets of words and equivalence problems in automata theory”, Theoretical computer science, vol. 108, no. 1, pp. 103-118, 1993.J. Karhumaki, "Equations over finite sets of words and equivalence problems in automata theory”, Theoretical computer science, vol. 108, no. 1, pp. 103-118, 1993.A. Okhotin, "Decision problems for language equations”, Journal of Computer and System Sciences, vol. 76, no. 3-4, pp. 251-266, 2010.A. Okhotin, "Decision problems for language equations”, Journal of Computer and System Sciences, vol. 76, no. 3-4, pp. 251-266, 2010.J. E. Hopcroft, R. Motwani, and J. D. Ullman, Introduction to Automata Theory, Languages, and Computation (3rd ed.) Addison-Wesley, 2006.J. E. Hopcroft, R. Motwani, and J. D. Ullman, Introduction to Automata Theory, Languages, and Computation (3rd ed.) Addison-Wesley, 2006.S. Eilenberg, Automata, languages, and machines. Academic press, 1974.S. Eilenberg, Automata, languages, and machines. Academic press, 1974.Y. Han, K. Salomaa, and D. Wood, "State Complexity of Prefix-Free Regular Languages.”, in DCFS, 2006, pp. 165-176.Y. Han, K. Salomaa, and D. Wood, "State Complexity of Prefix-Free Regular Languages.”, in DCFS, 2006, pp. 165-176.A. Martelli and U. Montanari, "An efficient unification algorithm”, ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 4, no. 2, pp. 258-282, 1982.A. Martelli and U. Montanari, "An efficient unification algorithm”, ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 4, no. 2, pp. 258-282, 1982.D. Arden, "Delayed-logic and finite-state machines”, in Proceedings of 2-nd Annual Symposium on Switching Circuit Theory and Logical Design (SWCT1961), IEEE, 1961, pp. 133-151.D. Arden, "Delayed-logic and finite-state machines”, in Proceedings of 2-nd Annual Symposium on Switching Circuit Theory and Logical Design (SWCT1961), IEEE, 1961, pp. 133-151.J. E. Hopcroft, A linear algorithm for testing equivalence of finite automata. Defense Technical Information Center, 1971, vol. 114.J. E. Hopcroft, A linear algorithm for testing equivalence of finite automata. Defense Technical Information Center, 1971, vol. 114.V. A. Zakharov and G. G. Temerbekova, "On the minimization of finite state transducers over semigroups”, Automatic Control and Computer Sciences, vol. 51, no. 7, pp. 523-530, 2017.V. A. Zakharov and G. G. Temerbekova, "On the minimization of finite state transducers over semigroups”, Automatic Control and Computer Sciences, vol. 51, no. 7, pp. 523-530, 2017.V. E. Itkin, "Logiko-termalnaya ekvivalentnost skhem programm”, Kibernetika i sistemnyj analiz, no. 1, pp. 5-27, 1972.V. E. Itkin, "Logiko-termalnaya ekvivalentnost skhem programm”, Kibernetika i sistemnyj analiz, no. 1, pp. 5-27, 1972.

The authors declare that there are no conflicts of interest present.