R. Alur and L. D'antoni, Streaming tree transducers, ICALP 2012, vol.7392, pp.42-53
DOI : 10.1145/3092842
URL : https://repository.upenn.edu/cgi/viewcontent.cgi?article=1606&context=cis_papers

, , 2012.

R. Alur and P. Madhusudan, Adding nesting structure to words, J. ACM, vol.56, issue.3, p.43, 2009.

O. Burkart and B. Steffen, Model checking the full modal mu-calculus for infinite sequential processes, ICALP 1997, vol.1256, pp.419-429, 1997.

M. Cadilhac, A. Finkel, and P. Mckenzie, On the expressiveness of Parikh automata and related models, Proceedings of the Third Workshop on Non-Classical Models for Automata and Applications -NCMA 2011, pp.103-119, 2011.

E. M. Clarke, E. A. Emerson, and A. P. Sistla, Automatic verification of finite state concurrent systems using temporal logic specifications, Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, pp.117-126, 1983.

B. Courcelle and J. Engelfriet, Graph Structure and Monadic Second-Order Logic -A Language-Theoretic Approach. Encyclopedia of Mathematics and its Applications, vol.138, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00646514

Z. Dang, O. H. Ibarra, T. Bultan, R. A. Kemmerer, and J. Su, Binary reachability analysis of discrete pushdown timed automata, CAV 2000, vol.1855, pp.69-84, 2000.

L. Dartois, E. Filiot, P. Reynier, and J. Talbot, Two-way visibly pushdown automata and transducers, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, pp.217-226, 2016.
DOI : 10.1145/2933575.2935315
URL : https://hal.archives-ouvertes.fr/hal-01475442

J. Engelfriet and H. J. Hoogeboom, MSO definable string transductions and two-way finite-state transducers, ACM Trans. Comput. Logic, vol.2, issue.2, pp.216-254, 2001.
DOI : 10.1145/371316.371512
URL : http://arxiv.org/pdf/cs/9906007v1.pdf

J. Engelfriet and S. Maneth, Macro tree transducers, attribute grammars, and MSO definable tree translations, Inf. Comput, vol.154, issue.1, pp.34-91, 1999.
DOI : 10.1006/inco.1999.2807
URL : https://doi.org/10.1006/inco.1999.2807

,

J. Esparza and P. Ganty, Complexity of pattern-based verification for multithreaded programs, ACM SIGPLAN Not. -POPL, vol.46, issue.1, pp.499-510, 2011.

D. Figueira and L. Libkin, Path logics for querying graphs: combining expressiveness and efficiency, 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, pp.329-340, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01778476

E. Filiot, J. Raskin, P. Reynier, F. Servais, and J. Talbot, Properties of visibly pushdown transducers, MFCS 2010, vol.6281, pp.355-367, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00492241

P. Gallot, A. Muscholl, G. Puppis, and S. Salvati, On the decomposition of finite-valued streaming string transducers, STACS 2017. LIPIcs, vol.66, p.14, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01431250

C. Haase, On the complexity of model checking counter automata, pp.43-043, 2012.

M. Hague and A. W. Lin, Model checking recursive programs with numeric data types, CAV 2011, vol.6806, pp.743-759

, , 2011.

M. Hague and A. W. Lin, Synchronisation-and reversal-bounded analysis of multithreaded programs with counters, CAV 2012, vol.7358, pp.260-276, 2012.

O. H. Ibarra, Reversal-bounded multicounter machines and their decision problems, J. ACM, vol.25, issue.1, pp.116-133, 1978.
DOI : 10.1145/322047.322058

O. H. Ibarra, Automata with reversal-bounded counters: a survey, DCFS 2014, vol.8614, pp.5-22

, , 2014.

W. Karianto, Parikh automata with pushdown stack, 2004.

F. Klaedtke, Parikh automata and monadic second-order logics with linear cardinality constraints, 2002.

F. Klaedtke, H. Rueß, J. C. Baeten, J. K. Lenstra, and J. Parrow, Monadic second-order logics with cardinalities, ICALP 2003, vol.2719, pp.681-696, 2003.
DOI : 10.1007/3-540-45061-0_54

B. König, J. Esparza, H. Ehrig, A. Rensink, and G. Rozenberg, Verification of graph transformation systems with contextfree specifications, ICGT 2010, vol.6372, pp.107-122, 2010.

R. J. Parikh, On context-free languages, J. ACM, vol.13, issue.4, pp.570-581, 1966.

B. Scarpellini, Complexity of subcases of Presburger arithmetic, Trans. Am. Math. Soc, vol.284, issue.1, pp.203-218, 1984.

S. Schwoon, Model checking pushdown systems, 2002.

J. C. Shepherdson, The reduction of two-way automata to one-way automata, IBM J. Res. Dev, vol.3, issue.2, pp.198-200, 1959.

M. Y. Vardi and P. Wolper, An automata-theoretic approach to automatic program verification (preliminary report), LICS, pp.332-344, 1986.

K. N. Verma, H. Seidl, and T. Schwentick, On the complexity of equational horn clauses, CADE 2005. LNCS (LNAI), vol.3632, pp.337-352, 2005.

I. Walukiewicz, Pushdown processes: games and model-checking, Inf. Comput, vol.164, issue.2, pp.234-263, 2001.
DOI : 10.1006/inco.2000.2894
URL : https://doi.org/10.1006/inco.2000.2894