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

B. , E. Genev-`-esgenev-`-genev-`-es, P. And-laya¨idalaya¨ida, and N. , On the analysis of queries with counting constraints, DocEng '09: Proceedings of the 9th ACM symposium on Document engineering, pp.21-24, 2009.

B. , E. Genev-`-esgenev-`-genev-`-es, P. Laya¨idalaya¨ida, N. And, and A. Schmitt, Query reasoning on trees with types, interleaving and counting, IJCAI'11 : Proceedings of the 22nd International Joint Conference on Artificial Intelligence, pp.718-723, 2011.

B. , V. Castagna, G. And-frisch, and A. , CDuce: An XML-centric general-purpose 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

C. , D. De-giacomo, G. Lenzerini, M. And, and M. Y. Vardi, Regular XPath: Constraints, query containment and view-based answering for xml documents, Proc. of the 2008 Int. Workshop on Logic in Databases, 2008.

C. , D. De-giacomo, G. Lenzerini, M. And, and M. Y. Vardi, An automata-theoretic approach to regular XPath, Proc. of the 12th Int. Symposium on Database Programming Languages, pp.18-35, 2009.

C. , D. Giacomo, G. D. Lenzerini, M. And, and M. Y. Vardi, Node selection query languages for trees, 2010.

C. , J. And-derose, and S. , XML path language (XPath) version 1.0, W3C recommendation, 1999.

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

C. , E. M. Grumberg, O. And-peled, and D. A. , Model checking, 1999.

F. , M. J. And, and R. E. Ladner, Propositional dynamic logic of regular programs, JCSS, vol.18, issue.2, pp.194-211, 1979.

F. , O. And, and M. Lange, The pgsolver collection of parity game solvers, 2009.

F. , O. And, and M. Lange, A solver for modal fixpoint logics, Electron. Notes Theor. Comput. Sci, vol.262, pp.99-111, 2010.

P. Genev-`-esgenev-`-genev-`-es, N. Gesbert, N. Laya¨idalaya¨ida, . And, and A. Schmitt, A satisfiability solver for XML and XPath, 2014.

P. Genev-`-esgenev-`-genev-`-es and N. And-laya¨idalaya¨ida, 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-`-esgenev-`-genev-`-es, N. Laya¨idalaya¨ida, . And, 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.

G. Gr¨adel, E. Thomas, W. And-wilke, and T. , Automata logics, and infinite games: a guide to current research, 2002.

H. , R. Krishnan, S. C. And-brayton, and R. K. , Early quantification and partitioned transition relations, ICCD '96: Proceedings of the 1996 International Conference on Computer Design, VLSI in Computers and Processors, pp.12-19, 1996.

H. , H. Vouillon, J. And-pierce, and B. C. , Regular expression types for XML, ACM Trans. Program. Lang. Syst, vol.27, issue.1, pp.46-90, 2005.
URL : https://hal.archives-ouvertes.fr/hal-00009271

K. , O. And, and M. Vardi, The weakness of self-complementation, Proc. 16th Symp. on Theoretical Aspects of Computer Science, pp.455-466, 1999.

L. , L. And, and C. Sirangelo, Reasoning about xml with temporal logics and automata, LPAR '08: Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, pp.97-112, 2008.

L. , L. And, and C. Sirangelo, Reasoning about xml with temporal logics and automata, J. Applied Logic, vol.8, issue.2, pp.210-232, 2010.

M. , G. And, and D. Suciu, Containment and equivalence for a fragment of XPath, Journal of the ACM, vol.51, issue.1, pp.2-45, 2004.

M. , M. Lee, D. Mani, M. And-kawaguchi, and K. , Taxonomy of XML schema languages using formal language theory, ACM Transactions on Internet Technology, vol.5, issue.4, pp.660-704, 2005.

O. , D. Meuss, H. Furche, T. And-bry, and F. , XPath: Looking forward, EDBT '02: Proceedings of the Worshop on XML-Based Data Management, pp.109-127, 2002.

P. , G. Sattler, U. And, and M. Y. Vardi, BDD-based decision procedures for the modal logic K, Journal of Applied Non-classical Logics, vol.16, pp.1-2, 2006.

T. , Y. Takahashi, K. And-hagiya, and M. , A decision procedure for alternation-free modal µcalculi, Advances in Modal Logic, pp.341-362, 2008.

T. , Y. Takahashi, K. Yamamoto, M. Tozawa, A. And-hagiya et al., A decision procedure for the alternation-free two-way modal µ-calculus, TABLEAUX 2005, pp.277-291, 2005.

J. Voss, Wikipedia dtd, 2007.

Z. , K. Kuncak, V. And-rinard, and M. C. , Full functional verification of linked data structures, pp.349-361, 2008.