Preview

Моделирование и анализ информационных систем

Расширенный поиск

Эффективные алгоритмы проверки эквивалентности для некоторых классов автоматов

https://doi.org/10.18255/1818-1015-2020-3-260-303

Полный текст:

Аннотация

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

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

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

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

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

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

Об авторе

Владимир Анатольевич Захаров
Национальный исследовательский университет Высшая школа экономики
Россия

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



Список литературы

1. A. L. Rosenberg, "A machine realization of the linear context-free languages”, Information and Control, vol. 10, no. 2, pp. 175-188, 1967.

2. M. Mohri, "Finite-state transducers in language and speech processing”, Computational linguistics, vol. 23, no. 2, pp. 269-311, 1997.

3. 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.

4. 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.

5. 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.

6. 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.

7. 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.

8. M. Mohri, "Minimization algorithms for sequential transducers”, Theoretical Computer Science, vol. 234, no. 2, pp. 177-201, 2000.

9. 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.

10. 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.

11. 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.

12. R. Loukanova, "Linear context free languages”, in International Colloquium on Theoretical Aspects of Computing, Springer, 2007, pp. 351-365.

13. B. Bedregal, "λ-ALN: automatos lineares nao-deterministicos com λ-transicoes”, Tendencias em Matematica Aplicada e Computacional, vol. 12, no. 3, pp. 171-182, 2011.

14. 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.

15. 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.

16. O. Klima and L. Polak, "On biautomata*”, RAIRO-Theoretical Informatics and Applications, vol. 46, no. 4, pp. 573-592, 2012.

17. M. Holzer and S. Jakobi, "Minimization and characterizations for biautomata”, Fundamenta Informaticae, vol. 136, no. 1-2, pp. 113-137, 2015.

18. 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.

19. 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.

20. 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.

21. M. Blattner and T. Head, "Single-valued a-transducers”, Journal of Computer and System Sciences, vol. 15, no. 3, pp. 310-327, 1977.

22. M. P. Schutzenberger, "Sur les relations rationnelles”, in Proceedings of the Conference on Automata Theory and Formal Languages, 1975, pp. 209-213.

23. 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.

24. 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.

25. A. Weber, "On the valuedness of finite transducers”, Acta Informatica, vol. 27, no. 8, pp. 749-780,1990.

26. 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.

27. 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.

28. A. Weber, "Decomposing finite-valued transducers and deciding their equivalence”, SIAM Journal on Computing, vol. 22, no. 2, pp. 175-202, 1993.

29. 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.

30. 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.

31. 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.

32. J. Sakarovitch and R. de Souza, "Lexicographic decomposition of ^-valued transducers”, Theory of Computing Systems, vol. 47, no. 3, pp. 758-785, 2010.

33. 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.

34. 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.

35. A. Weber, "On the lengths of values in a finite transducer”, Acta Informatica, vol. 29, no. 6-7, pp.663-687, 1992.

36. 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.

37. M. Bird, "The equivalence problem for deterministic two-tape automata”, Journal of Computer and System Sciences, vol. 7, no. 2, pp. 218-236, 1973.

38. L. G. Valiant, "The equivalence problem for deterministic finite-turn pushdown automata”, Information and Control, vol. 25, no. 2, pp. 123-133, 1974.

39. 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.

40. 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.

41. T. Harju and J. Karhumaki, "The equivalence problem of multitape finite automata”, Theoretical Computer Science, vol. 78, no. 2, pp. 347-355, 1991.

42. 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.

43. B. Bedregal, "Nondeterministic Linear Automata and a Class of Deterministic Linear Languages”, Preliminary Proceedings LSFA, pp. 183-196, 2015.

44. 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.

45. 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.

46. E. P. Friedman, "The inclusion problem for simple languages”, Theoretical Computer Science, vol. 1, no. 4, pp. 297-316, 1976.

47. D. Caucal, "A fast algorithm to decide on simple grammars equivalence”, in International Symposium on Optimal Algorithms, Springer, 1989, pp. 66-85.

48. 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.

49. 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.

50. 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.

51. 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.

52. 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.

53. M. Linna, "Two decidability results for deterministic pushdown automata”, Journal of Computer and System Sciences, vol. 18, no. 1, pp. 92-107, 1979.

54. V. Y. Meytus, "The equivalence problem for real-time strict deterministic pushdown automata”, Cybernetics, vol. 25, no. 2, pp. 581-594, 1989.

55. M. Oyamaguchi, "The equivalence problem for real-time DPDAs”, Journal of the ACM, vol. 34, no. 3, pp. 731-760, 1987.

56. V. Y. Romanovskii, "Equivalence problem for real-time deterministic pushdown automata”, Cybernetics, vol. 22, no. 2, pp. 162-175, 1985.

57. D. J. Rosenkrantz and R. E. Stearns, "Properties of deterministic top-down grammars”, Information and Control, vol. 17, no. 3, pp. 226-256, 1970.

58. 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.

59. 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.

60. 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.

61. 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.

62. 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.

63. V. A. Zakharov, "Program equivalence checking by two-tape automata”, Cybernetics and Systems Analysis, vol. 46, no. 4, pp. 554-562, 2010.

64. 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.

65. 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.

66. A. Okhotin, "Decision problems for language equations”, Journal of Computer and System Sciences, vol. 76, no. 3-4, pp. 251-266, 2010.

67. J. E. Hopcroft, R. Motwani, and J. D. Ullman, Introduction to Automata Theory, Languages, and Computation (3rd ed.) Addison-Wesley, 2006.

68. S. Eilenberg, Automata, languages, and machines. Academic press, 1974.

69. Y. Han, K. Salomaa, and D. Wood, "State Complexity of Prefix-Free Regular Languages.”, in DCFS, 2006, pp. 165-176.

70. 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.

71. 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.

72. J. E. Hopcroft, A linear algorithm for testing equivalence of finite automata. Defense Technical Information Center, 1971, vol. 114.

73. 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.

74. V. E. Itkin, "Logiko-termalnaya ekvivalentnost skhem programm”, Kibernetika i sistemnyj analiz, no. 1, pp. 5-27, 1972.


Для цитирования:


Захаров В.А. Эффективные алгоритмы проверки эквивалентности для некоторых классов автоматов. Моделирование и анализ информационных систем. 2020;27(3):260-303. https://doi.org/10.18255/1818-1015-2020-3-260-303

For citation:


Zakharov V.A. Efficient Equivalence Checking Technique for Some Classes of Finite-State Machines. Modeling and Analysis of Information Systems. 2020;27(3):260-303. (In Russ.) https://doi.org/10.18255/1818-1015-2020-3-260-303

Просмотров: 212


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)