Preview

Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS)

Advanced search

Modeling and analysis of the behavior of successive reactive programs

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

Abstract

Finite state transducers extend the finite state automata to model functions on strings or lists. They may be used also as simple models of sequential reactive programs. These programs operate in the interaction with the environment permanently receiving data (requests) from it. At receiving a piece of data such program performs a sequence of actions. When certain control points are achieved a program outputs the current results of computation as a response. It is significant that different sequences of actions may yield the same result. Therefore, the basic actions of a program may be viewed as generating elements of some appropriate semigroup, and the result of computation may be regarded as the composition of actions performed by the program. This paper offers an alternative technique for the analysis of finite state transducers over semigroups. To check the equivalence of transducers and we associate with them a Labeled Transition Systems . Each path in this LTS represents all possible runs of and on the same input word. Every node of keeps track of the states of and achieved at reading some input word and the deficiency of the output words computed so far. If both transducers reach their final states and the deficiency of their outputs is nonzero then this indicates that and produce different images for the same word, and, hence, they are not equivalent. The nodes of that capture this effect are called rejecting nodes. Thus, the equivalence checking of and is reduced to checking the reachability of rejecting nodes in LTS . We show that one needs to analyze only a bounded fragment of to certify (un)reachability of rejecting nodes. The size of this fragment is polynomial of the size of and if both transducers are deterministic, and single-exponential if they are k-bounded. The same approach is applicable for checking k-valuedness of transducers over semigroups.

About the Author

V. A. Zakharov
Institute for System Programming Russian Academy of Science; Higher School of Economics National Research University
Russian Federation


References

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.


Review

For citations:


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
This work is licensed under a Creative Commons Attribution 4.0 License.


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