On the Minimization of Finite State Trans- ducers over Semigroups
https://doi.org/10.18255/1818-1015-2016-6-741-753
Abstract
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.
About the Authors
V. A. Zakharov
Lomonosov Moscow State University
Russian Federation
Russian Federation
PhD, professor, Faculty of Computational Mathematics and Cybernetics, GSP-1, 1-52 Leninskiye Gory, Moscow 119991, Russia
G. G. Temerbekova
Lomonosov Moscow State University
Russian Federation
Russian Federation
graduate student, Faculty of Computational Mathematics and Cybernetics, GSP-1, 1-52 Leninskiye Gory, Moscow 119991, Russia
References
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.
2. Blattner M, Head T., “Single-valued a-transducers”, J. of Comput. and Syst. Sci., 15:3 (1977), 310–327.
3. Blattner M, Head T., “The decidability of equivalence for deterministic finite transducers”, J. of Comput. and Syst. Sci., 19:1 (1979), 45–49.
4. Beal M.-P., Carton O., “Computing the prefix of an automaton”, Theoretical Informatics and Applications, 34:6 (2000), 503–514.
5. Culik K., Karhumaki J., “The equivalence of finite-valued transducers (on HDTOL languages) is decidable”, Theor. Comput. Sci., 47 (1986), 71–84.
6. Diekert V., Metivier Y., “Partial commutation and traces”, Handbook of formal languages, 3, 1997, 457–533.
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, 1, 2003, 64–71.
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.
9. Griffiths T., “The unsolvability of the equivalence problem for ε-free nondeterministic generalized machines”, J. of the ACM, 15 (1968), 409–413.
10. Mohri M., “Finite-state transducers in language and speech processing”, Comput. Ling, 23:2 (1997), 269–311.
11. Mohri M., “Minimization algorithms for sequential transducers”, Theor. Comput. Sci., 234 (2000), 177–201.
12. Reutenauer C., Schuzenberger M. P., “Minimization of rational word functions”, SIAM J. of Comput., 20:4 (1991), 6699685.
13. Shofrutt C., “Minimizing subsequential transducers: a survey”, Theor. Comput. Sci., 292:1 (2003), 1311143.
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.
16. Watson B. W., “A taxonomy of finite automata minimization algorithm”, Computing Science Report. Eindhoven University of Technology, 93/44 (2005), 1–32.
17. Weber A., “Decomposing finite-valued transducers and deciding their equivalence”, SIAM Journal on Computing, 22:1 (1993), 175–202.
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), 88897.
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.
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).
21.
Review
For citations:
Zakharov V.A., Temerbekova G.G. On the Minimization of Finite State Trans- ducers over Semigroups. Modeling and Analysis of Information Systems. 2016;23(6):741-753. (In Russ.) https://doi.org/10.18255/1818-1015-2016-6-741-753
Views:
884
Email this article 