Extended symbolic finite automata and transducers

作者: Margus Veanes , Loris D’Antoni

DOI: 10.1007/S10703-015-0233-4

关键词:

摘要: Symbolic finite automata and transducers augment classic with symbolic alphabets represented as parametric theories. This extension enables to succinctly represent large potentially infinite while preserving closure decidability properties. Extended further extend these objects by allowing transitions read consecutive input elements in a single step. In this paper we study the properties of models. contrast case alphabets, show how reading multiple symbols increases expressiveness models, which causes some stop holding most decision problems become undecidable. particular extended are not closed under composition, equivalence problem is undecidable for both transducers. We then introduce subclass Cartesian guards limited conjunctions unary predicates propose an algorithm single-valued case. also present heuristic composing that works many practical cases. Finally, model real world programs use proposed algorithms prove their correctness.

参考文章(27)
Loris D’Antoni, Margus Veanes, Equivalence of Extended Symbolic Finite Transducers Computer Aided Verification. pp. 624- 639 ,(2013) , 10.1007/978-3-642-39799-8_41
Luc Segoufin, Automata and Logics for Words and Trees over an Infinite Alphabet Computer Science Logic. pp. 41- 57 ,(2006) , 10.1007/11874683_3
M. P. Schutzenberger, Sur les relations rationnelles Lecture Notes in Computer Science. pp. 209- 213 ,(1975) , 10.1007/3-540-07407-4_22
Loris D’Antoni, Rajeev Alur, Symbolic Visibly Pushdown Automata computer aided verification. pp. 209- 225 ,(2014) , 10.1007/978-3-319-08867-9_14
Karel Culik, Juhani Karhumäki, The Equivalence of Finite Valued Transducers (on HDTOL Languages) is Decidable mathematical foundations of computer science. ,vol. 47, pp. 264- 272 ,(1986) , 10.1007/BFB0016250
Pieter Hooimeijer, Margus Veanes, David Molnar, Prateek Saxena, Benjamin Livshits, Fast and precise sanitizer analysis with BEK usenix security symposium. pp. 1- 1 ,(2011)
Andreas Maletti, Jonathan Graehl, Mark Hopkins, Kevin Knight, The Power of Extended Top-Down Tree Transducers SIAM Journal on Computing. ,vol. 39, pp. 410- 430 ,(2009) , 10.1137/070699160
BRUCE W. WATSON, Implementing and using finite automata toolkits Natural Language Engineering. ,vol. 2, pp. 295- 302 ,(1996) , 10.1017/S135132499700154X