Preview

Труды Института системного программирования РАН

Расширенный поиск

Моделирование и анализ поведения последовательных реагирующих программ

https://doi.org/10.15514/ISPRAS-2015-27(2)-13

Аннотация

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

Об авторе

В. А. Захаров
ИСП РАН; НИУ ВШЭ
Россия


Список литературы

1. Aho A.V., Hopcroft J.E., Ullman J.D. The design and analysis of computer algorithms. Addison-Wesley, Reading, MA, 1974.

2. Aho A.V., Sethi R., Ullman J.D. Compilers: principles, techniques, and tools. Addison-Wesley, Reading, MA, 1986.

3. Alur R., Cerny P. Streaming transducers for algorithmic verification of single-pass list-processing programs. Proceedings of 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 2011, p. 599-610.

4. Blattner M, Head T. Single-valued a-transducers. Journal of Computer and System Sciences, 1977, v. 15, p. 310-327.

5. Blattner M, Head T. The decidability of equivalence for deterministic finite transducers. Journal of Computer and System Sciences, 1979, v. 19, p. 45-49.

6. Beal M.-P., Carton O., Prieur C., Sakarovitch J. Squaring transducers: an efficient procedure for deciding functionality and sequentiality. Theoretical Computer Science, 2003, v. 292.

7. Culik K., Karhumaki J. The equivalence of finite-valued transducers (on HDTOL languages) is decidable. Theoretical Computer Science, 1986, v. 47, p. 71-84.

8. Fischer P.C., Rosenberg A.L. Multi-tape one-way nonwriting automata. Journal of Computer and System Sciences, 1968, v. 2, p. 88-101.

9. Griffiths T. The unsolvability of the equivalence problem for -free nondeterministic generalized machines. Journal of the ACM, 1968, v. 15, p.409-413.

10. Gurari, E., Ibarra, O. A note on finite-valued and finitely ambiguous transducers. Mathematical Systems Theory, 1983, v. 16, p. 61-66.

11. Ibarra O. The unsolvability of the equivalence problem for Efree NGSM's with unary input (output) alphabet and applications. SIAM Journal on Computing, 1978, v. 4.

12. Malcev, A. I. Uber die Einbettung von assoziativen Systemen. Gruppen, Rec. Math. (Mat. Sbornik) N.S., 1939, v. 6, p. 331-336.

13. Malcev, A. I. Uber die Einbettung von assoziativen Systemen. Gruppen. II, Rec. Math. (Mat. Sbornik) N.S., 1940, v. 8, p. 251-264.

14. Mohri M. Finite state transducers in language and speech processing. Computer Linguistics, 1997, v. 23, N 2.

15. Mohri M. Minimization algorithms for sequential transducers. Theoretical Computer Science, 2000, v. 234, p. 177-201.

16. Nerode A., Kohn W. Models for hybrid systems: automata, topology, controllability, observability. Cornell University, Technical Report 93-28, 1993, MIT Press, Cambridge.

17. Sakarovitch J., de Souza R. On the decomposition of k-valued rational relations. Proceedings of 25th International Symposium on Theoretical Aspects of Computer Science, 2008, p.621-632.

18. Sakarovitch J., de Souza R. On the decidability of bounded valuedness for transducers. Proceedings of the 33rd International Symposium on Mathematical Foundations of Computer Science, 2008, p. 588-600.

19. Schutzenberger M. P. Sur les relations rationnelles. Proceedings of Conference on Automata Theory and Formal Languages, 1975, p. 209-213.

20. de Souza R. On the decidability of the equivalence for k-valued transducers. Proceedings of 12th International Conference on Developments in Language Theory, 2008, p. 252-263.

21. Veanes M., Hooimeijer P., Livshits B., et al. Symbolic finite state transducers: algorithms and applications. Proceedings of the 39th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 2012.

22. Weber A. On the valuedness of finite transducers. Acta Informatica, 1989, v. 27, p. 749-780.

23. Weber A. Decomposing finite-valued transducers and deciding their equivalence. SIAM Journal on Computing, 1993, v. 22, p. 175-202.

24. Zakharov V.A. An efficient and unified approach to the decidability of equivalence of propositional program schemes. Proceedings of the 25th International Colloquium ''Automata, Languages and Programming'', 1998, p. 247-258.


Рецензия

Для цитирования:


Захаров В.А. Моделирование и анализ поведения последовательных реагирующих программ. Труды Института системного программирования РАН. 2015;27(2):221-250. https://doi.org/10.15514/ISPRAS-2015-27(2)-13

For citation:


Zakharov V.A. Modeling and analysis of the behavior of successive reactive programs. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2015;27(2):221-250. (In Russ.) https://doi.org/10.15514/ISPRAS-2015-27(2)-13



Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)