Efficient equivalence checking technique for some classes of finite-state machines

V. A. Zakharov

Modelirovanie i analiz informacionnyh sistem, Tome 27 (2020) no. 3, pp. 260-303.

Résumé

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. 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. 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 $\varepsilon$-transitions) relative to the sizes of analysed machines. 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. 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. 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.

Détail

Keywords: transducer, two-tape automaton, equivalence checking, prefix-free language, language equation, decision procedure.
Mots-clés : biatomaton, simple grammar

Bibliographie

[1] A. L. Rosenberg, “A machine realization of the linear context-free languages”, Information and Control, 10:2 (1967), 175–188 | DOI | Zbl

[2] M. Mohri, “Finite-state transducers in language and speech processing”, Computational linguistics, 23:2 (1997), 269–311 | MR

[3] A. Roche-Lima, R. K. Thulasiram, “Bioinformatics algorithm based on a parallel implementation of a machine learning approach using transducers”, Journal of Physics: Conference Series, 341:1 (2012), 012–034

[4] R. Alur, P. Cerny, “Streaming transducers for algorithmic verification of single-pass list-processing programs”, Proceedings of 38-th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 2011, 599–610 | DOI | Zbl

[5] J. Thakkar, A. Kanade, R. Alur, “Transducer-based algorithmic verification of retransmission protocols over noisy channels”, Proceedings of IFIP Joint International Conference on Formal Techniques for Distributed Systems, Springer, 2013, 209–224 | DOI

[6] M. Veanes, P. Hooimeijer, B. Livshits, and et al, “Symbolic finite state transducers: Algorithms and applications”, Proceedings of the 39-th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 2012, 137–150 | DOI | Zbl

[7] D. G. Kozlova, V. A. Zakharov, “On the model checking of sequential reactive systems”, Proceedings of the 25-th International Workshop on Concurrency, Specification and Programming (Rostock, Germany, September 28–30), CEUR Workshop Proceedings, 1698, 2016, 233

[8] M. Mohri, “Minimization algorithms for sequential transducers”, Theoretical Computer Science, 234:2 (2000), 177–201 | DOI | MR | Zbl

[9] V. A. Zakharov, S. R. Jaylauova, “On the minimization problem for sequential programs”, Automatic Control and Computer Sciences, 51:7 (2017), 689–700 | DOI | MR

[10] H. Tamm, M. Nykanen, E. Ukkonen, “On size reduction techniques for multitape automata”, Theoretical computer science, 363:2 (2006), 234–246 | DOI | MR | Zbl

[11] D. C. Luckham, D. M. Park, M. S. Paterson, “On formalized computer programs”, Journal of Computer and System Sciences, 4:3 (1970), 220–249 | DOI | MR | Zbl

[12] R. Loukanova, “Linear context free languages”, International Colloquium on Theoretical Aspects of Computing, Springer, 2007, 351–365 | Zbl

[13] B. Bedregal, “$\lambda$-ALN: automatos lineares ñao-deterministicos com $\lambda$-transições”, Tendencias em Matematica Aplicada e Computacional, 12:3 (2011), 171–182 | DOI | MR | Zbl

[14] G. Jiraskova, O. Klima, “Deterministic Biautomata and Subclasses of Deterministic Linear Languages”, International Conference on Language and Automata theory and Applications, Springer, 2019, 315–327 | DOI | MR | Zbl

[15] M. Holzer, S. Jakobi, “Nondeterministic biautomata and their descriptional complexity”, International Workshop on Descriptional Complexity of Formal Systems, Springer, 2013, 112–123 | DOI | MR | Zbl

[16] O. Klima, L. Polak, “On biautomata*”, RAIRO-Theoretical Informatics and Applications, 46:4 (2012), 573–592 | DOI | MR | Zbl

[17] M. Holzer, S. Jakobi, “Minimization and characterizations for biautomata”, Fundamenta Informaticae, 136:1-2 (2015), 113–137 | DOI | MR | Zbl

[18] P. C. Fischer, A. L. Rosenberg, “Multitape one-way nonwriting automata”, Journal of Computer and System Sciences, 2:1 (1968), 88–101 | DOI | MR | Zbl

[19] T. Griffiths, “The unsolvability of the equivalence problem for $\Lambda$-free nondeterministic generalized machines”, Journal of the ACM (JACM), 15:3 (1968), 409–413 | DOI | MR | Zbl

[20] O. Ibarra, “The unsolvability of the equivalence problem for $\varepsilon$-free NGSM's with unary input (output) alphabet and applications”, SIAM Journal on Computing, 7:4 (1978), 524–532 | DOI | MR | Zbl

[21] M. Blattner, T. Head, “Single-valued a-transducers”, Journal of Computer and System Sciences, 15:3 (1977), 310–327 | DOI | MR | Zbl

[22] M. P. Schutzenberger, “Sur les relations rationnelles”, Proceedings of the Conference on Automata theory and Formal Languages, 1975, 209–213 | MR | Zbl

