{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T01:40:00Z","timestamp":1750556400934,"version":"3.41.0"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319633893"},{"type":"electronic","value":"9783319633909"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63390-9_10","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:50Z","timestamp":1499849630000},"page":"176-196","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Minimization of Symbolic Transducers"],"prefix":"10.1007","author":[{"given":"Olli","family":"Saarikivi","sequence":"first","affiliation":[]},{"given":"Margus","family":"Veanes","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"10_CR1","unstructured":"Automata library. https:\/\/github.com\/AutomataDotNet\/Automata"},{"key":"10_CR2","unstructured":"Emoticons, Unicode standard v9.0. http:\/\/unicode.org\/charts\/PDF\/U1F600.pdf"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/11605157_3","volume-title":"Implementation and Application of Automata","author":"PA Abdulla","year":"2006","unstructured":"Abdulla, P.A., Deneux, J., Kaati, L., Nilsson, M.: Minimization of non-deterministic automata with large alphabets. In: Farr\u00e9, J., Litovsky, I., Schmitz, S. (eds.) CIAA 2005. LNCS, vol. 3845, pp. 31\u201342. Springer, Heidelberg (2006). doi:10.1007\/11605157_3"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-540-70844-5_22","volume-title":"Implementation and Applications of Automata","author":"PA Abdulla","year":"2008","unstructured":"Abdulla, P.A., Bouajjani, A., Hol\u00edk, L., Kaati, L., Vojnar, T.: Composed bisimulation for tree automata. In: Ibarra, O.H., Ravikumar, B. (eds.) CIAA 2008. LNCS, vol. 5148, pp. 212\u2013222. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-70844-5_22"},{"key":"10_CR5","volume-title":"Compilers: Principles, Techniques, and Tools","author":"AV Aho","year":"2006","unstructured":"Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools, 2nd edn. Addison-Wesley, Boston (2006)","edition":"2"},{"issue":"6","key":"10_CR6","doi-asserted-by":"publisher","first-page":"983","DOI":"10.1142\/S0129054103002126","volume":"14","author":"C Allauzen","year":"2003","unstructured":"Allauzen, C., Mohri, M.: Finitely subsequential transducers. Int. J. Found. Comput. Sci. 14(6), 983\u2013994 (2003)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1007\/978-3-662-49674-9_46","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Almeida","year":"2016","unstructured":"Almeida, R., Hol\u00edk, L., Mayr, R.: Reduction of nondeterministic tree automata. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 717\u2013735. Springer, Heidelberg (2016). doi:10.1007\/978-3-662-49674-9_46"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-642-39212-2_7","volume-title":"Automata, Languages, and Programming","author":"R Alur","year":"2013","unstructured":"Alur, R., Raghothaman, M.: Decision problems for additive regular functions. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013. LNCS, vol. 7966, pp. 37\u201348. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39212-2_7"},{"issue":"1","key":"10_CR9","first-page":"599","volume":"46","author":"R Alur","year":"2011","unstructured":"Alur, R., \u010cern\u00fd, P.: Streaming transducers for algorithmic verification of single-pass list-processing programs. SIGPLAN Not. - POPL 2011 46(1), 599\u2013610 (2011)","journal-title":"SIGPLAN Not. - POPL 2011"},{"key":"10_CR10","unstructured":"Baschenis, F., Gauwin, O., Muscholl, A., Puppis, G.: Minimizing resources of sweeping and streaming string transducers. In: 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). LIPIcs, vol. 55, pp. 114:1\u2013114:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)"},{"issue":"9","key":"10_CR11","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1109\/12.537122","volume":"45","author":"B Bollig","year":"1996","unstructured":"Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput. 45(9), 993\u20131002 (1996)","journal-title":"IEEE Trans. Comput."},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-18275-4_7"},{"issue":"1","key":"10_CR13","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/j.jcss.2010.06.011","volume":"77","author":"D Buchfuhrer","year":"2011","unstructured":"Buchfuhrer, D., Umans, C.: The complexity of Boolean formula minimization. J. Comput. Syst. Sci. 77(1), 142\u2013153 (2011)","journal-title":"J. Comput. Syst. Sci."},{"key":"10_CR14","unstructured":"Choffrut, C.: Contribution \u00e0 l\u2019\u00e9tude de quelques familles remarquables de fonctions rationnelles. Ph.D. thesis, Universit Paris 7, Paris, France (1978)"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Colcombet, T., Fradet, P.: Enforcing trace properties by program transformation. In: Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2000), pp. 54\u201366. ACM (2000)","DOI":"10.1145\/325694.325703"},{"issue":"1","key":"10_CR16","first-page":"329","volume":"50","author":"M Dalla Preda","year":"2015","unstructured":"Dalla Preda, M., Giacobazzi, R., Lakhotia, A., Mastroeni, I.: Abstract symbolic automata: mixed syntactic\/semantic similarity analysis of executables. SIGPLAN Not. - POPL 2015 50(1), 329\u2013341 (2015)","journal-title":"SIGPLAN Not. - POPL 2015"},{"issue":"1","key":"10_CR17","first-page":"541","volume":"49","author":"L D\u2019Antoni","year":"2014","unstructured":"D\u2019Antoni, L., Veanes, M.: Minimization of symbolic automata. SIGPLAN Not. - POPL 2014 49(1), 541\u2013553 (2014)","journal-title":"SIGPLAN Not. - POPL 2014"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1007\/978-3-662-54577-5_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems 7","author":"L D\u2019Antoni","year":"2017","unstructured":"D\u2019Antoni, L., Veanes, M.: Forward bisimulations for nondeterministic symbolic finite automata. In: Legay, A., Margaria, T. (eds.) TACAS 201. LNCS, vol. 10205, pp. 518\u2013534. Springer, Heidelberg (2017). doi:10.1007\/978-3-662-54577-5_30"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Daviaud, L., Reynier, P.-A., Talbot, J.-M.: A generalised twinning property for minimisation of cost register automata. In: Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS 2016), pp. 857\u2013866. ACM (2016)","DOI":"10.1145\/2933575.2934549"},{"key":"10_CR20","unstructured":"Drobac, S., Lind\u00e9n, K., Pirinen, T., Silfverberg, M.: Heuristic hyper-minimization of finite state lexicons. In: Proceedings of the Ninth International Conference on Language Resources and Evaluation (LREC 2014). ELRA (2014)"},{"key":"10_CR21","series-title":"IISc Research Monographs Series","volume-title":"Modern Applications of Automata Theory","year":"2012","unstructured":"D\u2019Souza, D., Shankar, P. (eds.): Modern Applications of Automata Theory. IISc Research Monographs Series, vol. 2. World Scientific, Singapore (2012)"},{"issue":"5","key":"10_CR22","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/s00236-014-0197-7","volume":"51","author":"Z F\u00fcl\u00f6p","year":"2014","unstructured":"F\u00fcl\u00f6p, Z., Vogler, H.: Forward and backward application of symbolic tree transducers. Acta Informatica 51(5), 297\u2013325 (2014)","journal-title":"Acta Informatica"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-60630-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JG Henriksen","year":"1995","unstructured":"Henriksen, J.G., Jensen, J., J\u00f8rgensen, M., Klarlund, N., Paige, R., Rauhe, T., Sandholm, A.: Mona: monadic second-order logic in practice. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 89\u2013110. Springer, Heidelberg (1995). doi:10.1007\/3-540-60630-0_5"},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-540-76336-9_12","volume-title":"Implementation and Application of Automata","author":"J H\u00f6gberg","year":"2007","unstructured":"H\u00f6gberg, J., Maletti, A., May, J.: Backward and forward bisimulation minimisation of tree automata. In: Holub, J., \u017dd\u2019\u00e1rek, J. (eds.) CIAA 2007. LNCS, vol. 4783, pp. 109\u2013121. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-76336-9_12"},{"key":"10_CR25","unstructured":"Hooimeijer, P., Livshits, B., Molnar, D., Saxena, P., Veanes, M.: Fast and precise sanitizer analysis with Bek. In: Proceedings of the 20th USENIX Conference on Security (SEC 2011). USENIX Association (2011)"},{"issue":"9","key":"10_CR26","doi-asserted-by":"publisher","first-page":"1098","DOI":"10.1109\/JRPROC.1952.273898","volume":"40","author":"DA Huffman","year":"1952","unstructured":"Huffman, D.A.: A method for the construction of minimum-redundancy codes. Proc. IRE 40(9), 1098\u20131101 (1952)","journal-title":"Proc. IRE"},{"issue":"4","key":"10_CR27","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1142\/S012905410200128X","volume":"13","author":"N Klarlund","year":"2002","unstructured":"Klarlund, N., M\u00f8ller, A., Schwartzbach, M.I.: MONA implementation secrets. Int. J. Found. Comput. Sci. 13(4), 571\u2013586 (2002)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Manuel, A., Ramanujam, R.: Automata over infinite alphabets. In: D\u2019Souza, D., Shankar, P. (eds.) Modern Applications of Automata Theory, pp. 529\u2013554. World Scientific (2012)","DOI":"10.1142\/9789814271059_0017"},{"issue":"1","key":"10_CR29","first-page":"63","volume":"48","author":"R Mayr","year":"2013","unstructured":"Mayr, R., Clemente, L.: Advanced automata minimization. SIGPLAN Not. - POPL 2013 48(1), 63\u201374 (2013)","journal-title":"SIGPLAN Not. - POPL 2013"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Mesfar, S., Silberztein, M.: Transducer minimization and information compression for NooJ dictionaries. In: Proceedings of the 2009 Conference on Finite-State Methods and Natural Language Processing (FSMNLP 2008), pp. 110\u2013121. IOS Press (2009)","DOI":"10.3233\/978-1-58603-975-2-110"},{"key":"10_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/3-540-58094-8_14","volume-title":"Combinatorial Pattern Matching","author":"M Mohri","year":"1994","unstructured":"Mohri, M.: Minimization of sequential transducers. In: Crochemore, M., Gusfield, D. (eds.) CPM 1994. LNCS, vol. 807, pp. 151\u2013163. Springer, Heidelberg (1994). doi:10.1007\/3-540-58094-8_14"},{"issue":"2","key":"10_CR32","first-page":"269","volume":"23","author":"M Mohri","year":"1997","unstructured":"Mohri, M.: Finite-state transducers in language and speech processing. Comput. Linguist. 23(2), 269\u2013311 (1997)","journal-title":"Comput. Linguist."},{"issue":"1\u20132","key":"10_CR33","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0304-3975(98)00115-7","volume":"234","author":"M Mohri","year":"2000","unstructured":"Mohri, M.: Minimization algorithms for sequential transducers. Theoret. Comput. Sci. 234(1\u20132), 177\u2013201 (2000)","journal-title":"Theoret. Comput. Sci."},{"issue":"13","key":"10_CR34","doi-asserted-by":"publisher","first-page":"1367","DOI":"10.14778\/2733004.2733009","volume":"7","author":"M Poess","year":"2014","unstructured":"Poess, M., Rabl, T., Jacobsen, H.-A., Caufield, B.: TPC-DI: the first industry benchmark for data integration. Proc. VLDB Endowment 7(13), 1367\u20131378 (2014)","journal-title":"Proc. VLDB Endowment"},{"key":"10_CR35","doi-asserted-by":"crossref","unstructured":"Saarikivi, O., Veanes, M., Mytkowicz, T., Musuvathi, M.: Fusing effectful comprehensions. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). ACM (2017)","DOI":"10.1145\/3062341.3062362"},{"key":"10_CR36","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0304-3975(77)90055-X","volume":"4","author":"MP Sch\u00fctzenberger","year":"1977","unstructured":"Sch\u00fctzenberger, M.P.: Sur une variante des fonctions s\u00e9quentielles. Theoret. Comput. Sci. 4, 47\u201357 (1977)","journal-title":"Theoret. Comput. Sci."},{"issue":"3","key":"10_CR37","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1012291501330","volume":"4","author":"G van Noord","year":"2001","unstructured":"van Noord, G., Gerdemann, D.: Finite state transducers with predicates and identities. Grammars 4(3), 263\u2013286 (2001)","journal-title":"Grammars"},{"key":"10_CR38","doi-asserted-by":"crossref","unstructured":"Veanes, M., de Halleux, P., Tillmann, N.: Rex: symbolic regular expression explorer. In: Proceedings of the 2010 Third International Conference on Software Testing, Verification and Validation (ICST 2010), pp. 498\u2013507. IEEE (2010)","DOI":"10.1109\/ICST.2010.15"},{"issue":"1","key":"10_CR39","first-page":"137","volume":"47","author":"M Veanes","year":"2012","unstructured":"Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., Bjorner, N.: Symbolic finite state transducers: algorithms and applications. SIGPLAN Not. - POPL 2012 47(1), 137\u2013150 (2012)","journal-title":"SIGPLAN Not. - POPL 2012"},{"issue":"1","key":"10_CR40","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1145\/2775051.2677014","volume":"50","author":"M Veanes","year":"2015","unstructured":"Veanes, M., Mytkowicz, T., Molnar, D., Livshits, B.: Data-parallel string-manipulating programs. SIGPLAN Not. - POPL2015 50(1), 139\u2013152 (2015)","journal-title":"SIGPLAN Not. - POPL2015"},{"key":"10_CR41","unstructured":"Watson, B.W.: Implementing and using finite automata toolkits. In: Extended Finite State Models of Language, pp. 19\u201336. Cambridge University Press (1999)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63390-9_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T01:07:27Z","timestamp":1750554447000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63390-9_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633893","9783319633909"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63390-9_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}