{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:10:36Z","timestamp":1771024236228,"version":"3.50.1"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2009,5,1]],"date-time":"2009-05-01T00:00:00Z","timestamp":1241136000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000183","name":"Army Research Office","doi-asserted-by":"publisher","award":["DAAD19-01-0473"],"award-info":[{"award-number":["DAAD19-01-0473"]}],"id":[{"id":"10.13039\/100000183","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCR-0306382CPA-0541149"],"award-info":[{"award-number":["CCR-0306382CPA-0541149"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2009,5]]},"abstract":"<jats:p>\n            We propose the model of\n            <jats:italic>nested words<\/jats:italic>\n            for representation of data with both a linear ordering and a hierarchically nested matching of items. Examples of data with such dual linear-hierarchical structure include executions of structured programs, annotated linguistic data, and HTML\/XML documents. Nested words generalize both words and ordered trees, and allow both word and tree operations. We define\n            <jats:italic>nested word automata<\/jats:italic>\n            \u2014finite-state acceptors for nested words, and show that the resulting class of regular languages of nested words has all the appealing theoretical properties that the classical regular word languages enjoys: deterministic nested word automata are as expressive as their nondeterministic counterparts; the class is closed under union, intersection, complementation, concatenation, Kleene-*, prefixes, and language homomorphisms; membership, emptiness, language inclusion, and language equivalence are all decidable; and definability in monadic second order logic corresponds exactly to finite-state recognizability. We also consider regular languages of infinite nested words and show that the closure properties, MSO-characterization, and decidability of decision problems carry over.\n          <\/jats:p>\n          <jats:p>\n            The linear encodings of nested words give the class of\n            <jats:italic>visibly pushdown languages<\/jats:italic>\n            of words, and this class lies between balanced languages and deterministic context-free languages. We argue that for algorithmic verification of structured programs, instead of viewing the program as a context-free language over words, one should view it as a regular language of nested words (or equivalently, a visibly pushdown language), and this would allow model checking of many properties (such as stack inspection, pre-post conditions) that are not expressible in existing specification logics.\n          <\/jats:p>\n          <jats:p>We also study the relationship between ordered trees and nested words, and the corresponding automata: while the analysis complexity of nested word automata is the same as that of classical tree automata, they combine both bottom-up and top-down traversals, and enjoy expressiveness and succinctness benefits over tree automata.<\/jats:p>","DOI":"10.1145\/1516512.1516518","type":"journal-article","created":{"date-parts":[[2009,5,19]],"date-time":"2009-05-19T16:47:42Z","timestamp":1242751662000},"page":"1-43","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":227,"title":["Adding nesting structure to words"],"prefix":"10.1145","volume":"56","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, Pennsylvania"}]},{"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, Illinois"}]}],"member":"320","published-online":{"date-parts":[[2009,5,19]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1265530.1265564"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1075382.1075387"},{"key":"e_1_2_2_3_1","volume-title":"TACAS'04: Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Software. Lecture Notes in Computer Science","volume":"2988","author":"Alur R.","unstructured":"Alur , R. , Etessami , K. , and Madhusudan , P . 2004. A temporal logic of nested calls and returns . In TACAS'04: Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Software. Lecture Notes in Computer Science , vol. 2988 , Springer-Verlag, Berlin, Germany, 467--481. Alur, R., Etessami, K., and Madhusudan, P. 2004. A temporal logic of nested calls and returns. In TACAS'04: Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Software. Lecture Notes in Computer Science, vol. 2988, Springer-Verlag, Berlin, Germany, 467--481."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_89"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007352.1007390"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11779148_1"},{"key":"e_1_2_2_7_1","doi-asserted-by":"crossref","unstructured":"Autebert J. Berstel J. and Boasson L. 1997. Context-free languages and pushdown automata. In Handbook of Formal Languages. Vol. 1. Springer 111--174.   Autebert J. Berstel J. and Boasson L. 1997. Context-free languages and pushdown automata. In Handbook of Formal Languages. Vol. 1. Springer 111--174.","DOI":"10.1007\/978-3-642-59136-5_3"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_2_2_9_1","series-title":"Lecture Notes in Computer Science","volume-title":"Bebop: A symbolic model checker for boolean programs. In Proceedings of the SPIN 2000 Workshop on Model Checking of Software","author":"Ball T.","year":"2000","unstructured":"Ball , T. , and Rajamani , S . 2000 . Bebop: A symbolic model checker for boolean programs. In Proceedings of the SPIN 2000 Workshop on Model Checking of Software . Lecture Notes in Computer Science , vol. 1885 , Springer-Verlag , Berlin, Germany , 113--130. Ball, T., and Rajamani, S. 2000. Bebop: A symbolic model checker for boolean programs. In Proceedings of the SPIN 2000 Workshop on Model Checking of Software. Lecture Notes in Computer Science, vol. 1885, Springer-Verlag, Berlin, Germany, 113--130."},{"key":"e_1_2_2_10_1","volume-title":"Lecture Notes in Computer Science","volume":"2300","author":"Berstel J.","unstructured":"Berstel , J. , and Boasson , L . 2002. Balanced grammars and their languages. In Formal and Natural Computing: Essays Dedicated to Grzegorz Rozenberg . Lecture Notes in Computer Science , vol. 2300 , Springer-Verlag, Berlin, Germany, 3--25. Berstel, J., and Boasson, L. 2002. Balanced grammars and their languages. In Formal and Natural Computing: Essays Dedicated to Grzegorz Rozenberg. Lecture Notes in Computer Science, vol. 2300, Springer-Verlag, Berlin, Germany, 3--25."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDE.2006.48"},{"key":"e_1_2_2_12_1","volume-title":"CONCUR'97: Proceedings of the 8th International Conference on Concurrency Theory. Lecture Notes in Computer Science","volume":"1243","author":"Boujjani A.","unstructured":"Boujjani , A. , Esparza , J. , and Maler , O . 1997. Reachability analysis of pushdown automata: Applications to model checking . In CONCUR'97: Proceedings of the 8th International Conference on Concurrency Theory. Lecture Notes in Computer Science , vol. 1243 , Springer-Verlag, Berlin, Germany, 135--150. Boujjani, A., Esparza, J., and Maler, O. 1997. Reachability analysis of pushdown automata: Applications to model checking. In CONCUR'97: Proceedings of the 8th International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 1243, Springer-Verlag, Berlin, Germany, 135--150."},{"key":"e_1_2_2_13_1","volume-title":"FSTTCS 2003: Proceedings of the 23rd International Conference on Foundations of Software Technology and Theoretical Computer Science. Lecture Notes in Computer Science","volume":"2914","author":"Bouquet A.","unstructured":"Bouquet , A. , Serre , O. , and Walukiewicz , I . 2003. Pushdown games with unboundedness and regular conditions . In FSTTCS 2003: Proceedings of the 23rd International Conference on Foundations of Software Technology and Theoretical Computer Science. Lecture Notes in Computer Science , vol. 2914 , Springer-Verlag, Berlin, Germany, 88--99. Bouquet, A., Serre, O., and Walukiewicz, I. 2003. Pushdown games with unboundedness and regular conditions. In FSTTCS 2003: Proceedings of the 23rd International Conference on Foundations of Software Technology and Theoretical Computer Science. Lecture Notes in Computer Science, vol. 2914, Springer-Verlag, Berlin, Germany, 88--99."},{"key":"e_1_2_2_14_1","volume-title":"Tech. Rep. HKUST-TCSC-2001-0","author":"Br\u00fcggemann-Klein A.","year":"2001","unstructured":"Br\u00fcggemann-Klein , A. , Murata , M. , and Wood , D . 2001 . Regular tree and regular hedge languages over unranked alphabets: Version 1. Tech. Rep. HKUST-TCSC-2001-0 , The Hongkong University of Science and Technology . Br\u00fcggemann-Klein, A., Murata, M., and Wood, D. 2001. Regular tree and regular hedge languages over unranked alphabets: Version 1. Tech. Rep. HKUST-TCSC-2001-0, The Hongkong University of Science and Technology."},{"key":"e_1_2_2_15_1","volume-title":"Proceedings of the Extreme Markup Languages.","author":"Br\u00fcggermann-Klein A.","unstructured":"Br\u00fcggermann-Klein , A. , and Wood , D . 2004. Balanced context-free grammars, hedge grammars and pushdown caterpillar automata . In Proceedings of the Extreme Markup Languages. Br\u00fcggermann-Klein, A., and Wood, D. 2004. Balanced context-free grammars, hedge grammars and pushdown caterpillar automata. In Proceedings of the Extreme Markup Languages."},{"key":"e_1_2_2_16_1","volume-title":"CONCUR'92: Proceedings of the 3rd International Conference on Concurrency Theory. Lecture Notes in Computer Science","volume":"630","author":"Burkart O.","unstructured":"Burkart , O. , and Steffen , B . 1992. Model checking for context-free processes . In CONCUR'92: Proceedings of the 3rd International Conference on Concurrency Theory. Lecture Notes in Computer Science , vol. 630 , Springer-Verlag, Berlin, Germany, 123--137. Burkart, O., and Steffen, B. 1992. Model checking for context-free processes. In CONCUR'92: Proceedings of the 3rd International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 630, Springer-Verlag, Berlin, Germany, 123--137."},{"key":"e_1_2_2_17_1","volume-title":"Proceedings of the 11th Annual Conference of the European Association for Computer Science Logic, CSL 2002. Lecture Notes in Computer Science","volume":"2471","author":"Cachat T.","unstructured":"Cachat , T. , Duparc , J. , and Thomas , W . 2002. Solving pushdown games with a \u03a33 winning condition . In Proceedings of the 11th Annual Conference of the European Association for Computer Science Logic, CSL 2002. Lecture Notes in Computer Science , vol. 2471 , Springer-Verlag, Berlin, Germany, 322--336. Cachat, T., Duparc, J., and Thomas, W. 2002. Solving pushdown games with a \u03a33 winning condition. In Proceedings of the 11th Annual Conference of the European Association for Computer Science Logic, CSL 2002. Lecture Notes in Computer Science, vol. 2471, Springer-Verlag, Berlin, Germany, 322--336."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2004.06.001"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/586110.586142"},{"key":"e_1_2_2_20_1","unstructured":"Comon H. Dauchet M. Gilleron R. Lugiez D. Tison S. and Tommasi M. 2002. Tree automata techniques and applications. Draft Available at http:\/\/www.grappa.univ-lille3.fr\/tata\/.  Comon H. Dauchet M. Gilleron R. Lugiez D. Tison S. and Tommasi M. 2002. Tree automata techniques and applications. Draft Available at http:\/\/www.grappa.univ-lille3.fr\/tata\/."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(88)90148-2"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00139-1"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(67)80003-5"},{"key":"e_1_2_2_24_1","volume-title":"ICDT '03: Proceedings of the 9th International Conference on Database Theory. Lecture Notes in Computer Science","volume":"2572","author":"Green T.","unstructured":"Green , T. , Miklau , G. , Onizuka , M. , and Suciu , D . 2003. Processing XML streams with deterministic automata . In ICDT '03: Proceedings of the 9th International Conference on Database Theory. Lecture Notes in Computer Science , vol. 2572 , Springer-Verlag, Berlin, Germany, 173--189. Green, T., Miklau, G., Onizuka, M., and Suciu, D. 2003. Processing XML streams with deterministic automata. In ICDT '03: Proceedings of the 9th International Conference on Database Theory. Lecture Notes in Computer Science, vol. 2572, Springer-Verlag, Berlin, Germany, 173--189."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/872757.872809"},{"key":"e_1_2_2_26_1","doi-asserted-by":"crossref","unstructured":"Harel D. Kozen D. and Tiuryn J. 2000. Dynamic Logic. MIT Press Cambridge MA.   Harel D. Kozen D. and Tiuryn J. 2000. Dynamic Logic. MIT Press Cambridge MA.","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"e_1_2_2_27_1","volume-title":"CAV 02: Proceedings of the 14th Annual Conference on Computer Aided Verification. Lecture Notes in Computer Science","volume":"2404","author":"Henzinger T.","unstructured":"Henzinger , T. , Jhala , R. , Majumdar , R. , Necula , G. , Sutre , G. , and Weimer , W . 2002. Temporal-safety proofs for systems code . In CAV 02: Proceedings of the 14th Annual Conference on Computer Aided Verification. Lecture Notes in Computer Science , vol. 2404 , Springer-Verlag, Berlin, Germany, 526--538. Henzinger, T., Jhala, R., Majumdar, R., Necula, G., Sutre, G., and Weimer, W. 2002. Temporal-safety proofs for systems code. In CAV 02: Proceedings of the 14th Annual Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 2404, Springer-Verlag, Berlin, Germany, 526--538."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_2_29_1","unstructured":"Hopcroft J. and Ullman J. 1979. Introduction to Automata Theory Languages and Computation. Addison-Wesley Reading MA.   Hopcroft J. and Ullman J. 1979. Introduction to Automata Theory Languages and Computation. Addison-Wesley Reading MA."},{"key":"e_1_2_2_30_1","volume-title":"Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society Press","author":"Jensen T.","unstructured":"Jensen , T. , Metayer , D. L. , and Thorn , T . 1999. Verification of control flow based security properties . In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society Press , Los Alamitos, CA, 89--103. Jensen, T., Metayer, D. L., and Thorn, T. 1999. Verification of control flow based security properties. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society Press, Los Alamitos, CA, 89--103."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(67)90564-5"},{"key":"e_1_2_2_32_1","volume-title":"Proceedings of the 8th International Workshop on Computer Science Logic (CSL 94)","volume":"933","author":"Lautemann A.","unstructured":"Lautemann , A. , Schwentick , T. , and Th\u00e9rien , D . 1994. Logics for context-free languages . In Proceedings of the 8th International Workshop on Computer Science Logic (CSL 94) . Lecture Notes in Computer Science , vol. 933 , Springer-Verlag, New York, 205--216. Lautemann, A., Schwentick, T., and Th\u00e9rien, D. 1994. Logics for context-free languages. In Proceedings of the 8th International Workshop on Computer Science Logic (CSL 94). Lecture Notes in Computer Science, vol. 933, Springer-Verlag, New York, 205--216."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_4"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_34"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/11601524_15"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/321406.321411"},{"key":"e_1_2_2_37_1","volume-title":"Proceedings of the 11th Annual Conference of the European Association for Computer Science Logic CSL","author":"Neven F.","year":"2002","unstructured":"Neven , F. 2002. Automata, logic, and XML . In Proceedings of the 11th Annual Conference of the European Association for Computer Science Logic CSL 2002 . Lecture Notes in Computer Science, vol. 2471 , Springer-Verlag , Berlin, Germany, 2--26. Neven, F. 2002. Automata, logic, and XML. In Proceedings of the 11th Annual Conference of the European Association for Computer Science Logic CSL 2002. Lecture Notes in Computer Science, vol. 2471, Springer-Verlag, Berlin, Germany, 2--26."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2006.10.003"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/543613.543622"},{"key":"e_1_2_2_42_1","unstructured":"Sharir M. and Pnueli A. 1981. Two approaches to inter-procedural data-flow analysis. In Program flow analysis: Theory and applications. Prentice-Hall Englewood Cliffs NJ.  Sharir M. and Pnueli A. 1981. Two approaches to inter-procedural data-flow analysis. In Program flow analysis: Theory and applications. Prentice-Hall Englewood Cliffs NJ."},{"key":"e_1_2_2_43_1","volume-title":"Handbook of Theoretical Computer Science","author":"Thomas W.","unstructured":"Thomas , W. 1990. Automata on infinite objects . In Handbook of Theoretical Computer Science , J. van Leeuwen, Ed. Vol. B. Elsevier Science Publishers , Amsterdam, The Netherlands, 133--191. Thomas, W. 1990. Automata on infinite objects. In Handbook of Theoretical Computer Science, J. van Leeuwen, Ed. Vol. B. Elsevier Science Publishers, Amsterdam, The Netherlands, 133--191."},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1092"},{"key":"e_1_2_2_45_1","volume-title":"Proceedings of the Symposium on Fundamentals of Computation Theory. Lecture Notes in Computer Science","volume":"158","author":"von Braunm\u00fchl B.","unstructured":"von Braunm\u00fchl , B. , and Verbeek , R . 1983. Input-driven languages are recognized in log n space . In Proceedings of the Symposium on Fundamentals of Computation Theory. Lecture Notes in Computer Science , vol. 158 , Springer-Verlag, Berlin, Germany, 40--51. von Braunm\u00fchl, B., and Verbeek, R. 1983. Input-driven languages are recognized in log n space. In Proceedings of the Symposium on Fundamentals of Computation Theory. Lecture Notes in Computer Science, vol. 158, Springer-Verlag, Berlin, Germany, 40--51."}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1516512.1516518","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1516512.1516518","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:30:06Z","timestamp":1750253406000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1516512.1516518"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,5]]},"references-count":45,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,5]]}},"alternative-id":["10.1145\/1516512.1516518"],"URL":"https:\/\/doi.org\/10.1145\/1516512.1516518","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,5]]},"assertion":[{"value":"2007-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-05-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}