[23] M. Blattner, T. Head, “The decidability of equivalence for deterministic finite transducers”, Journal of Computer and System Sciences, 19:1 (1979), 45–49 | DOI | MR | Zbl

[24] E. M. Gurari, O. Ibarra, “A note on finite-valued and finitely ambiguous transducers”, Mathematical systems theory, 16:1 (1983), 61–66 | DOI | MR | Zbl

[25] A. Weber, “On the valuedness of finite transducers”, Acta Informatica, 27:8 (1990), 749–780 | DOI | MR | Zbl

[26] K. Culik, J. Karhumaki, “The equivalence of finite valued transducers (on HDT0L languages) is decidable”, Theoretical computer science, 47 (1986), 71–84 | DOI | MR | Zbl

[27] A. Weber, “A decomposition theorem for finite-valued transducers and an application to the equivalence problem”, Proceedings of the 13-th International Symposium on Mathematical Foundations of Computer Science, Springer, 1988, 552–562 | MR

[28] A. Weber, “Decomposing finite-valued transducers and deciding their equivalence”, SIAM Journal on Computing, 22:2 (1993), 175–202 | DOI | MR | Zbl

[29] M.-P. Beal, O. Carton, C. Prieur, J. Sakarovitch, “Squaring transducers: an efficient procedure for deciding functionality and sequentiality”, Theoretical computer science, 292:1 (2003), 45–63 | DOI | MR | Zbl

[30] J. Sakarovitch, R. de Souza, “On the decomposition of $k$-valued rational relations”, Proceedings of the 25-th International Symposium on Mathematical Foundations of Computer Science, 2008, 588–600 | MR | Zbl

[31] J. Sakarovitch, R. de Souza, “On the decidability of bounded valuedness for transducers”, Proceedings of the 25-th International Symposium on Mathematical Foundations of Computer Science, 2008, 588–600 | MR | Zbl

[32] J. Sakarovitch, R. de Souza, “Lexicographic decomposition of $k$-valued transducers”, Theory of Computing Systems, 47:3 (2010), 758–785 | DOI | MR | Zbl

[33] R. de Souza, “On the decidability of the equivalence for k-valued transducers”, Proceedings of the 12-th International Conference on Developments in Language Theory, Springer, 2008, 252–263 | DOI | Zbl

[34] V. A. Zakharov, “Equivalence checking problem for finite state transducers over semigroups”, Proceedings of the 6-th International Conference on Algebraic Informatics, Springer, 2015, 208–221 | DOI | MR | Zbl

[35] A. Weber, “On the lengths of values in a finite transducer”, Acta Informatica, 29:6-7 (1992), 663–687 | DOI | MR | Zbl

[36] R. de Souza, “On the Decidability of the Equivalence for a Certain Class of Transducers”, Proceedings of the 13-th International Conference on Developments in Language Theory, Springer, 2009, 478–489 | DOI | Zbl

[37] M. Bird, “The equivalence problem for deterministic two-tape automata”, Journal of Computer and System Sciences, 7:2 (1973), 218–236 | DOI | MR | Zbl

[38] L. G. Valiant, “The equivalence problem for deterministic finite-turn pushdown automata”, Information and Control, 25:2 (1974), 123–133 | DOI | MR | Zbl

[39] C. Beeri, “An improvement on Valiant's decision procedure for equivalence of deterministic finite turn pushdown machines”, Theoretical computer science, 3:3 (1976), 305–320 | DOI | MR

[40] E. P. Friedman, S. A. Greibach, “A polynomial time algorithm for deciding the equivalence problem for 2-tape deterministic finite state acceptors”, SIAM Journal on Computing, 11:1 (1982), 166–183 | DOI | MR | Zbl

[41] T. Harju, J. Karhumaki, “The equivalence problem of multitapenite automata”, Theoretical Computer Science, 78:2 (1991), 347–355 | DOI | MR | Zbl

[42] J. Worrell, “Revisiting the equivalence problem for finite multitape automata”, Proceedings of the 40-th International Colloquium on Automata, Languages, and Programming, Springer, 2013, 422–433 | MR | Zbl

[43] B. Bedregal, “Nondeterministic Linear Automata and a Class of Deterministic Linear Languages”, Preliminary Proceedings LSFA, 2015, 183–196

[44] Y. Bar-Hillel, M. Perles, E. Shamir, “On formal properties of simple phrase structure grammars”, Sprachtypologie und Universalienforschung, 14 (1961), 143–172 | MR

[45] A. J. Korenjak, J. E. Hopcroft, “Simple deterministic languages”, 7th Annual Symposium on Switching and Automata theory (swat 1966), IEEE, 1966, 36–46 | DOI

[46] E. P. Friedman, “The inclusion problem for simple languages”, Theoretical Computer Science, 1:4 (1976), 297–316 | DOI | MR | Zbl

[47] D. Caucal, “A fast algorithm to decide on simple grammars equivalence”, International Symposium on Optimal Algorithms, Springer, 1989, 66–85 | DOI | MR

