]. 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

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.

V. Benzaken, G. Castagna, and A. Frisch, CDuce: An XML-centric generalpurpose language, ICFP '03: Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, pp.51-63, 2003.
URL : https://hal.archives-ouvertes.fr/hal-00152619

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. 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.

D. Colazzo, G. Ghelli, P. Manghi, and C. Sartiani, Static analysis for path correctness of XML queries, Journal of Functional Programming, vol.16, issue.4&5, pp.4-5621, 2006.
DOI : 10.1017/S0956796806005983

S. Dal-zilio, D. Lugiez, and C. Meyssonnier, A logic you can count on, POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.135-146, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00071562

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

J. , E. M. Clarke, O. Grumberg, and D. A. Peled, Model Checking, 1999.
DOI : 10.1002/9780470050118.ecse247

E. A. Emerson and C. S. Jutla, Tree automata, µ-calculus and determinacy, Proceedings of the 32nd annual Symposium on Foundations of Computer Science, pp.368-377, 1991.

D. C. Fallside and P. Walmsley, XML Schema part 0: Primer second edition, W3C recommendation, 2004.

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

V. Gapeyev and B. C. Pierce, Regular object types A preliminary version was presented at FOOL '03, European Conference on Object-Oriented Programming, pp.151-175, 2003.

V. Gapeyev and B. C. Pierce, Paths into patterns, 2004.

P. Genevès and N. Laya¨?dalaya¨?da, A system for the static analysis of XPath, ACM Transactions on Information Systems, vol.24, issue.4, pp.475-502, 2006.
DOI : 10.1145/1185877.1185882

P. Genevès and N. Laya¨?dalaya¨?da, Deciding XPath containment with MSO, Data & Knowledge Engineering, vol.63, issue.1, pp.108-136, 2007.
DOI : 10.1016/j.datak.2006.11.003

P. Genevès, N. Laya¨?dalaya¨?da, and A. Schmitt, A satisfiability solver for XML and XPath, 2006.

P. Genevès, N. Laya¨?dalaya¨?da, and A. Schmitt, Efficient static analysis of XML paths and types, PLDI '07: Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, pp.342-351, 2007.

P. Genevès and J. Vion-dury, Logic-based XPath optimization, DocEng '04: Proceedings of the 2004 ACM Symposium on Document Engineering, pp.211-219, 2004.

E. Grädel, W. Thomas, and T. Wilke, Automata logics, and infinite games: a guide to current research, 2002.
DOI : 10.1007/3-540-36387-4

R. Hojati, S. C. Krishnan, and R. K. Brayton, Early quantification and partitioned transition relations, Proceedings International Conference on Computer Design. VLSI in Computers and Processors, pp.12-19, 1996.
DOI : 10.1109/ICCD.1996.563525

H. Hosoya and B. C. Pierce, XDuce, ACM Transactions on Internet Technology, vol.3, issue.2, pp.117-148, 2003.
DOI : 10.1145/767193.767195

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. P. Huet, The Zipper, Journal of Functional Programming, vol.7, issue.5, pp.549-554, 1997.
DOI : 10.1017/S0956796897002864

D. Kozen, Results on the Propositional ??-Calculus, DAIMI Report Series, vol.11, issue.146, pp.333-354, 1983.
DOI : 10.7146/dpb.v11i146.7420

O. Kupferman and M. Vardi, The Weakness of Self-Complementation, Proc. 16th Symp. on Theoretical Aspects of Computer Science, pp.455-466, 1999.
DOI : 10.1007/3-540-49116-3_43

M. Y. Levin and B. C. Pierce, Type-Based Optimization for Regular Patterns, DBPL '05: Proceedings of the 10th International Symposium on Database Programming Languages, 2005.
DOI : 10.1007/11601524_12

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

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

A. Møller, M. O. Olesen, and M. I. Schwartzbach, Static validation of XSL Transformations, BRICS, 2005.

A. Møller and M. I. Schwartzbach, The design space of type checkers for XML transformation languages, Proc. Tenth International Conference on Database Theory, ICDT '05, pp.17-36, 2005.

M. Murata, D. Lee, M. Mani, and K. Kawaguchi, Taxonomy of XML schema languages using formal language theory, ACM Transactions on Internet Technology, vol.5, issue.4, pp.660-704, 2005.
DOI : 10.1145/1111627.1111631

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.

D. Olteanu, H. Meuss, T. Furche, and F. Bry, XPath: Looking Forward, EDBT '02: Proceedings of the Worshop on XML-Based Data Management, pp.109-127, 2002.
DOI : 10.1007/3-540-36128-6_7

G. Pan, U. Sattler, and M. Y. Vardi, BDD-based decision procedures for the modal logic K ???, Journal of Applied Non-Classical Logics, vol.2, issue.2, pp.169-208, 2006.
DOI : 10.1016/0004-3702(92)90049-4

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

Y. Tanabe, K. Takahashi, M. Yamamoto, A. Tozawa, and M. Hagiya, A Decision Procedure for the Alternation-Free Two-Way Modal ??-Calculus, TABLEAUX 2005, 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, On binary tree logic for XML and its satisfiability test, PPL '04: the Sixth JSSST Workshop on Programming and Programming Languages Informal Proceedings, 2004.

M. Y. Vardi, Reasoning about the past with two-way automata, ICALP '98: Proceedings of the 25th International Colloquium on Automata, Languages and Programming, pp.628-641, 1998.
DOI : 10.1007/BFb0055090