]. L. Afanasiev, P. Blackburn, I. Dimitriou, B. Gaiffe, E. Goris et al., PDL for ordered trees, Journal of Applied Non-Classical Logics, vol.32, issue.2, pp.115-135, 2005.
DOI : 10.3166/jancl.15.115-135
URL : https://hal.archives-ouvertes.fr/inria-00001206

S. Amer-yahia, S. Cho, L. V. Lakshmanan, and D. Srivastava, Minimization of tree pattern queries, ACM SIGMOD Record, vol.30, issue.2, pp.497-508, 2001.
DOI : 10.1145/376284.375730

P. Barceló and L. Libkin, Temporal Logics over Unranked Trees, 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), pp.31-40, 2005.
DOI : 10.1109/LICS.2005.51

M. Benedikt, W. Fan, and F. Geerts, XPath satisfiability in the presence of DTDs, PODS '05: Proceedings of the twenty-fourth ACM Symposium on Principles of Database Systems, pp.25-36, 2005.

M. Benedikt, W. Fan, and G. M. Kuper, Structural properties of XPath fragments, Theoretical Computer Science, vol.336, issue.1, pp.3-31, 2005.
DOI : 10.1016/j.tcs.2004.10.030

M. Benedikt and L. Segoufin, Regular Tree Languages Definable in FO, STACS '05: Proceedings of the 22nd Annual Symposium on Theoretical Aspects of Computer Science, pp.327-339, 2005.
DOI : 10.1007/978-3-540-31856-9_27

M. Biehl, N. Klarlund, and T. Rauhe, Algorithms for guided tree automata, WIA '96: Revised Papers from the First International Workshop on Implementing Automata, pp.6-25, 1997.
DOI : 10.1007/3-540-63174-7_2

R. E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, vol.35, issue.8, pp.677-691, 1986.
DOI : 10.1109/TC.1986.1676819

J. Büchi, Weak Second-Order Arithmetic and Finite Automata, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, pp.66-92, 1960.
DOI : 10.1002/malq.19600060105

J. Clark and S. Derose, XML path language (XPath) version 1.0, W3C recommendation, 1999.

E. M. Clarke and E. A. Emerson, Design and synthesis of synchronization skeletons using branching-time temporal logic, Logic of Programs, pp.52-71, 1981.

A. Deutsch and V. Tannen, Containment of regular path expressions under integrity constraints, KRDB '01: Proceedings of the 8th International Workshop on Knowledge Representation meets Databases CEUR Workshop Proceedings, pp.1-11, 2001.

J. Doner, Tree acceptors and some of their applications, Journal of Computer and System Sciences, vol.4, issue.5, pp.406-451, 1970.
DOI : 10.1016/S0022-0000(70)80041-1

D. Draper, P. Fankhauser, M. Fernández, A. Malhotra, K. Rose et al., XQuery 1.0 and XPath 2.0 formal semantics, W3C working draft, 2005.

J. Elgaard, A. Møller, and M. I. Schwartzbach, Compile-Time Debugging of C Programs Working on Trees, ESOP '00: Proceedings of the 9th European Symposium on Programming Languages and Systems, pp.119-134, 2000.
DOI : 10.1007/3-540-46425-5_8

C. Elgot, Decision problems of finite automata design and related arithmetics. Transactions of the, pp.21-52, 1961.

W. Fan, C. Chan, and M. Garofalakis, Secure XML querying with security views, Proceedings of the 2004 ACM SIGMOD international conference on Management of data , SIGMOD '04, pp.587-598, 2004.
DOI : 10.1145/1007568.1007634

M. J. Fischer and R. E. Ladner, Propositional dynamic logic of regular programs, Journal of Computer and System Sciences, vol.18, issue.2, pp.194-211, 1979.
DOI : 10.1016/0022-0000(79)90046-1

M. Franceschet, XPathMark: An XPath Benchmark for the XMark Generated Data, XSYM '05: Proceedings of The Third International Symposium on Database and XML Technologies, pp.129-143, 2005.
DOI : 10.1007/11547273_10

P. Genevès and J. Vion-dury, XPath formal semantics and beyond: A Coq-based approach, TPHOLs '04: Emerging Trends Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics, pp.181-198, 2004.

A. Grzegorczyk, Some classes of recursive functions, Rozprawy Matematyczne, vol.4, pp.1-45, 1953.

H. Hosoya, J. Vouillon, and B. C. Pierce, Regular expression types for XML, ACM Transactions on Programming Languages and Systems, vol.27, issue.1, pp.46-90, 2005.
DOI : 10.1145/1053468.1053470
URL : https://hal.archives-ouvertes.fr/hal-00009271

