Get 20M+ Full-Text Papers For Less Than $1.50/day. Start a 14-Day Trial for You or Your Team.

Learn More →

Efficient Equivalence Checking Technique for Some Classes of Finite-State Machines

Efficient Equivalence Checking Technique for Some Classes of Finite-State Machines 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, and 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 \documentclass[12pt]{minimal}\usepackage{amsmath}\usepackage{wasysym}\usepackage{amsfonts}\usepackage{amssymb}\usepackage{amsbsy}\usepackage{mathrsfs}\usepackage{upgreek}\setlength{\oddsidemargin}{-69pt}\begin{document}$$O(n\;\text{log}\;n)$$\end{document}. 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 time (for prefix-free transducers with \documentclass[12pt]{minimal}\usepackage{amsmath}\usepackage{wasysym}\usepackage{amsfonts}\usepackage{amssymb}\usepackage{amsbsy}\usepackage{mathrsfs}\usepackage{upgreek}\setlength{\oddsidemargin}{-69pt}\begin{document}$$\varepsilon $$\end{document}-transitions) relative to the size of analyzed 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 analyzed 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 size of analyzed 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. http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png Automatic Control and Computer Sciences Springer Journals

Efficient Equivalence Checking Technique for Some Classes of Finite-State Machines

Download PDF
32 pages

Loading next page...
 
/lp/springer-journals/efficient-equivalence-checking-technique-for-some-classes-of-finite-LUjW5VNngE
Publisher
Springer Journals
Copyright
Copyright © Allerton Press, Inc. 2021. ISSN 0146-4116, Automatic Control and Computer Sciences, 2021, Vol. 55, No. 7, pp. 670–701. © Allerton Press, Inc., 2021. Russian Text © The Author(s), 2020, published in Modelirovanie i Analiz Informatsionnykh Sistem, 2020, No. 3, pp. 260–303.
ISSN
0146-4116
eISSN
1558-108X
DOI
10.3103/s014641162107018x
Publisher site
See Article on Publisher Site

Abstract

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, and 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 \documentclass[12pt]{minimal}\usepackage{amsmath}\usepackage{wasysym}\usepackage{amsfonts}\usepackage{amssymb}\usepackage{amsbsy}\usepackage{mathrsfs}\usepackage{upgreek}\setlength{\oddsidemargin}{-69pt}\begin{document}$$O(n\;\text{log}\;n)$$\end{document}. 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 time (for prefix-free transducers with \documentclass[12pt]{minimal}\usepackage{amsmath}\usepackage{wasysym}\usepackage{amsfonts}\usepackage{amssymb}\usepackage{amsbsy}\usepackage{mathrsfs}\usepackage{upgreek}\setlength{\oddsidemargin}{-69pt}\begin{document}$$\varepsilon $$\end{document}-transitions) relative to the size of analyzed 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 analyzed 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 size of analyzed 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.

Journal

Automatic Control and Computer Sciences – Springer Journals

Published: Dec 1, 2021

Keywords: transducer; two-tape automaton; biatomaton; simple grammar; equivalence checking; prefix-free language; language equation; decision procedure

References

  • A machine realization of the linear context-free languages
    Rosenberg, A.L.
  • Finite-state transducers in language and speech processing
    Mohri, M.
  • Bioinformatics algorithm based on a parallel implementation of a machine learning approach using transducers
    Roche-Lima, A.; Thulasiram, R.K.
  • Minimization algorithms for sequential transducers
    Mohri, M.
  • On the minimization problem for sequential programs
    Zakharov, V.A.; Jaylauova, S.R.
  • On size reduction techniques for multitape automata
    Tamm, H.; Nykänen, M.; Ukkonen, E.
  • On formalized computer programs
    Luckham, D.C.; Park, D.M.; Paterson, M.S.
  • λ-ALN: Autômatos lineares não-determinísticos com λ-transições
    Bedregal, B.
  • On biautomata*, RAIRO - Theor.
    Klima, O.; Polak, L.
  • Minimization and characterizations for biautomata
    Holzer, M.; Jakobi, S.
  • Multitape one-way nonwriting automata
    Fischer, P.C.; Rosenberg, A.L.
  • The unsolvability of the equivalence problem for Λ-free nondeterministic generalized machines
    Griffiths, T.
  • The unsolvability of the equivalence problem for ε-free NGSM’s with unary input (output) alphabet and applications
    Ibarra, O.
  • Single-valued a-transducers
    Blattner, M.; Head, T.
  • The decidability of equivalence for deterministic finite transducers
    Blattner, M.; Head, T.
  • A note on finite-valued and finitely ambiguous transducers
    Gurari, E.M.; Ibarra, O.
  • On the valuedness of finite transducers
    Weber, A.
  • The equivalence of finite valued transducers (on HDT0L languages) is decidable
    Culik, K.; Karhumäki, J.
  • Decomposing finite-valued transducers and deciding their equivalence
    Weber, A.
  • Squaring transducers: An efficient procedure for deciding functionality and sequentiality
    Béal, M.-P.; Carton, O.; Prieur, C.; Sakarovitch, J.
  • Lexicographic decomposition of k-valued transducers
    Sakarovitch, J.; de Souza, R.
  • On the lengths of values in a finite transducer
    Weber, A.
  • The equivalence problem for deterministic two-tape automata
    Bird, M.
  • The equivalence problem for deterministic finite-turn pushdown automata
    Valiant, L.G.
  • An improvement on Valiant’s decision procedure for equivalence of deterministic finite turn pushdown machines
    Beeri, C.
  • A polynomial time algorithm for deciding the equivalence problem for 2‑tape deterministic finite state acceptors
    Friedman, E.P.; Greibach, S.A.
  • The equivalence problem of multitape finite automata
    Harju, T.; Karhumäki, J.
  • On formal properties of simple phrase structure grammars, Sprachtypol.
    Bar-Hillel, Y.; Perles, M.; Shamir, E.
  • The inclusion problem for simple languages
    Friedman, E.P.
  • A polynomial algorithm for deciding bisimilarity of normed context-free processes
    Hirshfeld, Y.; Jerrum, M.; Moller, F.
  • Deterministic one-counter automata
    Valiant, L.G.; Paterson, M.S.
  • Two decidability results for deterministic pushdown automata
    Linna, M.
  • The equivalence problem for real-time strict deterministic pushdown automata
    Meytus, V.Y.
  • The equivalence problem for real-time DPDAs
    Oyamaguchi, M.
  • Equivalence problem for real-time deterministic pushdown automata
    Romanovskii, V.Y.
  • Properties of deterministic top-down grammars
    Rosenkrantz, D.J.; Stearns, R.E.
  • An extended direct branching algorithm for checking equivalence of deterministic pushdown automata
    Tomita, E.
  • The equivalence problem for some non-real-time deterministic pushdown automata
    Ukkonen, E.
  • Program equivalence checking by two-tape automata
    Zakharov, V.A.
  • A direct algorithm for checking equivalence of LL(k) grammars
    Olshansky, T.; Pnueli, A.
  • Equations over finite sets of words and equivalence problems in automata theory
    Karhumäki, J.
  • Decision problems for language equations
    Okhotin, A.
  • An efficient unification algorithm
    Martelli, A.; Montanari, U.
  • On the minimization of finite state transducers over semigroups
    Zakharov, V.A.; Temerbekova, G.G.