{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T21:38:35Z","timestamp":1791409115408,"version":"4.3.3"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"4","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Inf. Syst."],"published-print":{"date-parts":[[2006,10]]},"abstract":"<jats:p>XPath is the standard language for navigating XML documents and returning a set of matching nodes. We present a sound and complete decision procedure for containment of XPath queries, as well as other related XPath decision problems such as satisfiability, equivalence, overlap, and coverage. The considered XPath fragment covers most of the language features used in practice. Specifically, we propose a unifying logic for XML, namely, the alternation-free modal \u03bc-calculus with converse. We show how to translate major XML concepts such as XPath and regular XML types (including DTDs) into this logic. Based on these embeddings, we show how XPath decision problems, in the presence or absence of XML types, can be solved using a decision procedure for \u03bc-calculus satisfiability. We provide a complexity analysis of our system together with practical experiments to illustrate the efficiency of the approach for realistic scenarios.<\/jats:p>","DOI":"10.1145\/1185877.1185882","type":"journal-article","created":{"date-parts":[[2007,1,16]],"date-time":"2007-01-16T19:38:29Z","timestamp":1168976309000},"page":"475-502","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":35,"title":["A system for the static analysis of XPath"],"prefix":"10.1145","volume":"24","author":[{"given":"Pierre","family":"Genev\u00e8s","sequence":"first","affiliation":[{"name":"INRIA Rh\u00f4ne-Alpes, St Ismier Cedex, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nabil","family":"Laya\u00efda","sequence":"additional","affiliation":[{"name":"INRIA Rh\u00f4ne-Alpes, St Ismier Cedex, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2006,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1999.1627"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","first-page":"115","DOI":"10.3166\/jancl.15.115-135","article-title":"PDL for ordered trees","volume":"15","author":"Afanasiev L.","year":"2005","unstructured":"Afanasiev , L. , Blackburn , P. , Dimitriou , I. , Gaiffe , B. , Goris , E. , Marx , M. , and de Rijke , M. 2005 . PDL for ordered trees . J. Appl. Non-Classical Logics 15 , 2, 115 -- 135 .]] Afanasiev, L., Blackburn, P., Dimitriou, I., Gaiffe, B., Goris, E., Marx, M., and de Rijke, M. 2005. PDL for ordered trees. J. Appl. Non-Classical Logics 15, 2, 115--135.]]","journal-title":"J. Appl. Non-Classical Logics"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/376284.375730"},{"key":"e_1_2_1_4_1","unstructured":"Arnold A. and Niwinski D. 1992. Fixed point characterization of weak monadic logic definable sets of trees. In Tree Automata and Languages. North-Holland Amsterdam Netherlands. 159--188.]]  Arnold A. and Niwinski D. 1992. Fixed point characterization of weak monadic logic definable sets of trees. In Tree Automata and Languages. North-Holland Amsterdam Netherlands. 159--188.]]"},{"key":"e_1_2_1_5_1","volume-title":"IJCAR '01: Proceedings of the 1st International Joint Conference on Automated Reasoning. Springer-Verlag","author":"Baader F.","unstructured":"Baader , F. and Tobies , S . 2001. The inverse method implements the automata approach for modal satisfiability . In IJCAR '01: Proceedings of the 1st International Joint Conference on Automated Reasoning. Springer-Verlag , London. 92--106.]] Baader, F. and Tobies, S. 2001. The inverse method implements the automata approach for modal satisfiability. In IJCAR '01: Proceedings of the 1st International Joint Conference on Automated Reasoning. Springer-Verlag, London. 92--106.]]"},{"key":"e_1_2_1_6_1","volume-title":"LICS: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society","author":"Barcel\u00f3 P.","year":"2005","unstructured":"Barcel\u00f3 , P. and Libkin , L . 2005. Temporal logics over unranked trees . In LICS: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society , New York. 31--40.]] 10.1109\/LICS. 2005 .51 Barcel\u00f3, P. and Libkin, L. 2005. Temporal logics over unranked trees. In LICS: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, New York. 31--40.]] 10.1109\/LICS.2005.51"},{"key":"e_1_2_1_7_1","volume-title":"PODS: Proceedings of the 24th ACM Symposium on Principles of Database Systems. ACM","author":"Benedikt M.","unstructured":"Benedikt , M. , Fan , W. , and Geerts , F . 2005. XPath satisfiability in the presence of DTDs . In PODS: Proceedings of the 24th ACM Symposium on Principles of Database Systems. ACM , New York. 25--36.]] 10.1145\/1065167.1065172 Benedikt, M., Fan, W., and Geerts, F. 2005. XPath satisfiability in the presence of DTDs. In PODS: Proceedings of the 24th ACM Symposium on Principles of Database Systems. ACM, New York. 25--36.]] 10.1145\/1065167.1065172"},{"key":"e_1_2_1_8_1","volume-title":"STACS: Proceedings of the 22nd Annual Symposium on Theoretical Aspects of Computer Science. Lcture Notes in Computer Science","volume":"3404","author":"Benedikt M.","year":"1856","unstructured":"Benedikt , M. and Segoufin , L . 2005. Regular tree languages definable in FO . In STACS: Proceedings of the 22nd Annual Symposium on Theoretical Aspects of Computer Science. Lcture Notes in Computer Science vol. 3404 . Springer-Verlag. 327--339.]] 10.1007\/978-3-540-3 1856 -9_27 Benedikt, M. and Segoufin, L. 2005. Regular tree languages definable in FO. In STACS: Proceedings of the 22nd Annual Symposium on Theoretical Aspects of Computer Science. Lcture Notes in Computer Science vol. 3404. Springer-Verlag. 327--339.]] 10.1007\/978-3-540-31856-9_27"},{"key":"e_1_2_1_9_1","unstructured":"Berglund A. Boag S. Chamberlin D. Fern\u00e1ndez M. F. Kay M. Robie J. and Sim\u00e9on J. 2006. XML path language (XPath) 2.0 W3C candidate recommendation. http:\/\/www.w3.org\/TR\/xpath20\/.]]  Berglund A. Boag S. Chamberlin D. Fern\u00e1ndez M. F. Kay M. Robie J. and Sim\u00e9on J. 2006. XML path language (XPath) 2.0 W3C candidate recommendation. http:\/\/www.w3.org\/TR\/xpath20\/.]]"},{"key":"e_1_2_1_10_1","unstructured":"Bray T. Paoli J. Sperberg-McQueen C. M. Maler E. and Yergeau F. 2004. Extensible markup language (XML) 1.0 (3rd ed.) W3C recommendation. http:\/\/www.w3.org\/TR\/2004\/REC-xml-20040204\/.]]  Bray T. Paoli J. Sperberg-McQueen C. M. Maler E. and Yergeau F. 2004. Extensible markup language (XML) 1.0 (3rd ed.) W3C recommendation. http:\/\/www.w3.org\/TR\/2004\/REC-xml-20040204\/.]]"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_12_1","unstructured":"Clark J. and DeRose S. 1999. XML path language (XPath) version 1.0 W3C recommendation. http:\/\/www.w3.org\/TR\/1999\/REC-xpath-19991116.]]  Clark J. and DeRose S. 1999. XML path language (XPath) version 1.0 W3C recommendation. http:\/\/www.w3.org\/TR\/1999\/REC-xpath-19991116.]]"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the Logic of Programs Workshop. Lecture Notes in Computer Science","volume":"131","author":"Clarke E. M.","unstructured":"Clarke , E. M. and Emerson , E. A . 1981. Design and synthesis of synchronization skeletons using branching-time temporal logic . In Proceedings of the Logic of Programs Workshop. Lecture Notes in Computer Science vol. 131 . Springer-Verlag. 52--71.]] Clarke, E. M. and Emerson, E. A. 1981. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proceedings of the Logic of Programs Workshop. Lecture Notes in Computer Science vol. 131. Springer-Verlag. 52--71.]]"},{"key":"e_1_2_1_14_1","volume-title":"KRDB: Proceedings of the 8th International Workshop on Knowledge Representation Meets Databases. CEUR Workshop Proceedings","volume":"45","author":"Deutsch A.","unstructured":"Deutsch , A. and Tannen , V . 2001. Containment of regular path expressions under integrity constraints . In KRDB: Proceedings of the 8th International Workshop on Knowledge Representation Meets Databases. CEUR Workshop Proceedings vol. 45 , 1--11.]] Deutsch, A. and Tannen, V. 2001. Containment of regular path expressions under integrity constraints. In KRDB: Proceedings of the 8th International Workshop on Knowledge Representation Meets Databases. CEUR Workshop Proceedings vol. 45, 1--11.]]"},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","first-page":"406","DOI":"10.1016\/S0022-0000(70)80041-1","article-title":"Tree acceptors and some of their applications","volume":"4","author":"Doner J.","year":"1970","unstructured":"Doner , J. 1970 . Tree acceptors and some of their applications . J. Comput. Syst. Sci. 4 , 406 -- 451 .]] Doner, J. 1970. Tree acceptors and some of their applications. J. Comput. Syst. Sci. 4, 406--451.]]","journal-title":"J. Comput. Syst. Sci."},{"key":"e_1_2_1_16_1","unstructured":"Edmund M. Clarke J. Grumberg O. and Peled D. A. 1999. Model Checking. MIT Press Cambridge MA.]]   Edmund M. Clarke J. Grumberg O. and Peled D. A. 1999. Model Checking. MIT Press Cambridge MA.]]"},{"key":"e_1_2_1_17_1","unstructured":"Fallside D. C. and Walmsley P. 2004. XML Schema part 0: Primer 2nd ed. W3C recommendation. http:\/\/www.w3.org\/TR\/xmlschema-0\/.]]  Fallside D. C. and Walmsley P. 2004. XML Schema part 0: Primer 2nd ed. W3C recommendation. http:\/\/www.w3.org\/TR\/xmlschema-0\/.]]"},{"key":"e_1_2_1_18_1","volume-title":"SIGMOD: Proceedings of the ACM SIGMOD International Conference on Management of Data. ACM Press","author":"Fan W.","unstructured":"Fan , W. , Chan , C.-Y. , and Garofalakis , M . 2004. Secure XML querying with security views . In SIGMOD: Proceedings of the ACM SIGMOD International Conference on Management of Data. ACM Press , New York. 587--598.]] 10.1145\/1007568.1007634 Fan, W., Chan, C.-Y., and Garofalakis, M. 2004. Secure XML querying with security views. In SIGMOD: Proceedings of the ACM SIGMOD International Conference on Management of Data. ACM Press, New York. 587--598.]] 10.1145\/1007568.1007634"},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","article-title":"Propositional dynamic logic of regular programs","volume":"18","author":"Fischer M. J.","year":"1979","unstructured":"Fischer , M. J. and Ladner , R. E. 1979 . Propositional dynamic logic of regular programs . J. Comput. Syst. Sci. 18 , 2, 194 -- 211 .]] Fischer, M. J. and Ladner, R. E. 1979. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 2, 194--211.]]","journal-title":"J. Comput. Syst. Sci."},{"key":"e_1_2_1_20_1","series-title":"Lecture Notes in Computer Science","volume-title":"XSYM: Proceedings of the 3rd International Symposium on Database and XML Technologies","author":"Franceschet M.","unstructured":"Franceschet , M. 2005. XPathMark---An XPath benchmark for XMark generated data . In XSYM: Proceedings of the 3rd International Symposium on Database and XML Technologies . Lecture Notes in Computer Science vol. 3671 . Springer-Verlag . 129--143.]] 10.1007\/11547273_10 Franceschet, M. 2005. XPathMark---An XPath benchmark for XMark generated data. In XSYM: Proceedings of the 3rd International Symposium on Database and XML Technologies. Lecture Notes in Computer Science vol. 3671. Springer-Verlag. 129--143.]] 10.1007\/11547273_10"},{"key":"e_1_2_1_21_1","unstructured":"Genev\u00e8s P. and Laya\u00efda N. 2006. A &mu;-calculus satisfiability solver for XML. http:\/\/wam.inrialpes.fr\/xml.]]  Genev\u00e8s P. and Laya\u00efda N. 2006. A &mu;-calculus satisfiability solver for XML. http:\/\/wam.inrialpes.fr\/xml.]]"},{"key":"e_1_2_1_22_1","volume-title":"DocEng: Proceedings of the ACM Symposium on Document Engineering. ACM Press","author":"Genev\u00e8s P.","unstructured":"Genev\u00e8s , P. and Vion-Dury , J . -Y. 2004a. Logic-Based XPath optimization . In DocEng: Proceedings of the ACM Symposium on Document Engineering. ACM Press , New York. 211--219.]] 10.1145\/1030397.1030437 Genev\u00e8s, P. and Vion-Dury, J.-Y. 2004a. Logic-Based XPath optimization. In DocEng: Proceedings of the ACM Symposium on Document Engineering. ACM Press, New York. 211--219.]] 10.1145\/1030397.1030437"},{"key":"e_1_2_1_23_1","volume-title":"TPHOLs: Emerging Trends Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics","author":"Genev\u00e8s P.","unstructured":"Genev\u00e8s , P. and Vion-Dury , J . -Y. 2004b. XPath formal semantics and beyond: A Coq-Based approach . In TPHOLs: Emerging Trends Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics . Salt Lake City, UT. 181--198.]] Genev\u00e8s, P. and Vion-Dury, J.-Y. 2004b. XPath formal semantics and beyond: A Coq-Based approach. In TPHOLs: Emerging Trends Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics. Salt Lake City, UT. 181--198.]]"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1071610.1071614"},{"key":"e_1_2_1_25_1","volume-title":"Eds","author":"Gr\u00e4del E.","year":"2002","unstructured":"Gr\u00e4del , E. , Thomas , W. , and Wilke , T. , Eds . 2002 . Automata Logics, and Infinite Games: A Guide to Current Research. Springer-Verlag , New York.]] Gr\u00e4del, E., Thomas, W., and Wilke, T., Eds. 2002. Automata Logics, and Infinite Games: A Guide to Current Research. Springer-Verlag, New York.]]"},{"key":"e_1_2_1_26_1","first-page":"1","article-title":"Some classes of recursive functions","volume":"4","author":"Grzegorczyk A.","year":"1953","unstructured":"Grzegorczyk , A. 1953 . Some classes of recursive functions . Rozprawy Matematyczne 4 , 1 -- 45 .]] Grzegorczyk, A. 1953. Some classes of recursive functions. Rozprawy Matematyczne 4, 1--45.]]","journal-title":"Rozprawy Matematyczne"},{"key":"e_1_2_1_27_1","volume-title":"ICCD: Proceedings of the International Conference on Computer Design, VLSI in Computers and Processors. IEEE Computer Society. 12--19","author":"Hojati R.","unstructured":"Hojati , R. , Krishnan , S. C. , and Brayton , R. K . 1996. Early quantification and partitioned transition relations . In ICCD: Proceedings of the International Conference on Computer Design, VLSI in Computers and Processors. IEEE Computer Society. 12--19 .]] Hojati, R., Krishnan, S. C., and Brayton, R. K. 1996. Early quantification and partitioned transition relations. In ICCD: Proceedings of the International Conference on Computer Design, VLSI in Computers and Processors. IEEE Computer Society. 12--19.]]"},{"key":"e_1_2_1_28_1","unstructured":"Hopcroft J. E. Motwani R. Rotwani and Ullman J. D. 2000. Introduction to Automata Theory Languages and Computability. Addison-Wesley Longman Boston.]]   Hopcroft J. E. Motwani R. Rotwani and Ullman J. D. 2000. Introduction to Automata Theory Languages and Computability. Addison-Wesley Longman Boston.]]"},{"key":"e_1_2_1_29_1","unstructured":"Hoschka P. 1998. Synchronized multimedia integration language (SMIL) 1.0 specification W3C recommendation. http:\/\/www.w3.org\/TR\/REC-smil\/.]]  Hoschka P. 1998. Synchronized multimedia integration language (SMIL) 1.0 specification W3C recommendation. http:\/\/www.w3.org\/TR\/REC-smil\/.]]"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1053468.1053470"},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","article-title":"Results on the propositional &mu;-calculus","volume":"27","author":"Kozen D.","year":"1983","unstructured":"Kozen , D. 1983 . Results on the propositional &mu;-calculus . Theoret. Comput. Sci. 27 , 333 -- 354 .]] Kozen, D. 1983. Results on the propositional &mu;-calculus. Theoret. Comput. Sci. 27, 333--354.]]","journal-title":"Theoret. Comput. Sci."},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/BF00370554","article-title":"A finite model theorem for the propositional &mu;-calculus","volume":"47","author":"Kozen D.","year":"1988","unstructured":"Kozen , D. 1988 . A finite model theorem for the propositional &mu;-calculus . Studia Logica 47 , 3, 233 -- 241 .]] Kozen, D. 1988. A finite model theorem for the propositional &mu;-calculus. Studia Logica 47, 3, 233--241.]]","journal-title":"Studia Logica"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the 16th Symposium on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science","volume":"1563","author":"Kupferman O.","unstructured":"Kupferman , O. and Vardi , M . 1999. The weakness of self-complementation . In Proceedings of the 16th Symposium on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science vol. 1563 . Springer-Verlag. 455--466.]] Kupferman, O. and Vardi, M. 1999. The weakness of self-complementation. In Proceedings of the 16th Symposium on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science vol. 1563. Springer-Verlag. 455--466.]]"},{"key":"e_1_2_1_34_1","volume-title":"DBPL: Proceedings of the 10th International Symposium on Database Programming Languages. Lecture Notes in Computer Science","volume":"3774","author":"Levin M. Y.","unstructured":"Levin , M. Y. and Pierce , B. C . 2005. Type-Based optimization for regular patterns . In DBPL: Proceedings of the 10th International Symposium on Database Programming Languages. Lecture Notes in Computer Science vol. 3774 . Springer-Verlag.]] 10.1007\/11601524_12 Levin, M. Y. and Pierce, B. C. 2005. Type-Based optimization for regular patterns. In DBPL: Proceedings of the 10th International Symposium on Database Programming Languages. Lecture Notes in Computer Science vol. 3774. Springer-Verlag.]] 10.1007\/11601524_12"},{"key":"e_1_2_1_35_1","volume-title":"PODS: Proceedings of the 23rd ACM Symposium on Principles of Database Systems. ACM","author":"Martens W.","unstructured":"Martens , W. and Neven , F . 2004. Frontiers of tractability for typechecking simple XML transformations . In PODS: Proceedings of the 23rd ACM Symposium on Principles of Database Systems. ACM , New York. 23--34.]] 10.1145\/1055558.1055563 Martens, W. and Neven, F. 2004. Frontiers of tractability for typechecking simple XML transformations. In PODS: Proceedings of the 23rd ACM Symposium on Principles of Database Systems. ACM, New York. 23--34.]] 10.1145\/1055558.1055563"},{"key":"e_1_2_1_36_1","volume-title":"PODS: Proceedings of the 23rd ACM Symposium on Principles of Database Systems. ACM","author":"Marx M.","year":"2004","unstructured":"Marx , M. 2004 a. Conditional XPath, the 1st order complete XPath dialect . In PODS: Proceedings of the 23rd ACM Symposium on Principles of Database Systems. ACM , New York. 13--22.]] 10.1145\/1055558.1055562 Marx, M. 2004a. Conditional XPath, the 1st order complete XPath dialect. In PODS: Proceedings of the 23rd ACM Symposium on Principles of Database Systems. ACM, New York. 13--22.]] 10.1145\/1055558.1055562"},{"key":"e_1_2_1_37_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 9th International Conference on Extending Database Technology","author":"Marx M.","unstructured":"Marx , M. 2004b. XPath with conditional axis relations . In Proceedings of the 9th International Conference on Extending Database Technology . Lecture Notes in Computer Science vol. 2992 . Springer-Verlag . 477--494.]] Marx, M. 2004b. XPath with conditional axis relations. In Proceedings of the 9th International Conference on Extending Database Technology. Lecture Notes in Computer Science vol. 2992. Springer-Verlag. 477--494.]]"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/962446.962448"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111627.1111631"},{"key":"e_1_2_1_40_1","volume-title":"CSL: Proceedings of the 16th International Workshop and 11th Annual Conference of the EACSL on Computer Science Logic. Springer-Verlag. 2--26","author":"Neven F.","year":"2002","unstructured":"Neven , F. 2002 a. Automata, logic, and XML . In CSL: Proceedings of the 16th International Workshop and 11th Annual Conference of the EACSL on Computer Science Logic. Springer-Verlag. 2--26 .]] Neven, F. 2002a. Automata, logic, and XML. In CSL: Proceedings of the 16th International Workshop and 11th Annual Conference of the EACSL on Computer Science Logic. Springer-Verlag. 2--26.]]"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/601858.601869"},{"key":"e_1_2_1_42_1","volume-title":"ICDT: Proceedings of the 9th International Conference on Database Theory. Lecture Notes in Computer Science","volume":"2572","author":"Neven F.","unstructured":"Neven , F. and Schwentick , T . 2003. XPath containment in the presence of disjunction, DTDs, and variables . In ICDT: Proceedings of the 9th International Conference on Database Theory. Lecture Notes in Computer Science vol. 2572 . Springer-Verlag. 315--329.]] Neven, F. and Schwentick, T. 2003. XPath containment in the presence of disjunction, DTDs, and variables. In ICDT: Proceedings of the 9th International Conference on Database Theory. Lecture Notes in Computer Science vol. 2572. Springer-Verlag. 315--329.]]"},{"key":"e_1_2_1_43_1","volume-title":"CADE: Proceedings of the 18th International Conference on Automated Deduction. Springer-Verlag. 16--30","author":"Pan G.","unstructured":"Pan , G. , Sattler , U. , and Vardi , M. Y . 2002. BDD-Based decision procedures for K . In CADE: Proceedings of the 18th International Conference on Automated Deduction. Springer-Verlag. 16--30 .]] Pan, G., Sattler, U., and Vardi, M. Y. 2002. BDD-Based decision procedures for K. In CADE: Proceedings of the 18th International Conference on Automated Deduction. Springer-Verlag. 16--30.]]"},{"key":"e_1_2_1_44_1","volume-title":"Pemberton, S. 2000. XHTML 1.0 the extensible hypertext markup language","unstructured":"Pemberton, S. 2000. XHTML 1.0 the extensible hypertext markup language ( 2 nd ed.), W3C recommendation. http:\/\/www.w3.org\/TR\/xhtml1\/.]] Pemberton, S. 2000. XHTML 1.0 the extensible hypertext markup language (2nd ed.), W3C recommendation. http:\/\/www.w3.org\/TR\/xhtml1\/.]]","edition":"2"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/974121.974140"},{"key":"e_1_2_1_46_1","volume-title":"PLAN-X: Proceedings of the International Workshop on Programming Language Technologies for XML","volume":"4","author":"Sur G.","unstructured":"Sur , G. , Hammer , J. , and Sim\u00e9on , J . 2004. Updatex---An XQuery-Based language for processing updates in XML . In PLAN-X: Proceedings of the International Workshop on Programming Language Technologies for XML . Venice, Italy. BRICS Notes Series vol. NS-03- 4 . BRICS, Aarhus, Denmark. 40--53.]] Sur, G., Hammer, J., and Sim\u00e9on, J. 2004. Updatex---An XQuery-Based language for processing updates in XML. In PLAN-X: Proceedings of the International Workshop on Programming Language Technologies for XML. Venice, Italy. BRICS Notes Series vol. NS-03-4. BRICS, Aarhus, Denmark. 40--53.]]"},{"key":"e_1_2_1_47_1","volume-title":"TABLEAUX: Proceedings of the 14th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science","volume":"3702","author":"Tanabe Y.","unstructured":"Tanabe , Y. , Takahashi , K. , Yamamoto , M. , Tozawa , A. , and Hagiya , M . 2005. A decision procedure for the alternation-free two-way modal &mu;-calculus . In TABLEAUX: Proceedings of the 14th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science vol. 3702 . Springer-Verlag. 277--291.]] 10.1007\/11554554_21 Tanabe, Y., Takahashi, K., Yamamoto, M., Tozawa, A., and Hagiya, M. 2005. A decision procedure for the alternation-free two-way modal &mu;-calculus. In TABLEAUX: Proceedings of the 14th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science vol. 3702. Springer-Verlag. 277--291.]] 10.1007\/11554554_21"},{"key":"e_1_2_1_48_1","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/BF01691346","article-title":"Generalized finite automata theory with an application to a decision problem of second-order logic","volume":"2","author":"Thatcher J. W.","year":"1968","unstructured":"Thatcher , J. W. and Wright , J. B. 1968 . Generalized finite automata theory with an application to a decision problem of second-order logic . Math. Syst. Theory 2 , 1, 57 -- 81 .]] Thatcher, J. W. and Wright, J. B. 1968. Generalized finite automata theory with an application to a decision problem of second-order logic. Math. Syst. Theory 2, 1, 57--81.]]","journal-title":"Math. Syst. Theory"},{"key":"e_1_2_1_49_1","volume-title":"DocEng: Proceedings of the ACM Symposium on Document Engineering. ACM","author":"Tozawa A.","year":"2001","unstructured":"Tozawa , A. 2001 . Towards static type checking for XSLT . In DocEng: Proceedings of the ACM Symposium on Document Engineering. ACM , New York. 18--27.]] 10.1145\/502187.502191 Tozawa, A. 2001. Towards static type checking for XSLT. In DocEng: Proceedings of the ACM Symposium on Document Engineering. ACM, New York. 18--27.]] 10.1145\/502187.502191"},{"key":"e_1_2_1_50_1","volume-title":"ICALP: Proceedings of the 25th International Colloquium on Automata, Languages and Programming. Springer-Verlag. 628--641","author":"Vardi M. Y.","year":"1998","unstructured":"Vardi , M. Y. 1998 . Reasoning about the past with two-way automata . In ICALP: Proceedings of the 25th International Colloquium on Automata, Languages and Programming. Springer-Verlag. 628--641 .]] Vardi, M. Y. 1998. Reasoning about the past with two-way automata. In ICALP: Proceedings of the 25th International Colloquium on Automata, Languages and Programming. Springer-Verlag. 628--641.]]"},{"key":"e_1_2_1_51_1","unstructured":"Wadler P. 2000. Two semantics for XPath. Internal Tech. Note of the W3C XSL Working Group. http:\/\/homepages.inf.ed.ac.uk\/wadler\/papers\/xpath-semantics\/xpath-semantics.pdf.]]  Wadler P. 2000. Two semantics for XPath. Internal Tech. Note of the W3C XSL Working Group. http:\/\/homepages.inf.ed.ac.uk\/wadler\/papers\/xpath-semantics\/xpath-semantics.pdf.]]"},{"key":"e_1_2_1_52_1","series-title":"Lecture Notes in Computer Science","volume-title":"CL: Proceedings of the 1st International Conference on Computational Logic","author":"Wood P. T.","unstructured":"Wood , P. T. 2000. On the equivalence of XML patterns . In CL: Proceedings of the 1st International Conference on Computational Logic . Lecture Notes in Computer Science vol. 1861 . Springer-Verlag . 1152--1166.]] Wood, P. T. 2000. On the equivalence of XML patterns. In CL: Proceedings of the 1st International Conference on Computational Logic. Lecture Notes in Computer Science vol. 1861. Springer-Verlag. 1152--1166.]]"},{"key":"e_1_2_1_53_1","series-title":"Lecture Notes in Computer Science","volume-title":"ICDT: Proceedings of the 9th International Conference on Database Theory","author":"Wood P. T.","unstructured":"Wood , P. T. 2003. Containment for XPath fragments under DTD constraints . In ICDT: Proceedings of the 9th International Conference on Database Theory . Lecture Notes in Computer Science vol. 2572 . Springer-Verlag . 300--314.]] Wood, P. T. 2003. Containment for XPath fragments under DTD constraints. In ICDT: Proceedings of the 9th International Conference on Database Theory. Lecture Notes in Computer Science vol. 2572. Springer-Verlag. 300--314.]]"}],"container-title":["ACM Transactions on Information Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1185877.1185882","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T21:39:39Z","timestamp":1672263579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1185877.1185882"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,10]]},"references-count":53,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2006,10]]}},"alternative-id":["10.1145\/1185877.1185882"],"URL":"https:\/\/doi.org\/10.1145\/1185877.1185882","relation":{},"ISSN":["1046-8188","1558-2868"],"issn-type":[{"value":"1046-8188","type":"print"},{"value":"1558-2868","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,10]]},"assertion":[{"value":"2006-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}