[48] C. Bastien, J. Czyzowicz, W. Fraczak, W. Rytter, “Prime normal form and equivalence of simple grammars”, International Conference on Implementation and Application of Automata, Springer, 2005, 78–89 | MR

[49] Y. Hirshfeld, M. Jerrum, F. Moller, “A polynomial algorithm for deciding bisimilarity of normed context-free processes”, Theoretical Computer Science, 158:1-2 (1996), 143–159 | DOI | MR | Zbl

[50] L. G. Valiant, M. S. Paterson, “Deterministic one-counter automata”, Journal of Computer and System Sciences, 10:3 (1975), 340–350 | DOI | MR | Zbl

[51] S. Böhm, S. Göller, “Language equivalence of deterministic real-time one-counter automata is NL-complete”, International Symposium on Mathematical Foundations of Computer Science, Springer, 2011, 194–205 | MR | Zbl

[52] G. Senizergues, “The equivalence problem for t-turn dpda is co-NP”, Proceedings of the 30-th International Colloquium on Automata, Languages, and Programming, Springer, 2003, 478–489 | MR | Zbl

[53] M. Linna, “Two decidability results for deterministic pushdown automata”, Journal of Computer and System Sciences, 18:1 (1979), 92–107 | DOI | MR | Zbl

[54] V. Y. Meytus, “The equivalence problem for real-time strict deterministic pushdown automata”, Cybernetics, 25:2 (1989), 581–594 | MR

[55] M. Oyamaguchi, “The equivalence problem for real-time DPDAs”, Journal of the ACM, 34:3 (1987), 731–760 | DOI | MR | Zbl

[56] V. Y. Romanovskii, “Equivalence problem for real-time deterministic pushdown automata”, Cybernetics, 22:2 (1985), 162–175 | DOI | MR

[57] D. J. Rosenkrantz, R. E. Stearns, “Properties of deterministic top-down grammars”, Information and Control, 17:3 (1970), 226–256 | DOI | MR | Zbl

[58] E. Tomita, “An extended direct branching algorithm for checking equivalence of deterministic pushdown automata”, Theoretical Computer Science, 32:1-2 (1984), 87–120 | DOI | MR | Zbl

[59] E. Ukkonen, “The equivalence problem for some non-real-time deterministic pushdown automata”, Journal of the ACM, 29:4 (1982), 1166–1181 | DOI | MR | Zbl

[60] G. Senizergues, “The equivalence problem for deterministic pushdown automata is decidable”, Proceedings of the 24-th International Colloquium on Automata, Languages, and Programming, Springer, 1997, 671–681 | DOI | MR | Zbl

[61] C. Stirling, “Deciding DPDA equivalence is primitive recursive”, Proceedings of the 29-th International Colloquium on Automata, Languages, and Programming, Springer, 2002, 821–832 | MR | Zbl

[62] R. Madhavan, M. Mayer, S. Gulwani, V. Kuncak, “Automating grammar comparison”, Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2015, 183–200 | DOI

[63] V. A. Zakharov, “Program equivalence checking by two-tape automata”, Cybernetics and Systems Analysis, 46:4 (2010), 554–562 | DOI | MR | Zbl

[64] T. Olshansky, A. Pnueli, “A direct algorithm for checking equivalence of LL(k) grammars”, Theoretical Computer Science, 4:3 (1977), 321–349 | DOI | MR | Zbl

[65] J. Karhumaki, “Equations over finite sets of words and equivalence problems in automata theory”, Theoretical computer science, 108:1 (1993), 103–118 | DOI | MR | Zbl

[66] A. Okhotin, “Decision problems for language equations”, Journal of Computer and System Sciences, 76:3-4 (2010), 251–266 | DOI | MR | Zbl

[67] J. E. Hopcroft, R. Motwani, J. D. Ullman, Introduction to Automata theory, Languages, and Computation, 3rd ed., Addison-Wesley, 2006 | MR

[68] S. Eilenberg, Automata, languages, machines, Academic press, 1974 | MR | Zbl

[69] Y. Han, K. Salomaa, D. Wood, “State Complexity of Prefix-Free Regular Languages”, DCFS, 2006, 165–176 | MR

[70] A. Martelli, U. Montanari, “An efficient unification algorithm”, ACM Transactions on Programming Languages and Systems (TOPLAS), 4:2 (1982), 258–282 | DOI | Zbl

[71] D. Arden, “Delayed-logic and finite-state machines”, Proceedings of 2-nd Annual Symposium on Switching Circuiteory and Logical Design, SWCT 1961, IEEE, 1961, 133–151 | DOI | MR

[72] J. E. Hopcroft, A linear algorithm for testing equivalence of finite automata, Computer Science Technical Reports No 114, Defense Technical Information Center, 1971

[73] V. A. Zakharov, G. G. Temerbekova, “On the minimization of finite state transducers over semigroups”, Automatic Control and Computer Sciences, 51:7 (2017), 523–530 | DOI | MR

[74] V. E. Itkin, “Logiko-termalnaya ekvivalentnost skhem programm”, Kibernetika i sistemnyj analiz, 1972, no. 1, 5–27 | Zbl