On the minimization of finite state transducers over semigroups

V. A. Zakharov ; G. G. Temerbekova

Modelirovanie i analiz informacionnyh sistem, Tome 23 (2016) no. 6, pp. 741-753.

Résumé

Finite state transducers over semigroups are regarded as a formal model of sequential reactive programs that operate in the interaction with the environment. At receiving a piece of data a program performs a sequence of actions and displays the current result. Such programs usually arise at implementation of computer drivers, on-line algorithms, control procedures. In many cases verification of such programs can be reduced to minimization and equivalence checking problems for finite state transducers. Minimization of a transducer over a semigroup is performed in three stages. At first the greatest common left-divisors are computed for all states of the transducer, next the transducer is brought to a reduced form by pulling all such divisors “upstream”, and finally a minimization algorithm for finite state automata is applied to the reduced transducer.

Détail

Keywords: reactive system, transducer, semigroup, minimization, equivalence checking.

Bibliographie

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

[2] Blattner M, Head T., “Single-valued a-transducers”, J. of Comput. and Syst. Sci., 15:3 (1977), 310–327 | DOI | MR | Zbl

[3] Blattner M, Head T., “The decidability of equivalence for deterministic finite transducers”, J. of Comput. and Syst. Sci., 19:1 (1979), 45–49 | DOI | MR | Zbl

[4] Beal M.-P., Carton O., “Computing the prefix of an automaton”, Theoretical Informatics and Applications, 34:6 (2000), 503–514 | DOI | MR | Zbl

[5] Culik K., Karhumaki J., “The equivalence of finite-valued transducers (on HDTOL languages) is decidable”, Theor. Comput. Sci., 47 (1986), 71–84 | DOI | MR | Zbl

[6] Diekert V., Metivier Y., “Partial commutation and traces”, Handbook of formal languages, v. 3, 1997, 457–533 | DOI | MR

[7] Eisner J., “Simpler and more general minimization for weighted finite-state automata”, Proc. of the 2003 Conference of the North American Chapter of the Association for Computational Linguistics on Human Language Technology, v. 1, 2003, 64–71 | DOI

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

[9] Griffiths T., “The unsolvability of the equivalence problem for $\varepsilon$-free nondeterministic generalized machines”, J. of the ACM, 15 (1968), 409–413 | DOI | MR | Zbl

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

[11] Mohri M., “Minimization algorithms for sequential transducers”, Theor. Comput. Sci., 234 (2000), 177–201 | DOI | MR | Zbl

[12] Reutenauer C., Schuzenberger M. P., “Minimization of rational word functions”, SIAM J. of Comput., 20:4 (1991), 669–685 | DOI | MR | Zbl

[13] Shofrutt C., “Minimizing subsequential transducers: a survey”, Theor. Comput. Sci., 292:1 (2003), 131–143 | DOI | MR

[14] Thakkar J., Kanade A., Alur R., “A transducer-based algorithmic verification of retransmission protocols over noisy channels”, Proc. of IFIP Joint International Conference on Formal Techniques for Distributed Systems, LNCS, 7892, 2013, 209–224

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

[16] Watson B. W., A taxonomy of finite automata minimization algorithm, Computing Science Report, No 93/44, Eindhoven University of Technology, 2005, 32 pp.

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

[18] Wolper P., Boigelot B., “Verifying systems with infinite but regular state spaces”, Proc. 10th Int. Conf. on Computer Aided Verification, CAV-1998, LNCS, 1427, 1998, 88–97 | MR

[19] Zakharov V. A., “Equivalence checking problem for finite state transducers over semigroups”, Proc. of the 6-th International Conference on Algebraic Informatics, CAI-2015, LNCS, 9270, 2015, 208–221 | MR | Zbl

[20] Zakharov V. A., Podymov V. V., “Primenenije algoritmov proverki ekvivalentnisti dlya optimizacii program”, Trudy insituta sistemnogo programmirovaniya, 27:3 (2015), 145–174 (in Russian)