maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2016-6-741-753mais-411Research ArticleОригинальные статьиArticlesО минимизации конечных автоматов-преобразователей над полугруппамиOn the Minimization of Finite State Trans- ducers over Semigroupshttps://orcid.org/0000-0002-3794-9565ЗахаровВ. А.ZakharovV. A.

доктор физ.-мат. наук, профессор, факультет ВМК, Ленинские горы, д. 1, стр. 52, ГСП-1, Москва, 119991, Россия

PhD, professor, Faculty of Computational Mathematics and Cybernetics, GSP-1, 1-52 Leninskiye Gory, Moscow 119991, Russia

zakh@cs.msu.ruhttps://orcid.org/0000-0002-5856-8788ТемербековаГ. Г.TemerbekovaG. G.

магистр, факультет ВМК, Ленинские горы, д. 1, стр. 52, ГСП-1, Москва, 119991, Россия

graduate student, Faculty of Computational Mathematics and Cybernetics, GSP-1, 1-52 Leninskiye Gory, Moscow 119991, Russia

gulgaisha93@mail.ruМосковский государственный университет им. М.В. ЛомоносоваРоссияLomonosov Moscow State UniversityRussian Federation201620122016236741753Copyright © Захаров В.А., Темербекова Г.Г., 20162016Захаров В.А., Темербекова Г.Г.Zakharov V.A., Temerbekova G.G.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/411

Автоматы-преобразователи над полугруппами можно использовать в качестве модели последовательных реагирующих программ, работающих в постоянном взаимодействии со своим окружением. Получив очередную порцию данных, реагирующая программа выполняет некоторую последовательность действий и предъявляет результат. Такие программы возникают при проектировании компьютерных драйверов, алгоритмов, работающих в оперативном режиме, сетевых коммутаторов. Во многих случаях проблема верификации программ такого рода может быть сведена к задачам минимизации и проверки эквивалентности конечных автоматовпреобразователей. Минимизация преобразователей над полугруппами проводится в три этапа. Вначале для всех состояний преобразователя вычисляются наибольшие общие левые делители. Затем все вычисленные делители ”поднимаются вверх” по переходам преобразователя, и в результате образуется приведенный преобразователь. Наконец, для минимизации приведенных преобразователей применяются методы минимизации классических конечных автоматов-распознавателей.

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.

реагирующая системаавтомат-преобразовательполугруппаминимизацияпроверка эквивалентностиreactive systemtransducersemigroupminimizationequivalence checkingReferencesAlur 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.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.Blattner M, Head T., “Single-valued a-transducers”, J. of Comput. and Syst. Sci., 15:3 (1977), 310–327.Blattner M, Head T., “Single-valued a-transducers”, J. of Comput. and Syst. Sci., 15:3 (1977), 310–327.Blattner M, Head T., “The decidability of equivalence for deterministic finite transducers”, J. of Comput. and Syst. Sci., 19:1 (1979), 45–49.Blattner M, Head T., “The decidability of equivalence for deterministic finite transducers”, J. of Comput. and Syst. Sci., 19:1 (1979), 45–49.Beal M.-P., Carton O., “Computing the prefix of an automaton”, Theoretical Informatics and Applications, 34:6 (2000), 503–514.Beal M.-P., Carton O., “Computing the prefix of an automaton”, Theoretical Informatics and Applications, 34:6 (2000), 503–514.Culik K., Karhumaki J., “The equivalence of finite-valued transducers (on HDTOL languages) is decidable”, Theor. Comput. Sci., 47 (1986), 71–84.Culik K., Karhumaki J., “The equivalence of finite-valued transducers (on HDTOL languages) is decidable”, Theor. Comput. Sci., 47 (1986), 71–84.Diekert V., Metivier Y., “Partial commutation and traces”, Handbook of formal languages, 3, 1997, 457–533.Diekert V., Metivier Y., “Partial commutation and traces”, Handbook of formal languages, 3, 1997, 457–533.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.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.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.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.Griffiths T., “The unsolvability of the equivalence problem for ε-free nondeterministic generalized machines”, J. of the ACM, 15 (1968), 409–413.Griffiths T., “The unsolvability of the equivalence problem for ε-free nondeterministic generalized machines”, J. of the ACM, 15 (1968), 409–413.Mohri M., “Finite-state transducers in language and speech processing”, Comput. Ling, 23:2 (1997), 269–311.Mohri M., “Finite-state transducers in language and speech processing”, Comput. Ling, 23:2 (1997), 269–311.Mohri M., “Minimization algorithms for sequential transducers”, Theor. Comput. Sci., 234 (2000), 177–201.Mohri M., “Minimization algorithms for sequential transducers”, Theor. Comput. Sci., 234 (2000), 177–201.Reutenauer C., Schuzenberger M. P., “Minimization of rational word functions”, SIAM J. of Comput., 20:4 (1991), 6699685.Reutenauer C., Schuzenberger M. P., “Minimization of rational word functions”, SIAM J. of Comput., 20:4 (1991), 6699685.Shofrutt C., “Minimizing subsequential transducers: a survey”, Theor. Comput. Sci., 292:1 (2003), 1311143.Shofrutt C., “Minimizing subsequential transducers: a survey”, Theor. Comput. Sci., 292:1 (2003), 1311143.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.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.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.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.Watson B. W., “A taxonomy of finite automata minimization algorithm”, Computing Science Report. Eindhoven University of Technology, 93/44 (2005), 1–32.Watson B. W., “A taxonomy of finite automata minimization algorithm”, Computing Science Report. Eindhoven University of Technology, 93/44 (2005), 1–32.Weber A., “Decomposing finite-valued transducers and deciding their equivalence”, SIAM Journal on Computing, 22:1 (1993), 175–202.Weber A., “Decomposing finite-valued transducers and deciding their equivalence”, SIAM Journal on Computing, 22:1 (1993), 175–202.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.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.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.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.Захаров В. А., Подымов В. В., “Применение алгоритмов проверки эквивалентности для оптимизации программ”, Труды Института системного программирования, 27:3 (2015), 145–174.Zakharov V. A., Podymov V. V., “Primenenije algoritmov proverki ekvivalentnisti dlya optimizacii program”, Trudy insituta sistemnogo programmirovaniya, 27:3 (2015), 145–174, (in Russian).

The authors declare that there are no conflicts of interest present.