Bisimulations in Memory Finite Automata
https://doi.org/10.15514/ISPRAS-2025-37(6)-33
Abstract
This research aims at studying the bisimulation relation for memory finite automata, which are used as the automata model for extended regular expressions in the series of works, and encapsulate the expressiveness of the named capture groups. We propose an experimental algorithm for checking bisimulation of one-memory MFAs. For multi-memory automata, we show that, in some borderline cases, the bisimulation problem is closely related to a question of whether a parameterized word is always a solution of a given word equation of an arbitrary form.
About the Authors
Antonina Nikolaevna NEPEIVODARussian Federation
Researcher in the Program Systems Institute of RAS. Research interests: formal language theory, program semantics, mathematical logic, and functional programming.
Aleksandr Dmitrievich DELMAN
Russian Federation
Student of the Bauman Moscow State Technical University. Research interests: compiler design and natural language processing.
Anna Sergeevna TERENTYEVA
Russian Federation
Student of the Bauman Moscow State Technical University. Research interests: compiler design and optimization.
References
1. I. Free Software Foundation. (1993–2024) The GNU ed line editor. [Online]. Available: https://www.gnu.org/software/ed/manual/edmanual.html
2. D. D. Freydenberger, “Inclusion of pattern languages and related problems,” Ph.D. dissertation, Goe-the University Frankfurt am Main, 2011. [Online]. Available: http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/22351
3. T. Jiang, A. Salomaa, K. Salomaa, and S. Yu, “Inclusion is undecidable for pattern languages,” in Au-tomata, Languages and Programming, A. Lingas, R. Karlsson, and S. Carlsson, Eds. Berlin, Heidel-berg: Springer Berlin Heidelberg, 1993, pp. 301–312.
4. Google. (2010–2023) Official public repository of RE2 library. [Online]. Available: https://github.com/google/re2
5. C. Bianchini, B.Riccardi, A. Policriti, and R.Romanello, “Incremental NFA minimization,” in CEUR Workshop Proceedings, 2022.
6. C. Fu, Y. Deng, D. N. Jansen, and L. Zhang, “On equivalence checking of nondeterministic finite au-tomata,” in Dependable Software Engineering. Theories, Tools, and Applications, K. G. Larsen, O. Sokolsky, and J. Wang, Eds. Cham: Springer International Publishing, 2017, pp. 216–231.
7. F. Bonchi and D. Pous, “Checking NFA equivalence with bisimulations up to congruence,” SIGPLAN Not., vol. 48, no. 1, p. 457–468, jan 2013. [Online]. Available: https://doi.org/10.1145/2480359.2429124
8. C. Stirling, “Decidability of bisimulation equivalence for normed pushdown processes,” Theoretical Computer Science, vol. 195, no. 2, pp. 113–131, 1998, concurrency Theory. [Online]. Available: https://www.sciencedirect.com/science/article/pii/S0304397597002168
9. M. Benedikt, S. Goller, S. Kiefer, and A. S. Murawski, “Bisimilarity of pushdown automata is non-elementary,” in 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013, pp. 488–498.
10. L. D’Antoni and M. Veanes, “Forward bisimulations for nondeterministic symbolic finite automata,” in Tools and Algorithms for the Construction and Analysis of Systems, A. Legay and T. Margaria, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2017, pp. 518–534.
11. M. Berglund and B. van der Merwe, “Re-examining regular expressions with backreferences,” Theo-retical Computer Science, vol. 940, pp. 66–80, 2023. [Online]. Available: https://www.sciencedirect.com/science/article/pii/S0304397522006570
12. J. L. Peterson, Petri Net Theory and the Modelling of Systems. Prentice-Hall, April 1981.
13. L. Aceto, A. Ingolfsdottir, and J. Srba, The algorithmics of bisimilarity, ser. Cambridge Tracts in The-oretical Computer Science. Cambridge University Press, 2011, pp. 100–172. [Online]. Available: https://doi.org/10.1017/CBO9780511792588.004
14. M. L. Schmid, “Characterising REGEX languages by regular languages equipped with factor-referencing,” Information and Computation, vol. 249, pp. 1–17, 2016. [Online]. Available: https://www.sciencedirect.com/science/article/pii/S0890540116000109
15. P. Hazel. (1997–2021) PCRE2 electronic manual. [Online]. Available: https://www.pcre.org/current/doc/html/index.html
16. D. D. Freydenberger and M. L. Schmid, “Deterministic regular expressions with back-references,” Journal of Computer and System Sciences, vol. 105, pp. 1–39, 2019. [Online]. Available: https://doi.org/10.1016/j.jcss.2019.04.001
17. V. M. Glushkov, “The abstract theory of automata,” Uspekhi Mat. Nauk, vol. 16, pp. 3–62, 1961. [Online]. Available: http://mi.mathnet.ru/rm6668
18. J. D. Day, F. Manea, and D. Nowotka, “The hardness of solving simple word equations”, 42nd Inter-national Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz Inter-national Proceedings in Informatics (LIPIcs), Volume 83, pp. 18:1-18:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) Available: https://doi.org/10.4230/LIPIcs.MFCS.2017.18
19. D. Ismagilova and A. Nepeivoda, “Disambiguation of regular expressions with backreferences via term rewriting,” Modeling and Analysis of Information Systems, vol. 31 iss. 4, pp. 426-445, 2024. [Online]. https://doi.org/10.18255/1818-1015-2024-4-426-445
20. J. D. Day, V. Ganesh, and F. Manea, “Formal languages via theories over strings: An overview of some recent results,” Bull. EATCS, vol. 140, 2023. [Online]. Available: http://eatcs.org/beatcs/index.php/beatcs/article/view/765
21. G. S. Makanin, “The problem of solvability of equations in a free semigroup,” Mat. Sb. (N.S.), vol. 103(145), pp. 147–236, 1977.
Review
For citations:
NEPEIVODA A.N., DELMAN A.D., TERENTYEVA A.S. Bisimulations in Memory Finite Automata. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2025;37(6):7-18. https://doi.org/10.15514/ISPRAS-2025-37(6)-33






