×

Symbolic tree automata. (English) Zbl 1317.68103

Summary: We introduce symbolic tree automata as a generalization of finite tree automata with a parametric alphabet over any given background theory. We show that symbolic tree automata are closed under Boolean operations, and that the operations are effectively uniform in the given alphabet theory. This generalizes the corresponding classical properties known for finite tree automata.

MSC:

68Q45 Formal languages and automata

Software:

VATA; MONA; MTBDD; Rex
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Comon, H.; Dauchet, M.; Gilleron, R.; Löding, C.; Jacquemard, F.; Lugiez, D.; Tison, S.; Tommasi, M., Tree automata techniques and applications (2007), release October, 12th 2007
[2] Kaminski, M.; Tan, T., Tree automata over infinite alphabets, (Pillars of Computer Science (2008), Springer), 386-423 · Zbl 1133.68364
[3] Kaminski, M.; Francez, N., Finite-memory automata, (31st Annual Symposium on Foundations of Computer Science, vol. 2. 31st Annual Symposium on Foundations of Computer Science, vol. 2, FOCS 1990 (1990), IEEE), 683-688
[4] David, C.; Libkin, L.; Tan, T., Efficient reasoning about data trees via integer linear programming, (ICDT’11 (2011), ACM), 18-29
[5] Veanes, M.; Bjørner, N.; de Moura, L., Symbolic automata constraint solving, (Fermüller, C.; Voronkov, A., LPAR-17. LPAR-17, LNCS, vol. 6397 (2010), Springer), 640-654 · Zbl 1306.68097
[6] Veanes, M.; Hooimeijer, P.; Livshits, B.; Molnar, D.; Bjorner, N., Symbolic finite state transducers: algorithms and applications, (Proceedings of the Symposium on Principles of Programming Languages. Proceedings of the Symposium on Principles of Programming Languages, POPL’12 (2012)) · Zbl 1321.68341
[7] D’Antoni, L.; Veanes, M., Minimization of symbolic automata, (POPL’14 (2014), ACM), 541-553 · Zbl 1284.68347
[8] Gécseg, F.; Steinby, M., Tree Automata (1984), Akadémiai Kiadó: Akadémiai Kiadó Budapest · Zbl 0396.68041
[9] Hooimeijer, P.; Veanes, M., An evaluation of automata algorithms for string analysis, (VMCAI’11. VMCAI’11, LNCS (2011), Springer) · Zbl 1317.68287
[10] D’Antoni, L.; Veanes, M.; Livshits, B.; Molnar, D., Fast: a transducer-based language for tree manipulation, (PLDI’14 (2014), ACM)
[11] Fast tutorial
[12] Veanes, M.; Bjørner, N., Symbolic tree transducers, (Perspectives of System Informatics. Perspectives of System Informatics, PSI’11 (2011)) · Zbl 1257.68100
[13] Veanes, M.; Bjørner, N., Foundations of finite symbolic tree transducers, (Gurevich, Y., The Logic in Computer Science Column. The Logic in Computer Science Column, Bull. Eur. Assoc. Theor. Comput. Sci., vol. 105 (2011)), 141-173 · Zbl 1257.68100
[14] Fülöp, Z.; Vogler, H., Forward and backward application of symbolic tree transducers, Acta Inform., 51, 5, 297-325 (2014) · Zbl 1307.68047
[15] Watson, B. W., Implementing and using finite automata toolkits, (Extended Finite State Models of Language (1999), Cambridge University Press), 19-36
[16] Noord, G. V.; Gerdemann, D., Finite state transducers with predicates and identities, Grammars, 4, 263-286 (2001) · Zbl 1015.68087
[17] Bés, A., An application of the Feferman-Vaught theorem to automata and logics for words over an infinite alphabet, Log. Methods Comput. Sci., 4, 1-23 (2008) · Zbl 1149.03014
[18] Veanes, M.; de Halleux, P.; Tillmann, N., Rex: symbolic regular expression explorer, (Third International Conference on Software Testing, Verification and Validation. Third International Conference on Software Testing, Verification and Validation, ICST’10 (2010), IEEE)
[19] Segoufin, L., Automata and logics for words and trees over an infinite alphabet, (Ésik, Z., CSL. CSL, LNCS, vol. 4207 (2006)), 41-57 · Zbl 1225.68103
[20] Neven, F.; Schwentick, T.; Vianu, V., Finite state machines for strings over infinite alphabets, ACM Trans. Comput. Log., 5, 403-435 (2004) · Zbl 1367.68175
[21] Bojańczyk, M.; Muscholl, A.; Schwentick, T.; Segoufin, L.; David, C., Two-variable logic on words with data, (LICS 2006 (2006), IEEE), 7-16
[22] Bojańczyk, M.; Klin, B.; Lasota, S., Automata with group actions, (26th Annual IEEE Symposium on Logic in Computer Science (2011), IEEE), 355-364
[23] Henriksen, J.; Jensen, J.; Jørgensen, M.; Klarlund, N.; Paige, B.; Rauhe, T.; Sandholm, A., Mona: monadic second-order logic in practice, (Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop. Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop, TACAS ’95. Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop. Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop, TACAS ’95, LNCS, vol. 1019 (1995))
[24] Klarlund, N.; Møller, A.; Schwartzbach, M. I., MONA implementation secrets, Int. J. Found. Comput. Sci., 13, 4, 571-586 (2002) · Zbl 1066.68079
[25] Lengal, O.; Šimáček, J.; Vojnar, T., Vata: a library for efficient manipulation of non-deterministic tree automata, (TACAS’12. TACAS’12, LNCS, vol. 7214 (2012), Springer), 79-94 · Zbl 1352.68135
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.