G. Huet, G. Kahn, and C. Paulin-mohring, The Coq Proof Assistant -A tutorial - Version 8.0. INRIA, 2004.

N. Klarlund, &. Mona, and . Fido, The logic-automaton connection in practice. In CSL '97: Selected Papers from the 11th International Workshop on Computer Science Logic, LNCS, vol.1414, pp.311-326, 1998.

N. Klarlund and A. Møller, MONA Version 1.4 User Manual. BRICS Notes Series NS-01-1, 2001.

N. Klarlund, A. Møller, and M. I. Schwartzbach, MONA implementation secrets, CIAA '00: Revised Papers from the 5th International Conference on Implementation and Application of Automata, pp.182-194, 2001.

M. Marx, Conditional XPath, the first order complete XPath dialect, Proceedings of the twenty-third ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems , PODS '04, pp.13-22, 2004.
DOI : 10.1145/1055558.1055562

M. Marx, XPath with Conditional Axis Relations, Proceedings of the 9th International Conference on Extending Database Technology, pp.477-494, 2004.
DOI : 10.1007/978-3-540-24741-8_28
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.9.7870

A. Meyer, Weak monadic second-order theory of successor is not elementary-recursive

G. Miklau and D. Suciu, Containment and equivalence for a fragment of XPath, Journal of the ACM, vol.51, issue.1, pp.2-45, 2004.
DOI : 10.1145/962446.962448

F. Neven, Automata theory for XML researchers, ACM SIGMOD Record, vol.31, issue.3, pp.39-46, 2002.
DOI : 10.1145/601858.601869
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.12.907

F. Neven and T. Schwentick, XPath containment in the presence of disjunction, DTDs, and variables, ICDT '03: Proceedings of the 9th International Conference on Database Theory, pp.315-329, 2003.

T. Schwentick, XPath query containment, ACM SIGMOD Record, vol.33, issue.1, pp.101-109, 2004.
DOI : 10.1145/974121.974140

L. Stockmeyer, The complexity of decision problems in automata theory and logic, Project MAC, M.I.T, 1974.

L. Stockmeyer and A. Meyer, Word problems requiring exponential time, STOC '73: Proceedings of the 5th ACM symposium on Theory of computing, pp.1-9, 1973.
DOI : 10.1145/800125.804029
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.116.4618

G. Sur, J. Hammer, and J. Siméon, Updatex -an XQuery-based language for processing updates in XML, PLAN-X 2004: Proceedings of the International Workshop on Programming Language Technologies for XML NS-03-4 of BRICS Notes Series, pp.40-53, 2004.

Y. Tanabe, K. Takahashi, M. Yamamoto, A. Tozawa, and M. Hagiya, A Decision Procedure for the Alternation-Free Two-Way Modal ??-Calculus, TABLEAUX '05: Proceedings of the 14th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pp.277-291, 2005.
DOI : 10.1007/11554554_21

J. W. Thatcher and J. B. Wright, Generalized finite automata theory with an application to a decision problem of second-order logic, Mathematical Systems Theory, vol.12, issue.1, pp.57-81, 1968.
DOI : 10.1007/BF01691346

A. Tozawa, Towards static type checking for XSLT, Proceedings of the 2001 ACM Symposium on Document engineering , DocEng '01, pp.18-27, 2001.
DOI : 10.1145/502187.502191

]. P. Wadler, Two semantics for XPath Internal Technical Note of the W3C XSL Working Group, 2000.

P. T. Wood, On the Equivalence of XML Patterns, CL '00: Proceedings of the First International Conference on Computational Logic, pp.1152-1166, 2000.
DOI : 10.1007/3-540-44957-4_77

P. T. Wood, Containment for XPath Fragments under DTD Constraints, ICDT '03: Proceedings of the 9th International Conference on Database Theory, pp.300-314, 2003.
DOI : 10.1007/3-540-36285-1_20

I. Unité-de-recherche and . Rhône, Alpes 655, avenue de l'Europe -38334 Montbonnot Saint-Ismier (France) Unité de recherche INRIA Futurs : Parc Club Orsay Université -ZAC des Vignes 4

I. Unité-de-recherche and . Lorraine, Technopôle de Nancy-Brabois -Campus scientifique 615, rue du Jardin Botanique -BP 101 -54602 Villers-lès-Nancy Cedex (France) Unité de recherche INRIA Rennes : IRISA, Campus universitaire de Beaulieu -35042 Rennes Cedex (France) Unité de recherche INRIA Rocquencourt : Domaine de Voluceau -Rocquencourt -BP 105 -78153 Le Chesnay Cedex (France) Unité de recherche, 2004.

I. De-voluceau-rocquencourt, BP 105 -78153 Le Chesnay Cedex (France) http://www.inria.fr ISSN, pp.249-6399